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

DOI10.1145/1596550.1596566MaRDI QIDQ2936807zbMATH OpenOpenAlexWikidataFDO

Authors Gerwin Klein, Philip Derrin, Kevin Elphinstone

Publication date 6 January 2015

Published in Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1596550.1596566

zbMATH Keywords

HaskellIsabelle/HOLmicrokernelseL4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Secure Microkernels, State Monads and Scalable Refinement
• From a proven correct microkernel to trustworthy large systems
• Operating system verification---an overview
• seL4 enforces integrity
• Theorem Proving in Higher Order Logics

Cited in

(9)

• seL4
• A principled approach to operating system construction in Haskell
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• From a proven correct microkernel to trustworthy large systems
• seL4 enforces integrity
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• Secure Microkernels, State Monads and Scalable Refinement
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Balancing the load. Leveraging a semantics stack for systems verification

Describes a project that uses

Uses Software

• Isabelle/HOL
• Haskell

This page was built for publication: Experience report: seL4, formally verifying a high-performance microkernel

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2936807)