SECURITY KERNEL VERIFICATION TECHNIQUES - ALGORITHMIC REPRESENTATION

• NCJ Number: 57869
• Author(s): D K KALLMAN; J K MILLEN
• Date Published: 1978
• Length: 39 pages
• Contract Number(s): F19628-77-C-0001
• Sponsoring Agency: US Dept of the Air Force
• Corporate Author: Mitre Corporation
• Sale Source: National Technical Information Service
• Language: English
• Country: United States of America

Annotation

PROCEDURES FOR MINIMIZING THREATS TO COMPUTERS BY CONSTRUCTING AN ALGORITHMIC OR PROGRAMING LANGUAGE FOR A SECURITY KERNEL, A MECHANISM THAT ENFORCES ACCESS CONTROLS TO INFORMATION, ARE REPORTED.

Abstract

SECURITY THREATS TO COMPUTERS INCLUDE PHYSICAL DAMAGE, EAVESDROPPING, AND MISBEHAVIOR ON THE PART OF PERSONNEL WITH LEGITIMATE ACCESS TO COMPUTER SYSTEM SERVICES AND INFORMATION. AVAILABLE FEATURES OF A COMPUTER FOR DATA PROTECTION DETERMINE WHETHER AN EFFICIENT REFERENCE MONITOR CAN BE IMPLEMENTED. THE BOUNDARY BETWEEN HARDWARE AND SOFTWARE RESPONSIBILITIES IN THE IMPLEMENTATION OF A REFERENCE MONITOR IS HARDWARE-DEPENDENT. STAGES OF A SECURITY KERNEL, PROPOSED AS A REFERENCE MONITOR, PROGRESS FROM MODELING, FORMAL SPECIFICATION, AND ALGORITHMIC REPRESENTATION TO THE COMPUTER ITSELF. A MAJOR POINT OF CONCERN IN VERIFYING THE CORRESPONDENCE OF KERNEL DESIGN TO A MODEL FOR THE PROTECTION OF DATA IS WHETHER ALL REPOSITORIES OF INFORMATION HAVE BEEN IDENTIFIED. ALGORITHMIC REPRESENTATON IS A PROGRAMING LANGUAGE VERSION OF A KERNEL. PROPOSED STEPS IN CONSTRUCTING A SECURE ALGORITHMIC REPRESENTATON ARE TO PROVE THAT UPPER-LEVEL SPECIFICATION IS SECURE; TO DESIGN LOWER LEVELS OF SPECIFICATION; TO WRITE ABSTRACT PROGRAMS TO IMPLEMENT EACH FUNCTION IN THE NEXT LOWER LEVEL, FOR EACH LEVEL OF SPECIFICATION EXCEPT THE LOWEST; TO PROVE THAT EACH LEVEL IS BEHAVIORALLY IMPLEMENTED BY THE NEXT LOWER LEVEL; TO PROVE THAT THE SPECIFIC INITIAL STATE CHOSEN FOR A KERNEL SATISFIES THE RELATIONS; TO WRITE AND VERIFY FUNCTION SUBPROGRAMS TO CALCULATE VALUES OF HIGH-LEVEL STATE VARIABLES IN ABSTRACT PROGRAMS; AND TO DEVISE AN ALGORITHMIC REPRESENTATION OF A KERNEL USING THE SET OF ALL ABSTRACT PROGRAMS AND SUBPROGRAMS. A METHOD OF BEHAVIORAL EQUIVALENCE AMONG LEVELS IN COMPUTER SYSTEMS IS DETAILED WHEN COMPUTERS HAVE THE SAME SET OF INPUTS AND WHEN A LOWER-LEVEL COMPUTER HAS A MORE PRIMITIVE SET OF INPUTS THAN A HIGHER-LEVEL COMPUTER. THE IMPLEMENTATION OF ABSTRACT PROGRAMS TO TRANSLATE UPPER-LEVEL INPUTS INTO A SEQUENCE OF LOWER-LEVEL INPUTS IS DETAILED. ILLUSTRATIONS, ALGORITHMIC REPRESENTATIONS, AND REFERENCES ARE PROVIDED. (DEP)