A software engineering approach to designing trustworthy software

Some specific formal techniques that have proven useful in the SMMS design are examined. Attention is given to a simplified example derived from experience with the actual design. The formal techniques examined incorporate the use of a formal security model, formal specifications of module interfaces, and proofs of correspondence between the two. The use of a proof-driven design approach ensured that: (1) security design proceeded in an orderly fashion; (2) the system has high security assurance; (3) security flaws were exposed early in the design; (4) the system is more amenable to change; and (5) specific security responsibilities are traceable to individual components of the system