The Rainbow Books


Guidelines for Formal Verification Systems



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 
intended for vendors building formal specification and verification 
systems that trusted system developers may use in satisfying the 
requirements of the Department of Defense Trusted Computer System 
Evaluation Criteria (TCSEC), DoD 5200.28-STD, and the Trusted Network 
Interpretation of the TCSEC.

As the Director, National Computer Security Center, I invite your
recommendations for revision to this technical guideline.  Address all
proposals for revision through appropriate channels to the National Computer
Security Center, 9800 Savage Road, Fort George G.  Meade, MD, 20755-6000,
Attention: Chief, Technical Guidelines Division.








Patrick R.  Gallagher, Jr.
										
				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 
who helped develop this document.



TABLE OF CONTENTS


FOREWORD	i
ACKNOWLEDGMENTS	ii
PREFACE	iv
1. INTRODUCTION	1
	1.1 PURPOSE	1
	1.2 BACKGROUND	1
	1.3 SCOPE	2
2. EVALUATION APPROACH	3
	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. METHODOLOGY AND SYSTEM SPECIFICATION	8
	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. IMPLEMENTATION AND OTHER SUPPORT FACTORS	15
	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
5. FUTURE DIRECTIONS	23
APPENDIX A: CONFIGURATION MANAGEMENT	25
GLOSSARY	28
BIBLIOGRAPHY	35


		 PREFACE 




One of the goals of the NCSC is to encourage the development of 
production-quality verification systems.  This guideline was developed as 
part of the Technical Guideline Program specifically to support this goal.

Although there are manual methodologies for performing formal 
specification and verification, this guideline addresses verification 
systems that provide automated support. 

Throughout the document, the term developer is used to describe the 
developer of the verification system.  The term vendor is used to describe 
the individual(s) who are providing support for the tool.  These 
individuals 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 
support of this goal the DoD Trusted Computer System Evaluation Criteria 
(TCSEC) was created, against which computer systems could be evaluated.  
The TCSEC was originally published on 15 August 1983 as CSC-STD-001-83.  
In December 1985 the DoD modified and adopted the TCSEC as a DoD Standard, 
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 
document is primarily intended for developers of verification systems to 
use in the development of production-quality formal verification systems.  
It explains the requirements and the process used to evaluate formal 
verification systems submitted to the NCSC for endorsement.


	  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 
defining divisions and classes within divisions.  Currently, the most 
trusted class defined is A1, Verified Design, which requires formal design 
specification and formal verification.  As stated in the TCSEC and TNI, ". 
. . 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 
within the verification community, and stability of the system.

	  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 
placement on the ETL.  Although verification systems that have 
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 
in 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 
documentation.  

The requirements cover those characteristics that can and should exist in 
current verification technology for production-quality systems.  A 
production-quality verification system is one that is sound, 
user-friendly, efficient, robust, well documented, maintainable, developed 
with good software engineering techniques, and available on a variety of 
hardware. [2]  The NCSC's goal is to elevate the current state of  
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 
systems placed on the ETL will either be significant improvements to 
systems already on the list or will provide a useful approach or 
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 
sections 3 and 4.  Section 5 contains a short list of possibilities for 
next-generation verification systems.  It is not an all-encompassing list 
of features as this would be counterproductive to the goals of research.

2.		EVALUATION APPROACH 


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 
placement on the ETL.

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 
shall support the NCSC evaluators.  For example, the developers shall be 
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 
placement on the ETL (reevaluation for endorsement), and 3) the 
reevaluation of a system on the ETL being considered for removal from the 
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 
system meets this requirement, the evaluators shall analyze the entire 
verification system, concentrating on the requirements described in 
Chapters 3 and 4 of this document.  If a requirement is not completely 
satisfied, but the developer is working toward completion, the relative 
significance of the requirement shall be measured by the evaluation team.  
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 
satisfied shall be identified and documented in the final evaluation 
report.

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 
when evaluating the verification system.

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 
systems lack.

		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 
recommendations on endorsement.

		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 
warrant a reevaluation for endorsement.  The intent of this type of 
reevaluation is to permit improvements to endorsed versions and advocate 
state-of-the-art technology on the ETL while maintaining the assurance of 
the original endorsed version.  

A verification system that is already on the ETL maintains assurance of 
soundness and integrity through configuration management (see Appendix).  
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 
sufficient commentary to allow an understanding of every change made to 
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 
system does not sustain its endorsement, the vendor may be given the 
option for another review by the Committee.  The reevaluation cycle ends 
with an endorsement determination by the Committee Chairperson, and if the 
determination is favorable, a listing of the new release is added to the 
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 
revised verification system.

		8)	The VR is issued for the revised verification 
