seL4 Enforces Integrity

DOI10.1007/978-3-642-22863-6_24zbMath1342.68303OpenAlexW51058944MaRDI QIDQ3088017

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

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

Related Items (3)

System-level non-interference of constant-time cryptography. I: Model ⋮ Using formal reasoning on a model of tasks for FreeRTOS ⋮ Concerned with the unprivileged: user programs in kernel refinement

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• seL4

Cites Work

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

This page was built for publication: seL4 Enforces Integrity