Library FOREWORD This Guidelines for

NCSC-TG-014-89

Library No.  S-231,308

 FOREWORD 

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 

Director 

National Computer Security Center

			ACKNOWLEDGMENTS 

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 

TABLE OF CONTENTS

FOREWORD	i

ACKNOWLEDGMENTS	ii

	1.1 PURPOSE	1

	1.2 BACKGROUND	1

	1.3 SCOPE	2

	2.1 EVALUATION OF NEW SYSTEMS	3

	2.2 REEVALUATION FOR ENDORSEMENT	5

	2.3 REEVALUATION FOR REMOVAL	6

	2.4 BETA VERSIONS	7

	3.1 METHODOLOGY	8

	3.2 FEATURES	9

	3.2.1 Specification Language	9

	3.2.2 Specification Processing	10

	3.2.3 Reasoning Mechanism	11

	3.3 ASSURANCE, SOUNDNESS, AND ROBUSTNESS 	12

	3.4 DOCUMENTATION	14

	4.1 FEATURES	15

	4.1.1 User Interface	15

	4.1.2 Hardware Support	16

	4.2 ASSURANCE	17

	4.2.1 Configuration Management	17

	4.2.2 Support and Maintenance	19

	4.2.3 Testing	19

	4.3 DOCUMENTATION	19

APPENDIX A: CONFIGURATION MANAGEMENT	25

GLOSSARY	28

BIBLIOGRAPHY	35

		 PREFACE 

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.

 1.		INTRODUCTION 

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).

	  2.1		EVALUATION OF NEW SYSTEMS  

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 

endorsement.

		7)	If approved, an ETL entry is issued for the 

verification system.

		8)	A TAR is issued for the verification system.

	  2.2		REEVALUATION FOR ENDORSEMENT  

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 

archived.

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 

endorsement.

		7)	If approved, a new ETL entry is issued for the 

		8)	The VR is issued for the revised verification 

	  2.3		REEVALUATION FOR REMOVAL  

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 

evaluation.

	  2.4		BETA VERSIONS  

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 

 3.		METHODOLOGY AND SYSTEM SPECIFICATION 

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.

	  3.1		METHODOLOGY  

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 

conjunction.

		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 
form.
		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 
	  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 
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 
nterpretation.
	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 
	  3.4		DOCUMENTATION  
	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 
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 
construct.  
		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 
approval.
		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 
	  4.3		DOCUMENTATION  
	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 
 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 
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.
 APPENDIX
CONFIGURATION MANAGEMENT 
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]
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 IDENTIFICATION
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 
frequently.  
CONFIGURATION CONTROL
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
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
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 
 GLOSSARY 
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 
Complete
		A theory is complete if and only if every sentence of its 
language is either provable or refutable.
Concurrency 
		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.  
Conjecture 
		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, 
etc.
Correctness 
		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 
Documentation 
		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 
Eventuality 
		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 
Language 
		A set of symbols and rules of syntax regulating the 
Liveness 
		Formalizations that ensure that a system does something 
that it should do.
Metalogic 
		A type of logic used to describe another type of logic or 
a combination of different types of logic.
Methodology 
		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 
Semantics 
		A set of rules for interpreting the symbols and 
Sound 
		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).
Syntax 
		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.
Theorem 
		In a given logical system, a well-formed formula that is 
Theory 
		A formal theory is a coherent group of general 
User-Friendly 
		A system is user-friendly if it facilitates learning and 
usage in an efficient manner.
Valid 
		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.
Verification 
		The process of comparing two levels of system 
top-level specification, top-level specification with source code, or 
[1]
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 
verification.
Well-Formed Formula 
		A sequence of symbols from a language that is constructed 
n accordance with the syntax for that language.

 BIBLIOGRAPHY 
[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