Concerned with the unprivileged: user programs in kernel refinement

DOI10.1007/S00165-014-0296-9MaRDI QIDQ736848zbMATH OpenOpenAlexFDO

Authors Matthias Daum, Nelson Billing, Gerwin Klein

Publication date 5 August 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-014-0296-9

zbMATH Keywords

microkernel correctnessrefinement prooftrustworthy systems

Mathematics Subject Classification ID

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

Recommendations

• seL4 enforces integrity
• Secure Microkernels, State Monads and Scalable Refinement
• A Unified Memory Model for Pointers
• From a proven correct microkernel to trustworthy large systems
• Theorem Proving in Higher Order Logics

Cites work

• A Unified Memory Model for Pointers
• Compositional verification of a baby virtual memory manager
• Data Refinement
• Logic for Programming, Artificial Intelligence, and Reasoning
• Noninterference for operating system kernels
• Operating system verification---an overview
• Secure Microkernels, State Monads and Scalable Refinement
• Types, Maps and Separation Logic
• seL4 enforces integrity

Cited in

(3)

• Formal reasoning under cached address translation
• seL4 enforces integrity
• Secure Microkernels, State Monads and Scalable Refinement

Describes a project that uses

Uses Software

• seL4
• VCC
• Isabelle/HOL

This page was built for publication: Concerned with the unprivileged: user programs in kernel refinement

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