[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/1596550.1596566acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

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

Published: 31 August 2009 Publication History

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)
MP4 File (experiencereportsel4formallyverifyingahigh-performance.mp4)

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.

Cited By

View all
  • (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
  • (2022)Formal Verification of a KeystoreTheoretical Aspects of Software Engineering10.1007/978-3-031-10363-6_4(49-64)Online publication date: 2022
  • (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
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming
August 2009
364 pages
ISBN:9781605583327
DOI:10.1145/1596550
  • cover image ACM SIGPLAN Notices
    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
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Isabelle/HOL
  2. haskell
  3. microkernel
  4. seL4

Qualifiers

  • Research-article

Conference

ICFP '09
Sponsor:
ICFP '09: ACM SIGPLAN International Conference on Functional Programming
August 31 - September 2, 2009
Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)14
  • Downloads (Last 6 weeks)1
Reflects downloads up to 25 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (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
  • (2022)Formal Verification of a KeystoreTheoretical Aspects of Software Engineering10.1007/978-3-031-10363-6_4(49-64)Online publication date: 2022
  • (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
  • (2018)Porting the Pip Proto-Kernel's Model to Multi-core Environments2018 IEEE 16th Intl Conf on Dependable, Autonomic and Secure Computing, 16th Intl Conf on Pervasive Intelligence and Computing, 4th Intl Conf on Big Data Intelligence and Computing and Cyber Science and Technology Congress(DASC/PiCom/DataCom/CyberSciTech)10.1109/DASC/PiCom/DataCom/CyberSciTec.2018.00108(584-591)Online publication date: Aug-2018
  • (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
  • (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
  • (2016)Testing noninterference, quicklyJournal of Functional Programming10.1017/S095679681600005826Online publication date: 5-Apr-2016
  • (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
  • (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
  • (2014)Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems10.1145/256053732:1(1-70)Online publication date: 26-Feb-2014
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media