seL4 enforces integrity

DOI10.1007/978-3-642-22863-6_24MaRDI QIDQ3088017zbMATH OpenOpenAlexFDO

Authors Thomas D. Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, Gerwin Klein

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_24

Mathematics Subject Classification ID

Recommendations

• From a proven correct microkernel to trustworthy large systems
• Noninterference for operating system kernels
• Concerned with the unprivileged: user programs in kernel refinement
• Experience report: seL4, formally verifying a high-performance microkernel
• Secure Microkernels, State Monads and Scalable Refinement

Cites work

• A Linear Time Algorithm for Deciding Subject Security
• Operating system verification---an overview
• Programming semantics for multiprogrammed computations
• Secure Microkernels, State Monads and Scalable Refinement
• Specification and verification of the UCLA Unix security kernel

Cited in

(9)

• Creating high confidence in a separation kernel
• System-level non-interference of constant-time cryptography. I: Model
• Experience report: seL4, formally verifying a high-performance microkernel
• Machine assisted proof of ARMv7 instruction level isolation properties
• From a proven correct microkernel to trustworthy large systems
• Secure Microkernels, State Monads and Scalable Refinement
• Noninterference for operating system kernels
• Concerned with the unprivileged: user programs in kernel refinement
• Using formal reasoning on a model of tasks for FreeRTOS

Describes a project that uses

Uses Software

• HOL
• seL4
• Isabelle
• Isabelle/HOL

This page was built for publication: seL4 enforces integrity

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