Secure Microkernels, State Monads and Scalable Refinement

DOI10.1007/978-3-540-71067-7_16MaRDI QIDQ3543657zbMATH OpenOpenAlexFDO

Authors David Cock, Gerwin Klein, Thomas D. Sewell

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_16

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Experience report: seL4, formally verifying a high-performance microkernel
• From a proven correct microkernel to trustworthy large systems
• seL4 enforces integrity
• Concerned with the unprivileged: user programs in kernel refinement
• Formal verification of monad transformers

Cites work

• A principled approach to operating system construction in Haskell
• Data Refinement
• Guarded commands, nondeterminacy and formal derivation of programs
• Specification and verification of the UCLA Unix security kernel
• The logic of demand in Haskell
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Types, bytes, and separation logic

Cited in

(18)

• Operating system verification---an overview
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Eisbach: a proof method language for Isabelle
• A principled approach to operating system construction in Haskell
• Experience report: seL4, formally verifying a high-performance microkernel
• From a proven correct microkernel to trustworthy large systems
• seL4 enforces integrity
• A Hoare Logic for the State Monad
• A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
• A monadic analysis of information flow security with mutable state
• Cogent: uniqueness types and certifying compilation
• Verifying distributed systems: the operational approach
• A verified specification of TLSF memory management allocator using state monads
• SSCalc: a calculus for Solidity smart contracts
• Type safety for Isabelle/Solidity
• Concerned with the unprivileged: user programs in kernel refinement
• Proving fairness and implementation correctness of a microkernel scheduler

Describes a project that uses

Uses Software

• Haskell
• Isabelle/HOL
• Kit

This page was built for publication: Secure Microkernels, State Monads and Scalable Refinement

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