system.


	  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 
support and maintenance, and unsoundness are all reasons which may warrant 
removal of a verification system from the ETL.  Upon removal, the 
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 
system agreed upon in the MOA.  Verification evidence from a removed or 
replaced verification system shall not be accepted in new system 
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 
system from the ETL.

		1)	The Verification Committee questions the 
endorsement of a verification system on the ETL.

		2)	An evaluation team is formed and the verification 
system evaluation begins, focusing on the area in question.

		3)	Upon completion of the evaluation, a TAR is 
written by the evaluation team.

		4)	The Committee reviews the TAR and makes 
recommendations on removal.

		5)	The Committee Chairperson approves or disapproves 
removal.

		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 
system that has been endorsed may not be the newest and most capable 
version.  Modified versions are known as beta tool versions.  Beta 
versions are useful in helping system developers uncover bugs before 
submitting the verification system for evaluation.

The goal of beta versions is to stabilize the verification system.  Users 
should not assume that any particular beta version will be evaluated or 
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 
without significant modification using an endorsed tool as stated in the 
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 
require substantial modification by the trusted system developer.

 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 
divided into four categories: 1) methodology, 2) features, 3) assurance, 
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 
describe the verification system, its components, application, operation, 
and maintenance.

These categories extend across each of the components of the verification 
system.  These components minimally consist of the following:

	a)	a mathematical specification language that allows the user 
to express correctness conditions,

	b)	a specification processor that interprets the 
specification and generates conjectures interpretable by the reasoning 
mechanism, and 

	c)	a reasoning mechanism that interprets the conjectures 
generated by the processor and checks the proof or proves that the 
correctness conditions are satisfied.


	  3.1		METHODOLOGY  

The methodology of the verification system shall consist of a set of 
propositions used as rules for performing formal verification in that 
system.  This methodology shall have a sound, logical basis.  This 
requirement is a necessary but not sufficient condition for the 
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 
support the underlying methodology.  For example, if the methodology 
requires that a specification language be used to model systems as state 
machines, then the specification language must semantically and 
syntactically support all of the necessary elements for modeling systems 
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 
wherever possible; reasonably mnemonic symbols should be used in other 
cases.  This aids the users in interpreting constructs more readily.

		d.	Internal uniformity.

		The syntax of the specification language shall be 
internally uniform.  This ensures that the rules of the specification 
language are not contradictory.

		e.	Overloading.

		Each terminal symbol of the specification language's 
grammar should support one and only one semantic definition insofar as it 
increases 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 
interpretation 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 
specification at a single time.  Incremental verification may also include 
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 
specification processing to the user in an easily interpretable manner.


		   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 
generated by the specification processor that must be proven, then the 
reasoning mechanism must be able to interpret these conjectures correctly.

		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 " 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, 
standard reasoning mechanism that facilitates debugging and demonstrates 
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 
reprocessing completed proof sessions.  This is to ensure that users have 
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 
proof session.

		e.	Validation.

		The methodology shall provide a means for validating proof 
sessions independently of the reasoning mechanism.  Proof strategies 
checked by an independent, trustworthy proof checker shall ensure that 
only sound proof steps were employed in the proof process.  Trustworthy 
implies that there is assurance that the proof checker accepts only valid 
proofs.  The validation process shall not be circumventable and shall 
always be invoked for each completed proof session.

		f.	Reusability.

		The reasoning mechanism shall facilitate the use of 
system- and user-supplied databases of reusable definitions and theorems.  
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 
dependencies shall be identified and maintained so that if modifications 
are made to a specification (and indirectly to any related 
conjectures/theorems), the minimal set of theorems and lemmas that are 
dependent on the modified proofs will need to be reproved.


	  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 
results are  needed for the users to interpret the results homogeneously.  
This will ensure faster and easier interpretation and fewer errors in 
interpretation.  

	d.	Previous use.

	The verification system shall have a history of use to establish 
stability, usefulness, and credibility.  This history shall contain 
documentation of applications (for example, applications from academia or 
the developers).  These applications shall test the verification system, 
so that strengths and weaknesses may be uncovered.

	e.	Error recovery.

	The verification system shall gracefully recover from internal 
software errors.  This error handling is necessary to ensure that errors 
in the verification system do not cause damage to a user session.

	f.	Software engineering.

	The verification system shall be implemented using documented 
