KSOS Kernel Verification Results. Kernelized Secure Operating System

摘要

The original KSOS verification goals were the following: The instantiation of the multilevel security model to SPECIAL; The design and development of a computer tool (the MLS formula generator) whose input would be SPECIAL specifications, and whose output would be conjectures, the proof of which would imply that the specifications do not contaim any violations of the multilevel security model; The proofs that the specifications for the KSOS security perimeter (Kernel and NKSR) conform to the security model. In the event of violations, the proof process should pinpoint the violations so that they may be eliminated or bandwidth-limited; The development of support tools so that illustrative code proofs could be carried out. The goal of these code proofs is to demonstrate the feasibility of performing full code proofs at a later date, and The carrying out of illustrative code proofs. KSOS has succeeded in instantiating the multilevel security model to SPECIAL and developing the MLS formula generator, in producing proofs of the kernel specifications, in producing prototype support tools that could be used in code proofs, in producing a code proof for a version of the SMXflow module, and in producing some mapping functions (manually) showing the correspondence of VFUNS to Modula structures for certain kernel modules.