Secure Ada Target: Issues, System Design, and Verification

The Secure Ada Target (SAT) machine is designed to meet or exceed the DoD requirements for multi-level secure systems. This paper describes the require-ments on such designs, our approach to meeting these requirements by introducing tagged objects, and a specialized tagged object processor (TOP) that handles all operations involving tagged objects. Basic system security is achieved using a small software kernel and the TOP. The structure of our proofs, such that the system satisfies appropriate security properties, will be outlined. Brief remarks concerning the implementation of user Ada programs on the SAT system conclude the paper. Our design approach is largely independent of CPU selection, though implementation details necessarily depend on the processor selection.