This report comprises a high level design for a Security Kernel of an operating system which is currently being investigated by the Air Force. This operating system will provide a sophisticated time-sharing mode of operation with a large shared-file environment to a user community comprised of individuals of various clearances. The specifications of the Security Kernel are developed through a series of successively more complex models which are used to specify the system in increasing detail. The first specification defines in general what it means to say that a system is uncompromisable or that there can be no unauthorized disclosure of information. Subsequent models introduce directory structure, interprocess communication, file and process attributes, and other system functions. Using this approach, we can discuss various design issues related to security in an orderly and straightforward manner.