Library FOREWORD This Guidelines for

Found at: 0x1bi.net:70/textfiles/file?hacking/COLORBOOKS/purple.txt

Library No.  S-231,308
This publication, Guidelines for Formal Verification Systems, is issued by 
the National Computer Security Center (NCSC) under the authority and in 
accordance with Department of Defense (DoD) Directive 5215.1, "Computer 
Security Evaluation Center."  The guidelines defined in this document are 
ntended for vendors building formal specification and verification
Evaluation Criteria (TCSEC), DoD 5200.28-STD, and the Trusted Network 
As the Director, National Computer Security Center, I invite your
Security Center, 9800 Savage Road, Fort George G.  Meade, MD, 20755-6000,
Attention: Chief, Technical Guidelines Division.
				1 April 1989 
National Computer Security Center
The National Computer Security Center expresses appreciation to Barbara 
Mayer and Monica McGill Lu as principal authors and project managers of 
this document.  We recognize their contribution to the technical content 
and presentation of this publication.
We thank the many individuals who contributed to the concept, development, 
and review of this document.  In particular, we acknowledge:  Karen 
Ambrosi, Tom Ambrosi, Terry Benzel, David Gibson, Sandra Goldston, Dale 
Johnson, Richard Kemmerer, Carl Landwehr, Carol Lane, John McLean, 
Jonathan Millen, Andrew Moore, Michele Pittelli, Marvin Schaefer, Michael 
Sebring, Jeffrey Thomas, Tom Vander-Vlis, Alan Whitehurst, James Williams, 
Kimberly Wilson, and Mark Woodcock.  Additionally, we thank the 
verification system developers and the rest of the verification community 
	1.1 PURPOSE	1
	1.3 SCOPE	2
	3.2.1 Specification Language	9
	3.2.2 Specification Processing	10
	3.2.3 Reasoning Mechanism	11
	4.1 FEATURES	15
	4.1.1 User Interface	15
	4.1.2 Hardware Support	16
	4.2.1 Configuration Management	17
	4.2.2 Support and Maintenance	19
	4.2.3 Testing	19
One of the goals of the NCSC is to encourage the development of 
Although there are manual methodologies for performing formal 
Throughout the document, the term developer is used to describe the 
the individual(s) who are providing support for the tool.  These 
ndividuals may or may not be the same for a particular tool.
The principal goal of the National Computer Security Center (NCSC) is to 
encourage the widespread availability of trusted computer systems.  In 
(TCSEC) was created, against which computer systems could be evaluated.  
The TCSEC was originally published on 15 August 1983 as CSC-STD-001-83.  
DoD 5200.28-STD. [1]
	  1.1		PURPOSE  
This document explains the requirements for formal verification systems 
that are candidates for the NCSC's Endorsed Tools List (ETL). [5]  This 
use in the development of production-quality formal verification systems.  
verification systems submitted to the NCSC for endorsement.
	  1.2		BACKGROUND  
The requirement for NCSC endorsement of verification systems is stated in 
the TCSEC and the Trusted Network Interpretation of the TCSEC (TNI). [4]  
The TCSEC and TNI are the standards used for evaluating security controls 
built into automated information and network systems, respectively.  The 
TCSEC and TNI classify levels of trust for computer and network systems by 
trusted class defined is A1, Verified Design, which requires formal design 
. . verification evidence shall be consistent with that provided within 
the state of the art of the particular Computer Security Center-endorsed 
formal specification and verification system used." [1]
Guidelines were not available when the NCSC first considered endorsing 
verification systems.  The NCSC based its initial endorsement of 
verification systems on support and maintenance of the system, acceptance 
	  1.3		SCOPE  
Any verification system that has the capability for formally specifying 
and verifying the design of a trusted system to meet the TCSEC and TNI A1 
Design Specification and Verification requirement can be considered for 
capabilities beyond design verification are highly encouraged by the NCSC, 
this guideline focuses mainly on those aspects of verification systems 
that are sufficient for the design of candidate A1 systems.
The requirements described in this document are the primary consideration 
n the endorsement process.  They are categorized as either methodology
and system specification or implementation and other support factors.  
Within each category are requirements for features, assurances, and 
The requirements cover those characteristics that can and should exist in 
current verification technology for production-quality systems.  A 
user-friendly, efficient, robust, well documented, maintainable, developed 
verification technology to production quality, while still encouraging the 
advancement of research in the verification field.
Since the NCSC is limited in resources for both evaluation and support of 
verification systems, the ETL may reflect this limitation.  Verification 
capability that the currently endorsed systems lack.
This guideline was written to help in identifying the current needs in 
verification systems and to encourage future growth of verification 
technology.  The evaluation process is described in the following section. 
 Verification systems will be evaluated against the requirements listed in 
