Experience report

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Experience report: seL4: formally verifying a high-performance microkernel

Full text

Pdf (432 KB)

Source

International Conference on Functional Programming archive
Proceedings of the 14th ACM SIGPLAN international conference on Functional programming table of contents

Edinburgh, Scotland

SESSION: Session 4 table of contents

Pages 91-96

Year of Publication: 2009

ISBN:978-1-60558-332-7

Also published in ...

Authors

Gerwin Klein	NICTA & UNSW, Sydney, Australia
Philip Derrin	NICTA, Sydney, Australia
Kevin Elphinstone	NICTA & UNSW, Sydney, Australia

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 28, Downloads (12 Months): 128, 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/1596550.1596566 What is a DOI?

ABSTRACT

We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. The kernel comprises 8,700 lines of C code; the verification more than 150,000 lines of proof script.

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	D. Cock. Bitfields and tagged unions in C: Verification through automatic generation. In B. Beckert and G. Klein, editors, Proceedings of the 5th International VerificationWorkshop (VERIFY'08), volume 372 of CEUR Workshop Proceedings, pages 44--55, Sydney, Australia, Aug 2008.
	2	D. Cock, G. Klein, and T. Sewell. Secure microkernels, state monads and scalable refinement. In O. A. Mohamed, C. MuÜnoz, and S. Tahar, editors, 21st TPHOLs, volume 5170 of LNCS, pages 167--182, Montreal, Canada, Aug 2008. Springer.
	3	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, Portland, OR, USA, Sep 2006.
	4	D. Elkaduwe, G. Klein, and K. Elphinstone. Verified protection model of the seL4 microkernel. In J. Woodcock and N. Shankar, editors, VSTTE 2008 2008 -- Verified Softw.: Theories, Tools & Experiments, volume 5295 of LNCS, pages 99--114, Toronto, Canada, 2008. Springer.
	5	K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a practical, verified kernel. In 11th HotOS, pages 117--122, 2007.
	6	G. Klein. Operating system verification - an overview. Sadhana, 34(1): 27--69, Feb 2009.
	7	J. Liedtke. On ¼-kernel construction. In 15th SOSP, pages 237--250, Copper Mountain, CO, USA, Dec 1995.
	8	T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
	9	Open Kernel Labs. OKL4 v2.1. http://www.ok-labs.com, 2008.
	10	H. Tuch, G. Klein, and G. Heiser. OS verification - now! In 10th HotOS, pages 7--12, Santa Fe, NM, USA, Jun 2005. USENIX.
	11	H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In M. Hofmann and M. Felleisen, editors, 34th POPL, pages 97--108, 2007.
	12	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. 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), volume 5674 of LNCS. Springer, 2009. To appear.