NCJ Number
57607
Date Published
1978
Length
38 pages
Annotation
VOLUME ONE OF A TWO-VOLUME REPORT DISCUSSED THE SECURITY OF A TOP-LEVEL SPECIFICATION FOR A MULTICS SECURITY KERNEL, THIS VOLUME IS AN INTRODUCTION TO THE PROOF METHODOLOGY.
Abstract
A MAJOR STEP IN THE TECHNICAL CERTIFICATION OF A SYSTEM INTENDED TO SUPPORT MULTILEVEL OPERATION IS THE DEMONSTRATION THAT THE DESIGN IS SECURE. TO DEMONSTRATE THIS FOR THE TOP-LEVEL SPECIFICATION FOR MULTICS SECURITY KERNEL, A SECURITY POLICY IS DEFINED (MODEL) AND THE DESIGN IS MATHEMATICALLY VALIDATED TO SHOW ITS ADHERENCE TO THE SECURITY POLICY. THE PROOF METHODOLOGY INCLUDES: (1) A FORMAL DESCRIPTION OF THE DEPARTMENT OF DEFENSE SECURITY POLICY IN TERMS OF A MATHEMATICAL MODEL, (2) A COMPLETE DESCRIPTION OF THE KERNEL BEHAVIOR THAT IS PROVED CONSISTENT WITH THE MODEL, AND (3) A PROOF THAT THE KERNEL IS CORRECTLY IMPLEMENTED WITH RESPECT TO THE DESCRIPTION OF ITS BEHAVIOR USED IN THE SECOND STEP. IN DESCRIBING THE PROOF, IT IS NOTED THAT THE VALIDATION OF NONDISCRETIONARY SECURITY REQUIRES PROVING THAT CERTAIN AXIOMS ARE PRESERVED BY EACH O-FUNCTION IN THE SPECIFICATION. THESE AXIOMS ARE THE SIMPLE SECURITY CONDITION, THE PROPERTY, AND THE ACTIVITY, TRANQUILITY, AND ERASURE PRINCIPLES. THE PROOF OF EACH OF THESE AXIOMS IS DISCUSSED, WHICH INCLUDES: (1) EXPRESSING EACH AXIOM IN TERMS OF THE ABSTRACT MODEL ENTITIES, (2) AN INTERPRETATION OF THE AXIOM IN TERMS OF THE SPECIFICATION ENTITIES (O-FUNCTIONS, V-FUNCTIONS, AND OV-FUNCTIONS), AND (3) SHOWING HOW THE INTERPRETATION IS PROVEN. THE TREATMENT OF TRUSTED SUBJECTS IS ALSO DESCRIBED. SEVERAL TOP-LEVEL VALIDATIONS THAT HAVE BEEN PERFORMED ARE COMPARED, FOLLOWED BY A DISCUSSION OF OPEN ISSUES IN THE PROOF METHODOLOGY. THE ACTUAL PROOF IS CONTAINED IN THE APPENDIXES OF VOLUME II. (RCB)