next-generation verification systems.  It is not an all-encompassing list 
of features as this would be counterproductive to the goals of research.
A formal request for evaluation of a verification system for placement on 
the ETL shall be submitted in writing directly to:
				National Computer Security Center
				ATTN:		Deputy 
C	(Verification Committee Chairperson)
				9800 Savage Road
				Fort George G. Meade, MD 20755-6000
Submitting a verification system does not guarantee NCSC evaluation or 
The developers shall submit a copy of the verification system to the NCSC 
along with supporting documentation and tools, test suites, configuration 
management evidence, and source code.  In addition, the system developers 
available to answer questions, provide training, and meet with the 
evaluation team.
There are three cases in which an evaluation can occur:  1) the evaluation 
of a new verification system being considered for placement on the ETL, 2) 
the reevaluation of a new version of a system already on the ETL for 
ETL (reevaluation for removal).
To be considered for initial placement on the ETL, the candidate endorsed 
tool must provide some significant feature or improvement that is not 
available in any of the currently endorsed tools.  If the verification 
verification system, concentrating on the requirements described in 
Chapters 3 and 4 of this document.  If a requirement is not completely 
The team shall determine if the deficiency is substantial or detrimental.  
For example, a poor user interface would not be as significant as the lack 
of a justification of the methodology.  Requirements not completely 
Studies or prior evaluations (e.g., the Verification Assessment Study 
Final Report) [2] performed on the verification system shall be reviewed.  
Strengths and weaknesses identified in other reports shall be considered 
The following are the major steps leading to an endorsement and ETL 
listing for a new verification system.
		1)	The developer submits a request for evaluation to 
the NCSC Verification Committee Chairperson.
		2)	The Committee meets to determine whether the 
verification system provides a significant improvement to systems already 
on the ETL or provides a useful approach or capability that the existing 
		3)	If the result is favorable, an evaluation team is 
formed and the verification system evaluation begins.
		4)	Upon completion of the evaluation, a Technical 
Assessment Report (TAR) is written by the evaluation team.
		5)	The Committee reviews the TAR and makes 
		6)	The Committee Chairperson approves or disapproves 
		7)	If approved, an ETL entry is issued for the 
verification system.
		8)	A TAR is issued for the verification system.
The term reevaluation for endorsement denotes the evaluation of a new 
version of an endorsed system for placement on the ETL.  A significant 
number of changes or enhancements, as determined by the developer, may 
the original endorsed version.  
A verification system that is already on the ETL maintains assurance of 
The documentation of this process is evidence for the reevaluation of the 
verification system.  Reevaluations are based upon an assessment of all 
evidence and a presentation of this material by the vendor to the NCSC.  
The NCSC reserves the right to request additional evidence as necessary.
The vendor shall prepare the summary of evidence in the form of a Vendor 
Report (VR).  The vendor may submit the VR to the NCSC at any time after 
all changes have ended for the version in question.  The VR shall relate 
the reevaluation evidence at a level of detail equivalent to the TAR.  The 
VR shall assert that assurance has been upheld and shall include 
the verification system since the endorsed version.  
The Committee shall expect the vendor to present a thorough technical 
overview of changes to the verification system and an analysis of the 
changes, demonstrating continuity and retention of assurance.  The 
Committee subsequently issues a rec*ommendation to the Committee 
Chairperson stating that assurance has or has not been maintained by the 
current verification system since it was endorsed.  If the verification 
option for another review by the Committee.  The reevaluation cycle ends 
ETL, replacing the previously endorsed version; the old version is then 
The following are the major steps leading to an endorsement and ETL 
listing for a revised verification system.
		1)	The vendor submits the VR and other materials to 
the NCSC Verification Committee Chairperson.
		2)	An evaluation team is formed to review the VR.
		3)	The team adds any additional comments and submits 
