Guidelines for Formal Verification Systems

Front Cover
National Computer Security Center, 1989 - Computer programs - 35 pages
"This document explains the requirements for formal verification systems that are candidates for the NCSC's Endorsed Tools List (ETL). This document is primarily intended for developers of verification systems to use in the development of production-quality formal verification systems. It explains the requirements and the process used to evaluate formal verification systems submitted to the NCSC for endorsement."--DTIC.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Selected pages

Other editions - View all

Common terms and phrases

Popular passages

Page 33 - Verification - The process of comparing two levels of system specification for proper correspondence (eg, security policy model with top-level specification, TLS with source code, or source code with object code). This process may or may not be automated. Write - A fundamental operation that results only in the flow of information from a subject to an object.
Page 27 - ... that the changes made are approved, tested, documented, and implemented correctly. The members of the CCB should interact periodically, either through formal meetings or other available means, to discuss configuration management topics such as proposed changes, configuration status accounting reports, and other topics that may be of interest to the different areas of the system development. These interactions should be held to keep the entire system team updated on all advancements or alterations...
Page 30 - Specification that is written in a formal mathematical language to allow theorems showing the correspondence of the system specification to its formal requirements to be hypothesized and formally proven. Formal verification — the process of using formal proofs to demonstrate the consistency (design verification) between a formal specification of a system and a formal security policy model or (implementation verification) between the formal specification and its program implementation.
Page 28 - The concept of holding sensitive data in confidence, limited to an appropriate set of individuals or organizations. configuration control The process of controlling modifications to the system's hardware, firmware, software, and documentation that provides sufficient assurance that the system is protected against the introduction of improper modifications prior to, during, and after system implementation. Compare configuration management.
Page 18 - ... for the system and should be subject to the identification, control, accounting, and audit functions of configuration management. "Initial phases of configuration control are directed towards control of the system configuration as defined primarily in design documents. Often a change to one area of a system may necessitate a change to another area. It is not acceptable to only write documentation for new code or newly modified code, but rather documentation for all parts of the TCB that were...
Page 25 - Configuration management involves process monitoring, version control, information capture, quality control, bookkeeping, and an organizational framework to support these activities. The configuration being managed is the verification system plus all tools and documentation related to the configuration process. Four major aspects of configuration management are configuration identification, configuration control, configuration status accounting, and configuration auditing. CONFIGURATION IDENTIFICATION...
Page 26 - CI is a uniquely identifiable subset of the system that represents the smallest portion to be subject to independent configuration control procedures. The decomposition process of a verification system into CIs is called configuration identification. CIs can vary widely in size, type, and complexity. Although there are no hard-and-fast rules for decomposition, the granularity of CIs can have great practical importance. A favorable strategy is to designate relatively large CIs for elements that are...
Page i - National Computer Security Center 9800 Savage Road Fort George G. Meade, MD 20755-6000 Attention: Chief, Technical Guidelines Division 30 September 1987 Director National Computer Security Center "Thi.
Page 33 - a coherent group of general propositions used as principles of explanation for a class of phenomena
Page 17 - Also available shall be tools, maintained under strict configuration control, for comparing a newly generated version with the previous TCB version in order to ascertain that only the intended changes have been made in the code that will actually be used as the new version of the TCB.

Bibliographic information