Analysis of a Kemel Verification

This paper reports on the analysis and evaluation of the SCOMP kernel verification. The SCOMP system was developed by Honeywell FSD and is targeted at the Al class of the DoD Trusted Computer System Evaluation Criteria [CSC8S]. It is currently under evaluation by the Department.of Defense Computer Security Center (DoDCSC). The work reported on here is significant in that the SCOMP system is the first commercially-available formally verified operating system. Furthermore, it is the first, system to be evaluated against.the A1 requirements for formal design specification and verification. The methods and procedures used for this analysis and evaluation will be of interest to future system designers, verifiers, and evaluators. The results of the verification, in particular the types of assurances that were gained, will also be discussed.