In order to be affordable and satisfy user requirements, today's secure systems must be constructed out of trusted and untrusted components. A framework for designing secure system architectures has been developed. Four general-purpose secure architectures were designed, and one of them was validated on the secure system integration IR&D. This work and what has been learned about secure architectures and their implementation using commercial-off-the-shelf (COTS) secure products are described.>

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.>

This paper addresses some of the criticisms that have been leveled against Ada's stdtabillty for use in trusted computer systems. It treats the use of Ada for both untrusted applications programs and security kernel implementation. (It does not directly address the use of Ada for other trusted software, but much of what is said about its use for security kernels applies to trusted software as well.) The paper concludes that each Ada criticism is either unfounded or poses a problem that has a solution; thus, Ada is Indeed suitable for trusted computer system implementation.