KSOS Secure Unix Verification Plan (Kernelized Secure Operating System)

摘要

The purpose of this Verification Plan is to state how the Ford Aerospace and Communications Corp. (FACC) and its subcontractor, SRI International, intend to meet the verification requirements of KSOS, the Kernelized Secure Operating System. Also contained in this document are sections on the mathematical model of security policy to be used in KSOS, on the role of the model, on the programming language to be used for system implementation, on the tools to support the effort, and on the role of testing. FACC and SRI intend to use a restatement of the Bell ad LaPadula model as the conceptual basis for the system security. This modification extends the model of Bell and LaPadula, and incorporates their work as a proper subset. The resulting formulation appears to be well suited to proofs of correspondence between the formal specifications and the formal model. In particular, automatic proof is facilitated, using mostly syntactic properties and being based largely on existing tools.