them to the Verification Committee.
		4)	The vendor defends the VR before the Committee.
		5)	The Committee makes recommendations on endorsement.
		6)	The Committee Chairperson approves or disapproves 
		7)	If approved, a new ETL entry is issued for the 
		8)	The VR is issued for the revised verification 
Once a verification system is endorsed, it shall normally remain on the 
ETL as long as it is supported and is not replaced by another system.  The 
Committee makes the final decision on removal of a verification system 
from the ETL.  For example, too many bugs, lack of users, elimination of 
Committee makes a formal announcement and provides a written justification 
of their decision.  
Systems on the ETL that are removed or replaced shall be archived.  
Systems developers that have a Memorandum of Agreement (MOA) with the NCSC 
to use a verification system that is later archived may continue using the 
evaluations for use in satisfying the A1 Design Specification and 
Verification requirement.
The following are the major steps leading to the removal of a verification 
		1)	The Verification Committee questions the 
endorsement of a verification system on the ETL.
		2)	An evaluation team is formed and the verification 
		3)	Upon completion of the evaluation, a TAR is 
		4)	The Committee reviews the TAR and makes 
		5)	The Committee Chairperson approves or disapproves 
		6)	If removed, a new ETL is issued eliminating the 
verification system in question.
		7)	A TAR is issued for the verification system under 
Currently, verification systems are not production quality tools and are 
frequently being enhanced and corrected.  The version of a verification 
version.  Modified versions are known as beta tool versions.  Beta 
versions are useful in helping system developers uncover bugs before 
The goal of beta versions is to stabilize the verification system.  Users 
endorsed by the NCSC.  If the developer of a trusted system is using a 
beta version of a formal verification system, specifications and proof 
evidence shall be submitted to the NCSC which can be completely checked 
A1 requirement.  This can be accomplished by using either the currently 
endorsed version of a verification system or a previously endorsed version 
that was agreed upon by the trusted system developer and the developer's 
evaluation team.  Submitted specifications and proof evidence that are not 
compatible with the endorsed or agreed-upon version of the tool may 
The technical factors listed in this Chapter are useful measures of the 
quality and completeness of a verification system.  The factors are 
and 4) documentation.  Methodology is the underlying principles and rules 
of organization of the verification system.  Features include the 
functionality of the verification system.  Assurance is the confidence and 
level of trust that can be placed in the verification system.  
Documentation consists of a set of manuals and technical papers that fully 
and maintenance.
These categories extend across each of the components of the verification 
	a)	a mathematical specification language that allows the user 
to express correctness conditions,
	b)	a specification processor that interprets the 
mechanism, and 
	c)	a reasoning mechanism that interprets the conjectures 
correctness conditions are satisfied.
The methodology of the verification system shall consist of a set of 
endorsement of the system.
	  3.2		FEATURES  
		   3.2.1	Specification Language   
		a.	Language expressiveness.
		The specification language shall be sufficiently 
expressive to support the methodology of the verification system.  This 
ensures that the specification language is powerful and rich enough to 
machines, then the specification language must semantically and 
as state machines.  
		b.	Defined constructs.
		The specification language shall consist of a set of 
constructs that are rigorously defined (e.g., in Backus-Naur Form with 
appropriate semantic definitions).  This implies that the language is 
formally described by a set of rules for correct use.
		c.	Mnemonics.
		The syntax of the specification language shall be clear 
and concise without obscuring the interpretation of the language 
constructs.  Traditional symbols from mathematics should be employed 
cases.  This aids the users in interpreting constructs more readily.
		d.	Internal uniformity.
		The syntax of the specification language shall be 
nternally uniform.  This ensures that the rules of the specification
language are not contradictory.
		e.	Overloading.
		Each terminal symbol of the specification language's 
ncreases comprehensibility.  When it is beneficial to incorporate more
than one definition for a symbol or construct, the semantics of the 
construct shall be clearly defined from the context used.  This is 
necessary to avoid confusion by having one construct with more than one 
nterpretation or more than one construct with the same interpretation.
For example, the symbol "+" may be used for both integer and real 
addition, but it should not be used to denote both integer addition and 
		f.	Correctness conditions.
		The specification language shall provide the capability to 
