Specification and verification of the ASOS kernel

The Army Secure Operating System (ASOS) program is providing a family of operating systems for tactical data system applications in Ada. Two members of the ASOS family have been developed: a dedicated secure operating system intended for the TCSEC (the DoD Trusted Computer System Evaluation Criteria) C2 level, and a multilevel secure operating system intended for the TCSEC A1 level. An overview is presented of the A1 system concept and TRW´s solution to the ASOS kernel verification problem. A description is given of the model, the formal top-level specification :(FTLS), and proof approaches as well as some practical techniques for coping with proof complexity. Summary statistics on the actual proofs have been compiled and included in the discussion of the verification results