Symbol security condition considered harmful

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