The author identifies. interprets, and examines the requirements in the Department of Defense trusted computer system evaluation criteria (TCSEC) for the application of formal methods to the system design. The requirements are placed in their historical context to trace their origin. The TCSEC is found to have eliminated some widely-accepted, and critical, security assurance and analysis processes from its trust requirements. It is concluded that despite the flaws and omissions that occur in the published TCSEC, formal design verification is still of some potential value. However, use should not be considered to be an end in itself and may be harmful if applied as such.>

Problems associated with the application of the connectivity approach to computer system security are addressed. The failure of trusted connectivity to protect computer systems is indicated. The work is presented in the form of a humorous allegory.

It has been a tenet of the computer security research and development community that policy enforcement mechanisms must be designed into systems at the time of their conception rather than retrofitted on to existing systems. The paper examines what it means for an architecture to be extensible with respect to security. Results are shown of an examination of the Trusted Computer System Evaluation Criteria's requirements in order to try to make a clear distinction based on how "fundamental" each is to the design and implementation of systems in the individual evaluation classes. We note that, given strict hierarchical layering in a system, along with a strict integrity policy mechanism such as the ring mechanism, it should be possible to extend a system through the addition of new adjacent domains.