Specification and verification of the UCLA Unix security kernel

DOI10.1145/358818.358825MaRDI QIDQ3863057zbMATH OpenOpenAlexFDO

Authors Bruce J. Walker, Gerald J. Popek, Richard A. Kemmerer

Publication date 1980

Published in Communications of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/358818.358825

zbMATH Keywords

operating systemsprotectionsecurityUnixverification

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Cited in

(5)

• Operating system verification---an overview
• The programming language C and the operating system UNIX
• seL4 enforces integrity
• Secure Microkernels, State Monads and Scalable Refinement
• Formal memory models for the verification of low-level operating-system code

This page was built for publication: Specification and verification of the UCLA Unix security kernel

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