Concerned with the unprivileged: user programs in kernel refinement

DOI10.1007/S00165-014-0296-9zbMATH Open1342.68079OpenAlexW2074245744MaRDI QIDQ736848FDOQ736848

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

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

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)

Cites Work

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

Cited In (3)

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

Uses Software

• Isabelle/HOL
• VCC
• seL4

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)