express correctness conditions.
		g.	Incremental verification.
		The methodology shall allow incremental verification.  
This would allow, for example, a verification of portions of a system 
the capability for performing verification of different levels of 
abstraction.  This allows essential elements to be presented in the most 
abstract level and important details to be presented at successive levels 
of refinement.
		   3.2.2	Specification Processing   
		a.	Input.
		All of the constructs of the specification language shall 
be processible by the specification processor(s).  This is necessary to 
convert the specifications to a language or form that is interpretable by 
the reasoning mechanism.
		b.	Output.
		The output from the processor(s) shall be interpretable by 
the reasoning mechanism.  Conjectures derived from the correctness 
conditions shall be generated.  The output shall also report errors in 
		   3.2.3	Reasoning Mechanism   
		a.	Compatibility of components.
		The reasoning mechanism shall be compatible with the other 
components of the verification system to ensure that the mechanism is 
capable of determining the validity of conjectures produced by other 
components of the verification system.  For example, if conjectures are 
		b.	Compatibility of constructs.
		The well-formed formulas in the specification language 
that may also be input either directly or indirectly into the reasoning 
mechanism using the language(s) of the reasoning mechanism shall be 
mappable to ensure compatibility of components.  For example, if a lemma 
can be defined in the specification language as "LEMMA 
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 
		c.	Documentation.
		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.
		d.	Reprocessing.
		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 
		e.	Validation.
		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.
		f.	Reusability.
		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 
	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 
verification system.
	b.	Correctness.
	The verification system shall be rigorously tested to provide 
assurance that the majority of the system is free of error.
	c.	Predictability.
	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.
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 
and maintenance.
	  4.1		FEATURES  
		   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.  
		d.	Compatibility.
		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 
		e.	Functionality.
		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   
		a.	Availability.
		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 
verification system.
		b.	Efficiency.
		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		ASSURANCE  
		   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.  
		   4.2.3	Testing   
		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 
verification system.  
		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 
of each.
		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 
verification system.
	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 
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 
formally verified.
	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 
verification system.
Additional information on configuration management can be found in A Guide 
to Understanding Configuration Management in Trusted Systems. [3]
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.
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.  
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 Version 
		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.
Configuration Accounting 
		The recording and reporting of configuration item 
Configuration Audit 
		An independent review of computer software for the purpose 
of assessing compliance with established requirements, standards, and 
baselines. [3]
Configuration Control 
		The process of controlling modifications to the system's 
of improper modification prior to, during, and after system 
mplementation. [3]
Configuration Control Board (CCB) 
		An established vendor committee that is the final 
authority on all proposed changes to the verification system.
Configuration Identification 
		The identifying of the system configuration throughout the 
Configuration Item (CI) 
		The smallest component tracked by the configuration 
management system. [3]
Configuration Management 
		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.
Consistency (Mathematical) 
		A logical theory is consistent if it contains no formula 
Consistency (Methodological)
		Steadfast adherence to the same principles, course, form, 
		Free from errors; conforming to fact or truth.
Correctness Conditions 
		Conjectures that formalize the rules, security policies, 
models, or other critical requirements on a system.
Design Verification 
		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 
Formal Justification 
		Mathematically precise evidence that the methodology of 
the verification system is sound.
Formal Verification 
		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. [1]
Implementation Verification 
		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 
verification system.
		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). [2]
		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.
Reasoning Mechanism 
		A tool (interactive or fully automated) capable of 
checking or constructing proofs.
Safety Properties 
		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.
Specification Language 
		A logically precise language used to describe the 
Specification Processor 
		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 
Verification Committee 
		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.
Verification System 
		An integrated set of tools and techniques for performing 
Well-Formed Formula 
		A sequence of symbols from a language that is constructed 
n accordance with the syntax for that language.
[1]		Department of Defense, Department of Defense Trusted 
Computer System Evaluation Criteria, DOD 5200.28-STD, December 1985.  
[2]		Kemmerer, Richard A., Verification Assessment Study Final 
Report, University of California, March 1986.
[3]		National Computer Security Center, A Guide to 
Understanding Configuration Management in Trusted Systems, NCSC-TG-006, 
March 1988.
[4]		National Computer Security Center, Trusted Network 
NCSC-TG-005, July 1987.
[5]		National Security Agency, Information Systems Security