Accession Number:

ADA056901

Title:

Multics Security Kernel Validation: Proof Description. Volume I,

Descriptive Note:

Corporate Author:

MITRE CORP BEDFORD MASS

Personal Author(s):

• Ames ,S. R.
• Kallman,D. K.

Report Date:

1978-07-01

Pagination or Media Count:

38.0

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

Descriptors:

• *DATA PROCESSING SECURITY
• *COMPUTER COMMUNICATIONS
• *SECURE COMMUNICATIONS
• MATHEMATICAL MODELS
• SYSTEMS ENGINEERING
• SPECIFICATIONS
• KERNEL FUNCTIONS
• ERROR ANALYSIS
• SYSTEMS ANALYSIS
• COMPUTER PROGRAM VERIFICATION
• MULTIPLE OPERATION
• MULTIPLE ACCESS

Subject Categories:

• Computer Programming and Software
• Non-Radio Communications

Distribution Statement:

APPROVED FOR PUBLIC RELEASE