seL4

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

seL4: formal verification of an OS kernel

Full text

Pdf (977 KB)

Source

ACM Symposium on Operating Systems Principles archive
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles table of contents

Big Sky, Montana, USA

SESSION: Kernals table of contents

Pages 207-220

Year of Publication: 2009

ISBN:978-1-60558-752-3

Authors

Gerwin Klein	NICTA & UNSW, Sydney, Australia
Kevin Elphinstone	NICTA & UNSW, Sydney, Australia
Gernot Heiser	NICTA, UNSW & Open Kernel Labs, Sydney, Australia
June Andronick	NICTA & UNSW, Sydney, Australia
David Cock	NICTA & UNSW, Sydney, Australia
Philip Derrin	NICTA, Sydney, Australia
Dhammika Elkaduwe	NICTA & UNSW, Sydney, Australia
Kai Engelhardt	UNSW & NICTA, Sydney, Australia
Rafal Kolanski	NICTA & UNSW, Sydney, Australia
Michael Norrish	NICTA & ANU, Canberra, Australia
Thomas Sewell	NICTA, Sydney, Australia
Harvey Tuch	NICTA & UNSW, Sydney, Australia
Simon Winwood	NICTA & UNSW, Sydney, Australia

Sponsors

ACM: Association for Computing Machinery
SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 91, Downloads (12 Months): 91, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629575.1629596 What is a DOI?

ABSTRACT

Complete formal verification is the only known way to guarantee that a system is free of programming errors.

We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.

seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	M. Accetta, R. Baron, W. Bolosky, D. Golub, R. Rashid, A. Tevanian, and M. Young. Mach: A new kernel foundation for UNIX development. In 1986 Summer USENIX, pages 93--112, 1986.
	2	E. Alkassar, M. Hillebrand, D. Leinenbach, N. Schirmer, A. Starostin, and A. Tsyban. Balancing the load -- leveraging a semantics stack for systems verification. JAR, 42(2-4), 2009.
	3	E. Alkassar, N. Schirmer, and A. Starostin. Formal pervasive verification of a paging mechanism. In C.R. Ramakrishnan and J. Rehof, editors, Tools and Alg. for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 109--123. Springer, 2008.
	4	J. Alves-Foss, P.W. Oman, C. Taylor, and S. Harrison. The MILS architecture for high-assurance embedded systems. Int. J. Emb. Syst., 2:239--247, 2006.
	5	M. Archer, E. Leonard, and M. Pradella. Analyzing security-enhanced Linux policy specifications. In POLICY '03: Proc. 4th IEEE Int. WS on Policies for Distributed Systems and Networks, pages 158--169. IEEE Computer Society, 2003.
	6	T. Ball and S.K. Rajamani. SLIC: A specification language for interface checking. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
	7	B.N. Bershad, S. Savage, P. Pardyak, E.G. Sirer, M.E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In 15th SOSP, Dec 1995.
	8	W.R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382--1396, 1989.
	9	W.R. Bevier and L. Smith. A mathematical model of the Mach kernel: Atomic actions and locks. Technical Report 89, Computational Logic Inc., Apr 1993.
	10	I.T. Bowman, R.C. Holt, and N.V. Brewster. Linux as a case study: its extracted software architecture. In ICSE '99: Proc. 21st Int. Conf. on Software Engineering, pages 555--563. ACM, 1999.
	11	A. Boyton. A verified shared capability model. In G. Klein, R. Huuck, and B. Schlich, editors, 4th WS Syst. Softw. Verification SSV'09, ENTCS, pages 99--116. Elsevier, Jun 2009.
	12	P. Brinch Hansen. The nucleus of a multiprogramming operating system. CACM, 13:238--250, 1970.
	13	D. Cock. Bitfields and tagged unions in C: Verification through automatic generation. In B. Beckert and G. Klein, editors, VERIFY'08, volume 372 of CEUR Workshop Proceedings, pages 44--55, Aug 2008.
	14	D. Cock, G. Klein, and T. Sewell. Secure microkernels, state monads and scalable refinement. In O.A. Mohamed, C. Mu n oz, and S. Tahar, editors, 21st TPHOLs, volume 5170 of LNCS, pages 167--182. Springer, Aug 2008.
	15	B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M.Y. Vardi. Proving that programs eventually do something good. In 34th POPL. ACM, 2007.
	16	J. Criswell, A. Lenharth, D. Dhurjati, and V. Adve. Secure virtual architecture: A safe execution environment for commodity operating systems. In 16th SOSP, pages 351--366, Oct 2007.
	17	U. Dannowski. Personal communication.
	18	W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
	19	P. Derrin, K. Elphinstone, G. Klein, D. Cock, and M.M.T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In ACM SIGPLAN Haskell WS, Sep 2006.
	20	D. Elkaduwe, P. Derrin, and K. Elphinstone. Kernel design for isolation and assurance of physical memory. In 1st IIES, pages 35--40. ACM SIGOPS, Apr 2008.
	21	D. Elkaduwe, G. Klein, and K. Elphinstone. Verified protection model of the seL4 microkernel. In J. Woodcock and N. Shankar, editors, VSTTE 2008 -- Verified Softw.: Theories, Tools & Experiments, volume 5295 of LNCS, pages 99--114. Springer, Oct 2008.
	22	K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a practical, verified kernel. In 11th HotOS, pages 117--122, May 2007.
	23	M. Faehndrich, M. Aiken, C. Hawblitzel, O. Hodson, G.C. Hunt, J.R. Larus, and S. Levi. Language support for fast and reliable message-based communication in Singularity OS. In 1st EuroSys Conf., pages 177--190, Apr 2006.
	24	R.J. Feiertag and P.G. Neumann. The foundations of a provably secure operating system (PSOS). In AFIPS Conf. Proc., 1979 National Comp. Conf., Jun 1979.
	25	B. Ford, M. Hibler, J. Lepreau, R. McGrath, and P. Tullmann. Interface and execution models in the Fluke kernel. In 3rd OSDI. USENIX, Feb 1999.
	26	T. Garfinkel, B. Pfaff, J. Chow, M. Rosenblum, and D. Boneh. Terra: A virtual machine-based platform for trusted computing. In 19th SOSP, Oct 2003.
	27	Green Hills Software, Inc. INTEGRITY-178B separation kernel security target version 1.0. http://www.niap-ccevs.org/cc-scheme/st/st_vid10119-st.pdf, 2008.
	28	Greenhills Software, Inc. Integrity real-time operating system. http://www.ghs.com/products/rtos/integrity.html, 2008.
	29	J.D. Guttman, A.L. Herzog, J.D. Ramsdell, and C.W. Skorupka. Verifying information flow goals in security-enhanced Linux. Journal of Computer Security, 13(1):115--134, 2005.
	30	J.T. Haigh and W.D. Young. Extending the noninterference version of MLS for SAT. IEEE Trans. on Software Engineering, 13(2):141--150, 1987.
	31	D.S. Hardin, E.W. Smith, and W.D. Young. A robust machine code proof framework for highly secure applications. In ACL2'06: Proc. Int. WS on the ACL2 theorem prover and its applications. ACM, 2006.
	32	G. Heiser. Hypervisors for consumer electronics. In 6th IEEE CCNC, 2009.
	33	C.L. Heitmeyer, M. Archer, E.I. Leonard, and J. McLean. Formal specification and verification of data separation in a separation kernel for an embedded system. In CCS '06: Proc. 13th Conf. on Computer and Communications Security, pages 346--355. ACM, 2006.
	34	T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In SPIN'03, Workshop on Model Checking Software, 2003.
	35	M. Hohmuth, M. Peter, H. Haertig, and J.S. Shapiro. Reducing TCB size by using untrusted components -- small kernels versus virtual-machine monitors. In 11th SIGOPS Eur. WS, Sep 2004.
	36	M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In 2nd PLOS, Jul 2005.
	37	Iguana. http://www.ertos.nicta.com.au/software/kenge/iguana-project/latest/.
	38	Information Assurance Directorate. U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Jun 2007. Version 1.03. http://www.niap--ccevs.org/cc--scheme/pp/pp.cfm/id/pp_skpp_hr_v1.03/.
	39	ISO/IEC. Programming languages -- C. Technical Report 9899:TC2, ISO/IEC JTC1/SC22/WG14, May 2005.
	40	G. Klein. Operating system verification -- an overview. Sadhana, 34(1):27--69, Feb 2009.
	41	G. Klein, P. Derrin, and K. Elphinstone. Experience report: seL4 -- formally verifying a high-performance microkernel. In 14th ICFP, Aug 2009.
	42	R. Kolanski and G. Klein. Types, maps and separation logic. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Proc. TPHOLs'09, volume 5674 of LNCS. Springer, 2009.
	43	L4HQ. http://l4hq.org/arch/arm/.
	44	X. Leroy. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In J.G. Morrisett and S.L.P. Jones, editors, 33rd POPL, pages 42--54. ACM, 2006.
	45	J. Liedtke. Improving IPC by kernel design. In 14th SOSP, pages 175--188, Dec 1993.
	46	J. Liedtke. Towards real microkernels. CACM, 39(9):70--77, Sep 1996.
	47	J. Liedtke, K. Elphinstone, S. Schoenberg, H. Haertig, G. Heiser, N. Islam, and T. Jaeger. Achieved IPC performance (still the foundation for extensibility). In 6th HotOS, pages 28--31, May 1997.
	48	W.B. Martin, P. White, A. Goldberg, and F.S. Taylor. Formal construction of the mathematically analyzed separation kernel. In ASE '00: Proc. 15th IEEE Int. Conf. on Automated software engineering, pages 133--141. IEEE Computer Society, 2000.
	49	Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic system code: Machine context management. In Proc. TPHOLs'07, volume 4732 of LNCS, pages 189--206. Springer, Sep 2007.
	50	T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
	51	OKL4 web site. http://okl4.org.
	52	T. Perrine, J. Codd, and B. Hardy. An overview of the kernelized secure operating system (KSOS). In Proceedings of the Seventh DoD/NBS Computer Security Initiative Conference, pages 146--160, Sep 1984.
	53	Rockwell Collins, Inc. AAMP7r1 Reference Manual, 2003.
	54	J.M. Rushby. Design and verification of secure systems. In 8th SOSP, pages 12--21, 1981.
	55	O. Saydjari, J. Beckman, and J. Leaman. Locking computers securely. In 10th National Computer Security Conference, pages 129--141, Sep 1987.
	56	A. Seshadri, M. Luk, N. Qu, and A. Perrig. SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes. In 16th SOSP, pages 335--350, Oct 2007.
	57	J.S. Shapiro, D.F. Faber, and J.M. Smith. State caching in the EROS kernel--implementing efficient orthogonal peristence in a pure capability system. In 5th IWOOOS, pages 89--100, Nov 1996.
	58	J.S. Shapiro, J.M. Smith, and D.J. Farber. EROS: A fast capability system. In 17th SOSP, Dec 1999.
	59	L. Singaravelu, C. Pu, H. Haertig, and C. Helmuth. Reducing TCB complexity for security-sensitive applications: Three case studies. In 1st EuroSys Conf., pages 161--174, Apr 2006.
	60	R. Spencer, S. Smalley, P. Loscocco, M. Hibler, D. Andersen, and J. Lepreau. The Flask security architecture: System support for diverse security policies. In 8th USENIX Security Symp., Aug 1999.
	61	H. Tews, T. Weber, and M. Voelp. A formal model of memory peculiarities for the verification of low-level operating-system code. In R. Huuck, G. Klein, and B. Schlich, editors, Proc. 3rd Int. WS on Systems Software Verification (SSV'08), volume 217 of ENTCS, pages 79--96. Elsevier, Feb 2008.
	62	H. Tuch. Formal Memory Models for Verifying C Systems Code. PhD thesis, UNSW, Aug 2008.
	63	H. Tuch. Formal verification of C systems code: Structured types, separation logic and theorem proving. JAR, 42(2-4):125--187, 2009.
	64	H. Tuch, G. Klein, and G. Heiser. OS verification -- now! In 10th HotOS, pages 7--12. USENIX, Jun 2005.
	65	H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In M. Hofmann and M. Felleisen, editors, 34th POPL, pages 97--108, Jan 2007.
	66	US National Institute of Standards. Common Criteria for IT Security Evaluation, 1999. ISO Standard 15408. http://csrc.nist.gov/cc/.
	67	B.J. Walker, R.A. Kemmerer, and G.J. Popek. Specification and verification of the UCLA Unix security kernel. CACM, 23(2):118--131, 1980.
	68	D.A. Wheeler. SLOCCount. http://www.dwheeler.com/sloccount/, 2001.
	69	A. Whitaker, M. Shaw, and S. D. Gribble. Scale and performance in the Denali isolation kernel. In 5th OSDI, Dec 2002.
	70	S. Winwood, G. Klein, T. Sewell, J. Andronick, D. Cock, and M. Norrish. Mind the gap: A verification framework for low-level C. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Proc. TPHOLs'09, volume 5674. Springer, 2009.
	71	W. Wulf, E. Cohen, W. Corwin, A. Jones, R. Levin, C. Pierson, and F. Pollack. HYDRA: The kernel of a multiprocessor operating system. CACM, 17:337--345, 1974.