The experimental secure distributed operating system (SDOS) is described. It uses a composable property as its mandatory security policy. The security policy includes a fine granularity of discretionary access control immune to Trojan horse attacks. The high degree of assurance that composability makes practical and the richness of the discretionary controls lead SDOS to use balanced assurance. In balance assurance, the assurance measures are fitted to the portion of the security policy whose enforcement is being assured. Like the Cronus distributed computing environment from which it is derived, SDOS uses an object model with abstract operations on various types of system objects and permits an application to extend the paradigm to new types of application objects with new operations. The SDOS security policy and enforcement can likewise be extended for an application's security policy and enforcement.>

Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a specification written in SPECIAL (the specification language of HDM). In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center A1 evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process. In concept, it is open-ended. We introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality.

Muse is a verification system which extends the collection of tools developed by SRI for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a SPECIAL specification. In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center Al evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process.

The formal verification performed by SYTEK as part of the development and security assurance of NASA's Restricted Access Processor (RAP) represents important progress toward the verification of medium-scale and large-scale systems in the real world. It is interesting primarily because it was large, rigorous and meaningful and was successfully completed within its original budget. The experience helps show what can really be done with reasonable resources to verify the security properties of fairly complex systems. The RAP can be added to the short list of formally verified systems. Its successes and blind alleys provide lessons for those considering verification of the security of other systems, and the statistics of the RAP verification effort provide a data point for those interested in the practicality of formal techniques.