research-article

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

Authors:

Gerwin Klein,

Philip Derrin,

Kevin ElphinstoneAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 9

Pages 91 - 96

https://doi.org/10.1145/1631687.1596566

Published: 31 August 2009 Publication History

Get Access

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.

Supplementary Material

JPG File (experiencereportsel4formallyverifyingahigh-performance.jpg)

Download
17.60 KB

MP4 File (experiencereportsel4formallyverifyingahigh-performance.mp4)

Download
88.48 MB

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.

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[5]

K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a practical, verified kernel. In 11th HotOS, pages 117--122, 2007.

Digital Library

Google Scholar

[6]

G. Klein. Operating system verification - an overview. Sadhana, 34(1): 27--69, Feb 2009.

Crossref

Google Scholar

[7]

J. Liedtke. On ¼-kernel construction. In 15th SOSP, pages 237--250, Copper Mountain, CO, USA, Dec 1995.

Digital Library

Google Scholar

[8]

T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

Google Scholar

[9]

Open Kernel Labs. OKL4 v2.1. http://www.ok-labs.com, 2008.

Google Scholar

[10]

H. Tuch, G. Klein, and G. Heiser. OS verification - now! In 10th HotOS, pages 7--12, Santa Fe, NM, USA, Jun 2005. USENIX.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

Cited By

View all

Roggenbach MSchlingloff BSchneider GRoggenbach MCerone ASchlingloff BSchneider GShaikh S(2022)Formal MethodsFormal Methods for Software Engineering10.1007/978-3-030-38800-3_1(1-46)Online publication date: 23-Jun-2022
https://doi.org/10.1007/978-3-030-38800-3_1
Sabraoui MHieb JLauf AGraham J(2019)Modeling and Machine-Checking Bump-in-the-Wire Security for Industrial Control SystemsCritical Infrastructure Protection XIII10.1007/978-3-030-34647-8_14(271-288)Online publication date: 19-Nov-2019
https://doi.org/10.1007/978-3-030-34647-8_14
Madhavan RKulal SKuncak V(2017)Contract-based resource verification for higher-order functions with memoizationACM SIGPLAN Notices10.1145/3093333.300987452:1(330-343)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009874
Show More Cited By

Index Terms

Recommendations

seL4: formal verification of an OS kernel
SOSP '09: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles

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 ...
Experience report: seL4: formally verifying a high-performance microkernel
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

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 ...
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 ...

Reviews

Reviewer: Wolfgang Schreiner

The formal verification of computer software is not confined to toy programs anymore. It has reached a state where it is applicable to real-life applications. This experience report witnesses this evolution, by demonstrating an approach to the verification of an operating system microkernel-in fact, to the whole process of specifying, implementing, and verifying such a piece of software. The process starts with the development of a rapid prototype, in a subset of the functional programming language Haskell, which was automatically translated into the language of the theorem prover Isabelle/HOL. From this executable specification, a verification team constructed an abstract specification, in which the intended correctness properties could be expressed and verified. The main effort was to develop a refinement proof that insures that the executable specification also satisfies these properties. At the same time, an implementation team constructed a high-performance C implementation from the executable specification, verifying the correspondence of these two levels in a second refinement proof. In the course of this process-that took 20 person-years-the Haskell prototype was repeatedly modified, due to insights gained from the efforts of both teams. The paper presents numerous interesting insights into the process of designing, implementing, and verifying a realistic piece of software, and how these activities go hand in hand. Unfortunately, little is said about the actual correctness properties of the microkernel and their verification (these details are described in a separate publication). Nevertheless, the paper nicely demonstrates how the development of safety-critical software should or might proceed in the future. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 44, Issue 9

ICFP '09

September 2009

343 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1631687

Issue’s Table of Contents

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming
August 2009
364 pages
ISBN:9781605583327
DOI:10.1145/1596550
General Chair:
Graham Hutton
University of Nottingham
,
Program Chair:
Andrew Tolmach
Portland State University

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Published in SIGPLAN Volume 44, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
850
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Roggenbach MSchlingloff BSchneider GRoggenbach MCerone ASchlingloff BSchneider GShaikh S(2022)Formal MethodsFormal Methods for Software Engineering10.1007/978-3-030-38800-3_1(1-46)Online publication date: 23-Jun-2022
https://doi.org/10.1007/978-3-030-38800-3_1
Sabraoui MHieb JLauf AGraham J(2019)Modeling and Machine-Checking Bump-in-the-Wire Security for Industrial Control SystemsCritical Infrastructure Protection XIII10.1007/978-3-030-34647-8_14(271-288)Online publication date: 19-Nov-2019
https://doi.org/10.1007/978-3-030-34647-8_14
Madhavan RKulal SKuncak V(2017)Contract-based resource verification for higher-order functions with memoizationACM SIGPLAN Notices10.1145/3093333.300987452:1(330-343)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009874
Madhavan RKulal SKuncak VCastagna GGordon A(2017)Contract-based resource verification for higher-order functions with memoizationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009874(330-343)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009874
Koromilas LVasiliadis GAthanasopoulos EIoannidis S(2016)GRIM: Leveraging GPUs for Kernel Integrity MonitoringResearch in Attacks, Intrusions, and Defenses10.1007/978-3-319-45719-2_1(3-23)Online publication date: 7-Sep-2016
https://doi.org/10.1007/978-3-319-45719-2_1
Wang XMizuno MNeilsen MOu XRajagopalan SBoldwin WPhillips BRay IThomas RCardenas A(2015)Secure RTOS Architecture for Building AutomationProceedings of the First ACM Workshop on Cyber-Physical Systems-Security and/or PrivaCy10.1145/2808705.2808709(79-90)Online publication date: 16-Oct-2015
https://dl.acm.org/doi/10.1145/2808705.2808709
Alkhammash EButler MFathabadi ACîrstea C(2015)Building traceable Event-B models from requirementsScience of Computer Programming10.1016/j.scico.2015.06.002111:P2(318-338)Online publication date: 1-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.06.002
Siapoush MAlves-Foss J(2023)Is Formal Verification of seL4 Adequate to Address the Key Security Challenges of Kernel Design?IEEE Access10.1109/ACCESS.2023.331603111(101750-101759)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3316031
Boender JBadevic G(2022)Formal Verification of a KeystoreTheoretical Aspects of Software Engineering10.1007/978-3-031-10363-6_4(49-64)Online publication date: 2022
https://doi.org/10.1007/978-3-031-10363-6_4
Qian ZLiu WYao Y(2021)Verification of Operating Systems for Internet of Things in Smart Cities From the Assembly Perspective Using Isabelle/HOLIEEE Access10.1109/ACCESS.2020.30474119(2854-2863)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2020.3047411
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

Supplementary Material

References

Cited By

Index Terms

Recommendations

seL4: formal verification of an OS kernel