A model of security is presented which integrates notions of confidentiality and integrity. This model has been developed to fulfil the needs of the RSRE SMITE project because existing modeling approaches proved to be inadequate. The authors introduce the model and subsequently compare and contrast it with existing approaches. Both an inductive confidentiality property and a noninductive integrity property have been modeled. To successfully utilize the second property, the authors have used an approach whereby the noninductiveness is absent in the model, but appears in proof obligations on refinement.>

If signaling channels can only be driven by a trusted path, they cannot be exploited by trojan horses in untrusted software. To this end, the SMITE secure computer system provides a general-purpose trusted path, based on a screen editor, which would act as the users' normal interface to the system. The feasibility of the approach relies on the use of a sympathetic computer architecture, which supports a fine grain of protection. The authors describe the trusted path and the user interface of the SMITE system. They discuss the formal specification of the display functions. They examine the use of SMITE for high-assurance applications.>