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

Formal verification tools and techniques are difficult and expensive to apply. To make verification of large, complex systems more practical, TRW is developing the deductive theory manager (DTM). A knowledge-based tool that integrates with the Gypsy verification environment (GVE), the DTM supports the construction of deductive theories and applies them to proofs. Knowledge bases applicable to a variety of projects, and one specific to the army secure operating system (ASOS) proofs, are simultaneously under development. The authors describe the underlying philosophy of the verification strategy on which the DTM is based, present the DTM architecture, and illustrate DTM knowledge engineering and proof processing with a case study.>

A description is given of ASDViews, an implementation of views as the security object in a multilevel secure relational database management system (DBMS) that results in a small trusted computing base (TCB) as required to meet the criteria for evaluation class B2 and above. A general view is the result of a database query. Since most of the code which implements the DBMS is involved in processing the query, most of the DBMS must be trusted. ASDViews is defined using a subset of the relational algebra to restrict the size of the query language available to define a secure view. This approach reduces that part of the TCB required to implement secure views to roughly 1000 lines of code.>