software engineering practices.  The software shall be internally 
structured into well-defined, independent modules for ease of 
maintainability and configuration management.  

	g.	Logical theory.

	All logical theories used in the verification system shall be 
sound.  If more than one logical theory is used in the verification 
system, then there shall be evidence that the theories work together via a 
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 
different hardware environments that support the verification system.


	  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 
shall be explained and fully documented.  This documentation is essential 
for the evaluators and will aid the users in understanding the methodology.

	b.	Formal definition.

	A formal definition (e.g., denotational semantics) of the 
specification language(s) shall be provided.  A formal definition shall 
include a clear semantic definition of the expressions supported by the 
specification language and a concise description of the syntax of all 
specification language constructs.  This is essential for the evaluators 
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 
provided.  This is essential for users to be able to understand the 
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 
describe the verification system, its components, application, operation, 
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 
shall be easily interpretable, precise, and consistent.  This is to ensure 
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 
should be compatible in the specification language (reasoning mechanism).

		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 
in the message is encountered.  The output must be informative and 
interpretable 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 
shall be proportional to the processing time of smaller, less complex 
specifications.  Users should not need to wait an unacceptable amount of 
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 
provides both the system maintainers and the evaluators with a method of 
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 
possibility that system changes will convert non-CI components into CIs.

		c.	Configuration management tools.

		Tools shall exist for comparing a newly generated version 
with the pre*vious version.  These tools shall confirm that a) only the 
intended 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 
have been inserted into the verification system that were not intended by 
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 
including software, documentation, design data, source code, the running 
version of the object code, and tests.  Configuration control shall begin 
in 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 
implementation but also the updat*ing of all related material to reflect 
each change.  For example, often a change to one area of a verification 
system may necessitate a change to an*other area.  It is not acceptable to 
write or update documentation only for new code or newly modified code, 
rather than for all parts of the verification sys*tem affected by the 
addition or change.  Changes to all CIs shall be subject to review and 
approval.

		The configuration control process begins with the 
documentation of a change request.  This change request should include 
justification for the proposed change, all of the affected items and 
documents, and the proposed solution.  The change request shall be 
recorded in order to provide a way of tracking all proposed system changes 
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 
why not?  What were all the changes in a given CI between releases N and 
N+1?  By whom were they made, and why?  What other modifications were 
required by the changes to this CI?  Were modifications required in the 
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 
status of the system.

		g.	Configuration control board.

		The vendor's Configuration Control Board (CCB) shall be 
responsible for approving and disapproving change requests, prioritizing 
approved modifications, and verifying that changes are properly 
incorporated.  The members of the CCB shall interact periodically to 
discuss configuration man*agement topics such as proposed changes, 
configuration status accounting reports, and other topics that may be of 
interest to the different areas of the system development.


		   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 
system.  The test suite shall be enhanced as software errors are 
identified 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 
demonstrate that software accurately generates assertions, correctly 
implements 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 
specifications.


	  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 
documentation.  The plan shall include the following:

		1.	The configuration management plan shall describe 
what is to be done to implement configuration management in the 
verification system.  It shall define the roles and responsibilities of 
designers, developers, management, the Configuration Control Board, and 
all of the personnel involved with any part of the life cycle of the 
verification system.  

		2.	Tools used for configuration management shall be 
documented in the configuration management plan.  The forms used for 
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 
design and implementation of changes are proposed, evaluated, coordinated, 
and approved or disapproved.  The configuration management plan shall also 
include the steps to ensure that only those approved changes are actually 
included and that the changes are included in all of the necessary areas.

		4.	The configuration management plan shall describe 
how changes are made to the plan itself and how emergency procedures are 
handled.  It should describe the procedures for performing time-sensitive 
changes without going through a full review process.  These procedures 
shall define the steps for retroactively implementing configuration 
management after the emergency change has been completed.

	b.	Configuration management evidence.

	Documentation of the configuration management activities shall be 
provided to the evaluators.  This ensures that the policies of the 
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, 
shall be provided.  This provides the evaluators with evidence that good 
software engineering practices and configuration management procedures 
were used in the implementation of the verification system.

	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 
interfacing 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 
reside in the user's guide, the reference manual, or a separate document.

 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 
in 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 
properties involving liveness, concurrency, and eventuality.

	c.	The reasoning mechanism should include a method for 
reasoning about information flows.

	d.	The design and code of the verification system should be 
formally verified.

	e.	The theory should support rapid prototyping.  Rapid 
