Title :
Specification and verification of the ASOS kernel
Author :
Di Vito, Ben L. ; Palmquist, Paul H. ; Anderson, Eric R. ; Johnston, Michael L.
Author_Institution :
TRW Syst. Integration Group, Redondo Beach, CA, USA
Abstract :
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
Keywords :
formal specification; military computing; operating systems (computers); program verification; ASOS kernel; Ada; Army Secure Operating System; DoD Trusted Computer System Evaluation Criteria; dedicated secure operating system; formal top-level specification; multilevel secure operating system; proof complexity; tactical data system applications; verification; Data security; Data systems; Information security; Kernel; Multilevel systems; Operating systems; Permission; Real time systems; Software performance; Statistics;
Conference_Titel :
Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-2060-9
DOI :
10.1109/RISP.1990.63839
