From a proven correct microkernel to trustworthy large systems

DOI10.1007/978-3-642-18070-5_1MaRDI QIDQ3067529zbMATH OpenOpenAlexFDO

Authors June Andronick

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18070-5_1

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• seL4 enforces integrity
• Experience report: seL4, formally verifying a high-performance microkernel
• Secure Microkernels, State Monads and Scalable Refinement
• Theorem Proving in Higher Order Logics
• Noninterference for operating system kernels

Cites work

• Isabelle/HOL. A proof assistant for higher-order logic
• Programming semantics for multiprogrammed computations
• Types, bytes, and separation logic

Cited in

(14)

• Operating system verification---an overview
• Toward compositional verification of interruptible OS kernels and device drivers
• Creating high confidence in a separation kernel
• Safe functional systems through integrity types and verified assembly
• Experience report: seL4, formally verifying a high-performance microkernel
• Policy-centric protection of OS kernel from vulnerable loadable kernel modules
• seL4 enforces integrity
• Secure Microkernels, State Monads and Scalable Refinement
• Noninterference for operating system kernels
• Theorem Proving in Higher Order Logics
• Towards applying the composition principle to verify a microkernel operating system
• Refinement-based specification and analysis of multi-core ARINC 653 using Event-B
• 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

• Isabelle/HOL
• seL4

This page was built for publication: From a proven correct microkernel to trustworthy large systems

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