prototyping supports a way of developing a first, quick version of a 
specification.  The prototype provides immediate feedback to the user.

	f.	The verification system should make use of standard (or 
reusable) components where possible (for example, use of a standard 
windowing system, use of a standard language-independent parser, editor, 
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 
identifying 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 
high-level debugging/tracing of unsuccessful proofs.

	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, 
deletions, or changes made to the verification system do not jeopardize 
its 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 
physical characteristics of each configuration item for the system; 2) 
manage all changes to these characteristics; and 3) record and report the 
status of change processing and implementation.  Configuration management 
involves process monitoring, version control, information capture, quality 
control, bookkeeping, and an organizational framework to support these 
activities.  The configuration being managed is the verification system 
plus all tools and documentation related to the configuration process.

Four major aspects of configuration management are configuration 
identification, configuration control, configuration status accounting, 
and configuration auditing.  



CONFIGURATION IDENTIFICATION

Configuration management entails decomposing the verification system into 
identifi*able, understandable, manageable, trackable units known as 
Configuration Items (CIs).  A CI is a uniquely identifiable subset of the 
system that represents the small*est portion to be subject to independent 
configuration control procedures.  The decomposition process of a 
verification system into CIs is called configuration identification.  

CIs can vary widely in size, type, and complexity.  Although there are no 
hard-and-fast rules for decomposition, the granularity of CIs can have 
great practical importance.  A favorable strategy is to designate 
relatively large CIs for elements that are not expected to change over the 
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 
involves strict procedures for proposing, monitoring, and approving system 
changes and their implementation.  Configuration control entails central 
direction of the change process by personnel who coordinate analytical 
tasks, approve system changes, review the implementation of changes, and 
supervise other tasks such as documentation.



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 
status of that CI at any specific time.  The associated records must 
include commentary about the reason for each change and its major 
implications 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 
describes what the vendor is doing to the system at each moment and what 
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, 
documented, and implemented correctly.  

The members of the CCB should interact periodically, either through formal 
meetings or other available means, to discuss configuration management 
topics such as proposed changes, configuration status accounting reports, 
and other topics that may be of interest to the different areas of the 
system development.  These interactions should be held to keep the entire 
system team updated on all advancements or alterations in the verification 
system.

 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 
prior to submission for endorsement.

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 
descriptions and all departures from the baseline during design and 
production.

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 
design, hardware, firmware, software, and documentation which provides 
sufficient assurance that the system is protected against the introduction 
of improper modification prior to, during, and after system 
implementation. [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 
design, development, test, and production tasks. [3]

Configuration Item (CI) 

		The smallest component tracked by the configuration 
management system. [3]

Configuration Management 

		The process of controlling modifications to a verification 
system, including documentation, that provides sufficient assurance that 
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 
such that the formula and its negation are provable theorems.

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 
system satisfies the correctness conditions (critical requirements 
specification).

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 
recommended by the NCSC for use in developing highly trusted systems.

Eventuality 

		The ability to prove that at some time in the future, a 
particular event will occur.

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 
system and a formal security policy model or (implementation verification) 
between the formal specification and its program implementation. [1]

Implementation Verification 

		A demonstration that a program implementation satisfies a 
formal specification of a system.

Informal Justification 

		An English description of the tools of a verification 
system and how they interact.  This includes a justification of the 
soundness of the theory.

Language 

		A set of symbols and rules of syntax regulating the 
relationship between the symbols, used to convey information.

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.

Production Quality 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]

Proof 

		A syntactic analysis performed to validate the truth of an 
assertion relative to an (assumed) base of assertions.

Proof Checker 

		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 
something that it should not do.

Semantics 

		A set of rules for interpreting the symbols and 
well-formed formulae of a language.

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 
given semantics if every conjecture that can be proved is a valid 
consequence of the assumptions used in the proof.

Specification Language 

		A logically precise language used to describe the 
structure or behavior of a system to be verified.

Specification Processor 

		A software tool capable of receiving input, parsing it, 
generating conjectures (candidate theorems), and supplying results for 
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 
proven in that system.

Theory 

		A formal theory is a coherent group of general 
propositions used as principles of explanation for a particular class of 
phenomena.

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 
specification for proper correspondence (e.g., security policy model with 
top-level specification, top-level specification with source code, or 
source code with object code).  This process may or may not be automated. 
[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 
representatives from both the NCSC's Office of Research and Development 
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 
in 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 
Interpretation of the Trusted Computer System Evaluation Criteria, 
NCSC-TG-005, July 1987.

[5]		National Security Agency, Information Systems Security 
Products and Services Catalogue, Issued Quarterly, January 1989 and 
successors.