Multics Security Kernel Validation: Proof Description. Volume I,
Abstract
A major step in the design of a system intended to support multilevel operation is the demonstration that the design is secure. One methodology for demonstrating security is to define (model) a security policy and mathematically verify that the design adheres to that policy. The first step in the design process, after the model, is a rigorous but abstract specification of the system. This paper was written to demonstrate the security of the top level specification for Multics security kernel. Security is demonstrated by a rigorous proof that the abstract specifications correspond to the model. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1978
- Accession Number
- ADA056901
Entities
People
- D. K. Kallman
- S. R. Ames
Organizations
- MITRE Corporation