formula>" and can also be defined in the reasoning mechanism, then the
construct for the lemma in the reasoning mechanism shall be in the same
The reasoning mechanism shall document the steps it takes
to develop the proof. Documentation provides users with a stable,
completed proofs. If the reasoning mechanism is defined to use more than
one method of reasoning, then it should clearly state which method is used
and remain consistent within each method of reasoning.
The reasoning mechanism shall provide a means for
a means of reprocessing theorems without reconstructing the proof process.
This mechanism shall also save the users from reentering voluminous input
to the reasoning mechanism. For example, reprocessing may be accomplished
by the generation of command files that can be invoked to recreate the
The methodology shall provide a means for validating proof
checked by an independent, trustworthy proof checker shall ensure that
only sound proof steps were employed in the proof process. Trustworthy
mplies that there is assurance that the proof checker accepts only valid
always be invoked for each completed proof session.
The reasoning mechanism shall facilitate the use of
This provides a foundation for proof sessions that will save the user time
and resources in reproving similar theorems and lemmas.
g. Proof dependencies.
The reasoning mechanism shall track the status of the use
and reuse of theorems throughout all phases of development. Proof
are made to a specification (and indirectly to any related
conjectures/theorems), the minimal set of theorems and lemmas that are
3.3 ASSURANCE, SOUNDNESS, AND ROBUSTNESS
a. Sound basis.
Each of the verification system's tools and services shall support
the method*ology. This ensures that users can understand the
functionality of the verification system with respect to the methodology
and that the methodology is supported by the components of the
The verification system shall be rigorously tested to provide
assurance that the majority of the system is free of error.
The verification system shall behave predictably. Consistent
This will ensure faster and easier interpretation and fewer errors in
d. Previous use.
The verification system shall have a history of use to establish
the developers). These applications shall test the verification system,
e. Error recovery.
The verification system shall gracefully recover from internal
n the verification system do not cause damage to a user session.
f. Software engineering.
The verification system shall be implemented using documented
maintainability and configuration management.
g. Logical theory.
All logical theories used in the verification system shall be
metalogic. This provides the users with a sound method of interaction
among the theories.
h. Machine independence.
The functioning of the methodology and the language of the
verification system shall be machine independent. This is to ensure that
the functioning of the theory, specification language, reasoning mechanism
and other essential features does not change from one machine to another.
Additionally, the responses that the user receives from each of the
components of the verification system should be consistent across the
a. Informal justification.
An informal justification of the methodology behind the
verification system shall be provided. All parts of the methodology must
be fully documented to serve as a medium for validating the accuracy of
the stated implementation of the verification system. The logical theory
used in the verification system shall be documented. If more than one
logical theory exists in the system, the metalogic employed in the system
for the evaluators and will aid the users in understanding the methodology.
b. Formal definition.
A formal definition (e.g., denotational semantics) of the
nclude a clear semantic definition of the expressions supported by the
and will aid the users in understanding the specification language.
c. Explanation of methodology.
A description of how to use the methodology, its tools, its
limitations, and the kinds of properties that it can verify shall be
methodology and to use the verification system effectively.
4. IMPLEMENTATION AND OTHER SUPPORT FACTORS
The NCSC considers the support factors listed in this section to be
measures of the usefulness, understandability, and maintainability of the
verification system. The support factors are divided into the following
three categories: 1) features, 2) assurances, and 3) documentation.
Two features that provide support for the user are the interface and the
base hardware of the verification system. Configuration management,
testing, and mainte*nance are three means of providing assurance. (The
Appendix contains additional information on configuration management.)
Documentation consists of a set of manuals and technical papers that fully
4.1.1 User Interface
a. Ease of use.
The interface for the verification system shall be
user-friendly. Input must be understandable, output must be informative,
and the entire interface must support the users' goals.
b. Understandable input.
Input shall be distinct and concise for each language
construct and ade*quately represent what the system requires for the
c. Understandable output.
Output from the components of the verification system
that users are provided with understandable and helpful information.
Output from the screen, the processor, and the reasoning
mechanism shall be compatible with their respective input, where
appropriate. It is reasonable for a specification processor (reasoning
mechanism) to put assertions into a canonical form, but canonical forms
The interface shall support the tasks required by the user
to exercise the verification system effectively. This is to ensure that
all commands necessary to utilize the components of the methodology are
available and functioning according to accompanying documentation.
f. Error reporting.
The verification system shall detect, report, and recover
from errors in a specification. Error reporting shall remain consistent
by having the same error message generated each time the error identified
n the message is encountered. The output must be informative and
nterpretable by the users.
4.1.2 Hardware Support
The verification system shall be available on commonly
used computer systems. This will help ensure that users need not purchase
expensive or outdated machines, or software packages to run the
Processing efficiency and memory usage shall be reasonable
for specifications of substantial size. This ensures that users are able
to process simple (no complex constructs), short (no more than two or
three pages) specifications in a reasonable amount of time (a few
minutes). The processing time of larger, more complex specifications
time for feedback.
4.2.1 Configuration Management
a. Life-cycle maintenance.
Configuration management tools and procedures shall be
used to track changes (both bug fixes and new features) to the
verification system from initial concept to final implementation. This
tracking the numerous changes made to the verification system to ensure
that only sound changes are implemented.
b. Configuration items.
Identification of Configuration Items (CIs) shall begin
early in the design stage. CIs are readily established on a logical basis
at this time. The configuration management process shall allow for the
c. Configuration management tools.
Tools shall exist for comparing a newly generated version
ntended changes have been made in the code that will actually be used as
the new version of the verification system, and b) no additional changes
the system developer. The tools used to perform these functions shall
also be under strict configuration control.
d. Configuration control.
Configuration control shall cover a broad range of items
ncluding software, documentation, design data, source code, the running
version of the object code, and tests. Configuration control shall begin
n the earliest stages of design and development and extend over the full
life of the CIs. It involves not only the approval of changes and their
mplementation but also the updat*ing of all related material to reflect
each change. For example, often a change to one area of a verification
addition or change. Changes to all CIs shall be subject to review and
The configuration control process begins with the
and to ensure against duplicate change requests being processed.
e. Configuration accounting.
Configuration accounting shall yield information that can
be used to answer the following questions: What source code changes were
made on a given date? Was a given change absolutely necessary? Why or
N+1? By whom were they made, and why? What other modifications were
test set or documentation to accommodate any of these changes? What were
all the changes made to support a given change request?
f. Configuration auditing.
A configuration auditor shall be able to trace a system
change from start to finish. The auditor shall check that only approved
changes have been implemented, and that all tests and documentation have
been updated concurrently with each implementation to reflect the current
g. Configuration control board.
The vendor's Configuration Control Board (CCB) shall be
approved modifications, and verifying that changes are properly
ncorporated. The members of the CCB shall interact periodically to
configuration status accounting reports, and other topics that may be of
nterest to the different areas of the system development.
4.2.2 Support and Maintenance
The verification system shall have ongoing support and maintenance from
the developers or another qualified vendor. Skilled maintainers are
necessary to make changes to the verification system.
a. Functional tests.
Functional tests shall be conducted to demonstrate that
the verification system operates as advertised. These tests shall be
maintained over the life cycle of the verification system. This ensures
that a test suite is available for use on all versions of the verification
dentified to demonstrate the elimination of the errors in subsequent
versions. Tests shall be done at the module level to demonstrate
compliance with design documentation and at the system level to
mplements the logic, and correctly responds to user commands.
b. Stress testing.
The system shall undergo stress testing by the evaluation
team to test the limits of and to attempt to generate contradictions in
the specification language, the reasoning mechanism, and large
a. Configuration management plan.
A configuration management plan and supporting evidence assuring a
consistent mapping of documentation and tools shall be provided for the
evaluation. This provides the evaluators with evidence that compatibility
exists between the components of the verification system and its
1. The configuration management plan shall describe
verification system. It shall define the roles and responsibilities of
all of the personnel involved with any part of the life cycle of the
2. Tools used for configuration management shall be
change control, conventions for labeling configuration items, etc., shall
be contained in the configuration management plan along with a description
3. The plan shall describe procedures for how the
and approved or disapproved. The configuration management plan shall also
nclude the steps to ensure that only those approved changes are actually
ncluded and that the changes are included in all of the necessary areas.
4. The configuration management plan shall describe
changes without going through a full review process. These procedures
management after the emergency change has been completed.
b. Configuration management evidence.
Documentation of the configuration management activities shall be
configuration management plan have been followed.
c. Source code.
Well-documented source code for the verification system, as well
as documentation to aid in analysis of the code during the evaluation,
d. Test documentation.
Documentation of test suites and test procedures used to check
functionality of the system shall be provided. This provides an
explanation to the evaluators of each test case, the testing methodology,
test results, and procedures for using the tests.
e. User's guide.
An accurate and complete user's guide containing all available
commands and their usage shall be provided in a tutorial format. The
user's guide shall contain worked examples. This is necessary to guide
the users in the use of the verification system.
f. Reference manuals.
A reference manual that contains instructions, error messages, and
examples of how to use the system shall be provided. This provides the
users with a guide for problem-solving techniques as well as answers to
questions that may arise while using the verification system.
g. Facilities manual.
A description of the major components of the software and their
nterfacing shall be provided. This will provide users with a limited
knowledge of the hardware base required to configure and use the
h. Vendor report.
A report written by the vendor during a reevaluation that provides
a complete description of the verification system and changes made since
the initial evaluation shall be provided. This report, along with
configuration management documentation, provides the evaluators with
evidence that soundness of the system has not been jeopardized.
i. Significant worked examples.
Significant worked examples shall be provided which demonstrate
the strengths, weaknesses, and limitations of the verification system.
These examples shall reflect portions of computing systems. They may
5. FUTURE DIRECTIONS
The purpose of this section is to list possible features for future or
beyond-A1 verification systems. Additionally, it contains possibilities
for future research -- areas that researchers may choose to investigate.
Research and development of new verification systems or investigating
areas not included in this list is also encouraged. Note that the order
n which these items appear has no bearing on their relative importance.
a. The specification language should permit flexibility in
approaches to specification.
b. The specification language should allow the expression of
c. The reasoning mechanism should include a method for
d. The design and code of the verification system should be
e. The theory should support rapid prototyping. Rapid
f. The verification system should make use of standard (or
or printer, use of a standard database support system, etc.).
g. The verification system should provide a language-specific
verifier for a commonly used systems programming language.
h. The verification system should provide a method for
mapping a top-level specification to verified source code.
i. The verification system should provide a tool for
automatic test data generation of the design specification.
j. The verification system should provide a means of
dentifying which paths in the source code of the verification system are
tested by a test suite.
k. The verification system should provide a facility for
l. A formal justification of the methodology behind the
verification system should be provided.
The purpose of configuration management is to ensure that changes made to
verification systems take place in an identifiable and controlled
environment. Configuration managers take responsibility that additions,
ts ability to satisfy the requirements in Chapters 3 and 4. Therefore,
configuration management is vital to maintaining the endorsement of a
Additional information on configuration management can be found in A Guide
to Understanding Configuration Management in Trusted Systems. 
OVERVIEW OF CONFIGURATION MANAGEMENT
Configuration management is a discipline applying technical and
administrative direction to: 1) identify and document the functional and
manage all changes to these characteristics; and 3) record and report the
nvolves 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
Four major aspects of configuration management are configuration
dentification, configuration control, configuration status accounting,
and configuration auditing.
Configuration management entails decomposing the verification system into
dentifi*able, understandable, manageable, trackable units known as
Configuration Items (CIs). A CI is a uniquely identifiable subset of the
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
life of the system, and small CIs for elements likely to change more
Configuration control is a means of assuring that system changes are
approved before being implemented, only the proposed and approved changes
are implemented, and the implementation is complete and accurate. This
nvolves strict procedures for proposing, monitoring, and approving system
changes and their implementation. Configuration control entails central
tasks, approve system changes, review the implementation of changes, and
Configuration accounting documents the status of configuration control
activities and in general provides the information needed to manage a
configuration effectively. It allows managers to trace system changes and
establish the history of any developmental problems and associated fixes.
Configuration accounting also tracks the status of current changes as they
move through the configuration control process. Configuration accounting
establishes the granularity of recorded information and thus shapes the
accuracy and usefulness of the audit function.
The accounting function must be able to locate all possible versions of a
CI and all of the incremental changes involved, thereby deriving the
nclude commentary about the reason for each change and its major
mplications for the verification system.
Configuration audit is the quality assurance component of configuration
management. It involves periodic checks to determine the consistency and
completeness of accounting information and to verify that all
configuration management policies are being followed. A vendor's
configuration management program must be able to sustain a complete
configuration audit by an NCSC review team.
CONFIGURATION MANAGEMENT PLAN
Strict adherence to a comprehensive configuration management plan is one
of the most important requirements for successful configuration
management. The configuration management plan is the vendor's document
tailored to the company's practices and personnel. The plan accurately
evidence is being recorded.
CONFIGURATION CONTROL BOARD
All analytical and design tasks are conducted under the direction of the
vendor's corporate entity called the Configuration Control Board (CCB).
The CCB is headed by a chairperson who is responsible for assuring that
changes made do not jeopardize the soundness of the verification system.
The Chairperson assures that the changes made are approved, tested,
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
Beta versions are intermediate releases of a product to be
tested at one or more customer sites by the software end-user. The
customer describes in detail any problems encountered during testing to
the developer, who makes the appropriate modifications. Beta versions are
not endorsed by the NCSC, but are primarily used for debugging and testing
A theory is complete if and only if every sentence of its
language is either provable or refutable.
Simultaneous or parallel processing of events.
The recording and reporting of configuration item
An independent review of computer software for the purpose
of assessing compliance with established requirements, standards, and
The process of controlling modifications to the system's
of improper modification prior to, during, and after system
Configuration Control Board (CCB)
An established vendor committee that is the final
authority on all proposed changes to the verification system.
The identifying of the system configuration throughout the
Configuration Item (CI)
The smallest component tracked by the configuration
management system. 
The process of controlling modifications to a verification
the system is protected against the introduction of improper modification
before, during, and after system implementation.
A general conclusion proposed to be proved upon the basis
of certain given premises or assumptions.
A logical theory is consistent if it contains no formula
Steadfast adherence to the same principles, course, form,
Free from errors; conforming to fact or truth.
Conjectures that formalize the rules, security policies,
models, or other critical requirements on a system.
A demonstration that a formal specification of a software
A set of manuals and technical papers that fully describe
the verification system, its components, application, and operation.
Endorsed Tools List (ETL)
A list composed of those verification systems currently
The ability to prove that at some time in the future, a
Mathematically precise evidence that the methodology of
the verification system is sound.
The process of using formal proofs to demonstrate the
consistency (design verification) between a formal specification of a
between the formal specification and its program implementation. 
A demonstration that a program implementation satisfies a
formal specification of a system.
An English description of the tools of a verification
A set of symbols and rules of syntax regulating the
Formalizations that ensure that a system does something
that it should do.
A type of logic used to describe another type of logic or
a combination of different types of logic.
The underlying principles and rules of organization of a
A verification system that is sound, user-friendly,
efficient, robust, well-documented, maintainable, well-engineered
(developed with software engineering techniques), available on a variety
of hardware, and promoted (has education available for users). 
A syntactic analysis performed to validate the truth of an
assertion relative to an (assumed) base of assertions.
A tool that 1) accepts as input an assertion (called a
conjecture), a set of assertions (called assumptions), and a proof; 2)
terminates and outputs either success or failure; and 3) if it succeeds,
then the conjecture is a valid consequence of the assumptions.
A tool (interactive or fully automated) capable of
checking or constructing proofs.
Formalizations that ensure that a system does not do
A set of rules for interpreting the symbols and
An argument is sound if all of its propositions are true
and its argument form is valid. A proof system is sound relative to a
consequence of the assumptions used in the proof.
A logically precise language used to describe the
A software tool capable of receiving input, parsing it,
further analysis (e.g., reasoning mechanism).
A set of rules for constructing sequences of symbols from
the primitive symbols of a language.
Technical Assessment Report (TAR)
A report that is written by an evaluation team during an
evaluation of a verification system and available upon completion.
In a given logical system, a well-formed formula that is
A formal theory is a coherent group of general
A system is user-friendly if it facilitates learning and
usage in an efficient manner.
An argument is valid when the conclusion is a valid
consequence of the assumptions used in the argument.
Vendor Report (VR)
A report that is written by a vendor during and available
upon completion of a reevaluation of a verification system.
The process of comparing two levels of system
top-level specification, top-level specification with source code, or
A standing committee responsible for the management of the
verification efforts at the NCSC. The committee is chaired by the NCSC
Deputy Director and includes the NCSC Chief Scientist, as well as
and Office of Computer Security Evaluations, Publications, and Support.
An integrated set of tools and techniques for performing
A sequence of symbols from a language that is constructed
n accordance with the syntax for that language.
 Department of Defense, Department of Defense Trusted
Computer System Evaluation Criteria, DOD 5200.28-STD, December 1985.
 Kemmerer, Richard A., Verification Assessment Study Final
Report, University of California, March 1986.
 National Computer Security Center, A Guide to
Understanding Configuration Management in Trusted Systems, NCSC-TG-006,
 National Computer Security Center, Trusted Network
NCSC-TG-005, July 1987.
 National Security Agency, Information Systems Security