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

Author

Smith, Bill ; Reese, Cynthia ; Lindsay, Kenneth ; Crane, Brian

Author_Institution

Magnavox Electron. Syst. Co., Ashburn, VA, USA

fYear

1988

fDate

12-16 Dec 1988

Firstpage

401

Lastpage

408

Abstract

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

Keywords

formal specification; program verification; security of data; TCSEC; Trusted Computer System Evaluation Criteria; design specification; formal validation; formal verification; hierarchical development methodology; multi-level security tool; security policy; theorem prover; trusted computer base; verified protection; Cranes; Data analysis; Design engineering; Failure analysis; Formal verification; Information security; Mathematical model; Performance analysis; Protection; Software design;

fLanguage

English

Publisher

ieee

Conference_Titel

Aerospace Computer Security Applications Conference, 1988., Fourth

Conference_Location

Orlando, FL

Print_ISBN

0-8186-0895-1

Type

conf

DOI

10.1109/ACSAC.1988.113339

Filename

113339