A description of a formal verification and validation (FVV) process

The Department of Defense Trusted Computer System Evaluation Criteria (TCSEC) establishes a requirement for formal verification activities of a TCB (trusted computer base) designed for mandatory of verified protection. The goal of formal verification is to prove that the design specification of a system is consistent with its security policy. The authors elaborate the principles of the formal verification process. They discuss the inputs needed, processing performed, outputs produced, and analysis involved. In addition, they examine the resources required and present some observations in the form of cautions