A methodology for demonstrating the security of trusted applications on a security kernel base is presented. The methodology consists of selecting and authenticating security criteria, and demonstrating through verification techniques that the implementation obeys the selected criteria. Difficulties encountered in the placement of a trusted application on top of a security kernel base motivated the development of the methodology.

Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.