Durga Vemuri
ABSTRACT
An operating system forms the foundation for all of the user's computer activities. Therefore, it should be trustworthy and function flawlessly. Unfortunately, today's operating systems, such as Windows and Linux, fail to deliver to this ideal, because they suffer from fundamental design flaws and bugs. Their monolithic kernel tend be overloaded with functionality that runs at the highest privilege level. This easily introduces bugs and breaches the Principle of Least Authorization (POLA) with all the related risks. Microkernel operating systems have a different design that makes them less vulnerable to these problems. A microkernel provides only a minimal set of abstractions that runs at the highest privilege level. Extended operating system functionality is typically available by means of user-space servers. By splitting an operating system into small, independent parts, the system becomes less complex and more robust, because the smaller parts are more manageable and help to isolate faults, respectively. This paper reviews the concepts and mechanisms used to improve security in Microkernel Operating system and described in brief about two real-world microkernel operating system, trying to achieve security as its goal.
- P. Derrin, K. Elphinstone, G. Klein, D. Cock, and M. M. T Chakravarty. Running the manual: An approach to high-assurance microkernel development.Google Scholar
- B. Kauer and M. Volp. L4.sec: Preliminary Microkernel Reference manual Dresden University of Technology http://os.inf.tu-dresden.de/L4/L4.Sec/.Google Scholar
- TCG 2005: TCG: What is the Trusted Computing Group https://www.trustedcomputinggroup.org/.Google Scholar
- Wikipedia Various, Security, Wikipedia http://en.wikipedia.org/wiki/Secure.Google Scholar
- Anderson: Ross Andersen: Trusted Computing FAQ. University of Cambridge http://www.cl.cam.ac.uk/users/rja14/tcpa-faq.htmlGoogle Scholar
- Shapiro: Jonathan Shapiro, Understanding the Windows EAL4 Evaluation, Johns Hopkins University Information Security Institute, http://eros.cs.jhu.edu/~shap/NTEAL4.htmlGoogle Scholar
- Verification Technology: Heiko Blume http://kbs.cs.tu-berlin.de/teaching/ws2005/htos/folien/sec_mkernel.pdf.Google Scholar
- Operating system verification: Gerwin Klein http://nsl.ias.ac.in/sadhana/Pdf2009Feb/27.pdfGoogle Scholar
- Cinnabar Networks: Eugen Bacic, Security as core compentency of the QNX microkernel, http://www.ic-4s.com/Whitepapers/QNX/MKS.pdf.Google Scholar
- Turstworthy computing system: Gernot Heiser/Kevin Elphinstone Ihor Kuz Gerwin Klein Stefan M. Petters, Taking Microkernels to the Next Level, http://www.ok-labs.com/_assets/image_library/Trustworthy_Computing_Systems.pdfGoogle Scholar
- seL4: Gerwin Klein 1;2, Kevin Elphinstone 1;2, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrishl, Thomas Sewell 1, Harvey Tuch, Simon Winwood. Formal Verification of Microkernel. http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf.Google Scholar
- Garfinkel 2004: Garfinkel et al, Terra: A Virtual Machine-based Platform for Trusted Computing, Stanford University 2004.Google Scholar
- VMware 2005: VMWare Inc.: VMware - Virtual Infrastructure Software. EMC Corporation 2005, http://www.vmware.com/.Google Scholar
- Xen 2005: Ian Pratt: Xen virtual machine monitor. Cambridge University 2005, http://www.cl.cam.ac.uk/Research/SRG/netos/xen/Google Scholar
- TCG 2005: TCG: What is the Trusted Computing Group. Trusted computing Group 2005, https://www.trustedcomputinggroup.org/Google Scholar
- USFS1037C: Various, Federal Standard 1037C, Institute for Telecommunication Sciences 2000, http://www.its.bldrdoc.gov/fs-1037/fs-1037c.htm.Google Scholar
- Garfinkel 2005: Simson L. Garfinkel, Design Principles and Patterns for Computer Systems That Are Simultaneously Secure and Usable, MASSACHUSETTS INSTITUTE OF TECHNOLOGY 2005. Google ScholarDigital Library
- Common Criteria 2006 Common Criteria for information technology security evaluation (CC v3·1), http://www.commoncriteriaportal.org/. Link visited July 2007.Google Scholar
- BevierWR, HuntWA, Moore J SYoungWD1989 An approach to systems verification. J. Automated.Google Scholar
- Elkaduwe D, Derrin P, Elphinstone K 2007 A memory allocation model for an embedded microkernel. In: Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, NICTA, Sydney, Australia 28--34Google Scholar
- Wheeler 2001: David A. Wheeler, Counting Source Lines of Code (SLOC), (Self) 2001, http://www.dwheeler.com/sloc/.Google Scholar
- CC 2006: BSI et al., Common Criteria, CCP 2006, http://www.commoncriteriaportal.org/.Google Scholar
- Infoworld 2004: Joris Evers: Microsoft revisits NGSCB security plan. IDG News Service 2004, http://www.infoworld.com/article/04/05/05/HNngsc_1Google Scholar
- Liedtke 1996: Jochen Liedtke, L4 Reference Manual, GMD/IBM Watson 1996, http://os.inf.tu-dresden.de/L4/14refx86.ps.gzGoogle Scholar
- Tews 2000: Hendrik Tews, Case study in coalgebraic specification: Memory management in the Fiasco microkernel, TU Dresden 2000, http://wwwtcs.inf.tudresdende/~tews/vfiasco/vfiasco-report.ps.gz.Google Scholar
- Härtig 2002: Hermann Härtig, Security architectures revisited, TU Dresden 2002, http://os.inf.tu-dresden.de/papers_ps/secarch.pdf.Google Scholar
- Greve D, Wilding M, Vanfleet W M 2003 A separation kernel formal security policy. In: Fourth International Workshop on the ACL2 Prover and its Applications (ACL2-2003). Available from http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding-vanfleet/security-policy.pdf.Google Scholar
- Hohmuth M, Tews H 2005 The VFiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOPWorkshop on Programming Languages and Operating Systems, Glasgow, UK. Available from http://wwwtcs.inf.tu-dresden/de/tews/Plos-2005/ecoop-plos-05-a4.ps.Google Scholar
- Hohmuth M, Tews H, Stephens S G 2002a Applying source-code verification to a microkernel: the VFiasco project. In: G Muller, E Jul, (eds), Proceedings of the 10th Workshop, (New York, NY, USA: ACM) 165--169. Google ScholarDigital Library
- Hohmuth M, Tews H, Stephens S G 2002b Applying source-code verification to a microkernel: the VFiasco project, Technical Report TUD-FI02-03-ärz 2002, Technische Universiät Dresden, Dresden, Germany.Google Scholar
- Greve D, Wilding M, Vanfleet W M 2005 High assurance formal security policy modeling. In: Proceedings of the 17th Systems and Software Technology Conference 2005 (SSTC05).Google Scholar
- Elphinstone K, Klein G, Kolanski R 2006 Formalising a high-performance microkernel. In: R Leino, ed., Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Microsoft Research Technical Report MSR-TR-2006-117, Seattle, USA 1--7.Google Scholar
- NICTA: Gernot Heiser, Kevin Elphinstone, Michael von Tessin, http://ertos.nicta.com.au/research/se14/.Google Scholar
- MACH 1997: School of Computer Science: CMU CS Project Mach Home Page. Carnegie Mellon University 1997, http://www-2.cs.cmu.edu/afs/cs/project/mach/public.Google Scholar
- Shrink to fit verifiction: Heiko Blume http://kbs.cs.tu-berlin.de/teaching/ws2005/htos/folien/sec_mkernel.pdf.Google Scholar
Index Terms
- Measures to improve security in a microkernel operating system
Recommendations
Comprehensive formal verification of an OS microkernel
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel.
We discuss the kernel design we used to make its verification tractable. We then describe the functional ...
Power-Efficient microkernel of embedded operating system on chip
ACSAC'06: Proceedings of the 11th Asia-Pacific conference on Advances in Computer Systems ArchitectureBecause the absence of hardware support, almost all of embedded operating system are based on SDRAM in past time. With progress of embedded system hardware, embedded system can provide more substrative supports for embedded operating systems. In this ...
Research on Microkernel-based Power Dedicated Secure Operating System
AbstractIndustrial security situation is increasingly serious; operating system security is an important basis for the entire information security. In the industrial security systems, industrial control terminal at the operating system level, lack of a ...
Comments