INTRODUCTION
The primary goal of the National Computer Security Center (NCSC) is
to encourage the widespread availability of trusted systems. This goal is
realized, in large measure, through the NCSC's Commercial Product Evaluation
Program. This program focuses on the technical evaluation of the protection
capabilities of commercially produced and supported systems. The standards
against which products are evaluated are the Department of Defense Trusted
Computer System Evaluation Criteria (TCSEC) for automatic data processing
systems and the Trusted Network Interpretation of the Trusted Computer System
Evaluation Criteria (TNI) for network systems.
The TCSEC and TNI classify systems into seven hierarchical classes
based on features and assurances to support three types of security
requirements - policy, accountability, and assurance. One of the assurance
requirements, Design Specification and Verification, appears in the upper
classes of the TCSEC and TNI. The highest level of trust, Verified Design or
A1, requires that a Formal Top Level Specification of the design be maintained
and shown, either formally or informally, to be consistent with the formal
security policy model for the system. In addition, the requirements state
that "[t]his 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."
PURPOSE
The purpose of the Endorsed Tools List (ETL) is to inform system
developers which formal specification and verification tools are endorsed by
the NCSC for use in designing candidate A1 systems (that is, approved for use
in satisfying the A1 Design Specification and Verification requirement). The
ETL specifies the current version of each verification tool that is approved
by the NCSC.
Additions to and deletions from the ETL will occur as the need
arises, as determined by the NCSC. A compelling reason must exist to justify
the addition of a verification tool onto the ETL. The proposed tool will have
to offer some significant capability not provided by the current set of tools.
Addition of a tool onto the ETL means that this tool may be named in a
Verification Tool Memorandum of Agreement (MOA) between the NCSC and a system
developer. The MOA should specify the specific tool and version to be used in
the formal verification process.
Likewise, profound changes in circumstances could result in the
removal of a verification tool from the list (e.g., discontinuance of support
from the tool developer). Removal of a tool from the ETL means that no *new*
MOAs between the NCSC and system developers will be executed specifying that
particular tool as the vehicle for formal specification and verification.
Formal verification is a young technology. The tools are almost
constantly undergoing enhancement and correction. Consequently, the version
of a tool that has been evaluated by the NCSC may not be the newest most
capable version. These modified versions of an endorsed tool are known as
"beta" tool versions. Beta tool versions may undergo evaluation by the NCSC,
and if the evaluation criteria are met, are declared to be the new evaluated
version, are placed on the ETL, and replace the previously endorsed version.
Trusted system developers may choose to use a beta version of an
endorsed tool. However, it must be realized that beta versions have not been
completely evaluated and are not endorsed. Beta versions are released
primarily to allow the verification tool developers to test the tool before
submitting it for evaluation. Thus, beta tool users incur a slight risk.
When entering a formal evaluation with the NCSC, specifications and proof
evidence must be submitted which can be completely checked without significant
modification using either the currently endorsed version of a verification
tool or a previously endorsed version that was agreed upon in a MOA.
Submitted specifications and proof evidence which are not compatible with the
endorsed or agreed upon version of the tool may require substantial
modification by the system developer.
The products on the ETL have been evaluated against the Formal
Verification Environments Criteria (currently in draft). The outcome of the
evaluation, including a complete analysis of the verification tool, is
documented in a Technical Assessment Report (TAR). The ETL entry is intended
as only a brief summary for quick reference and therefore should not be used
as the sole source for choosing a verification tool. Combining information
from both the ETL entry and the TAR is vital to making a well-informed
decision. The TARs can be obtained by contacting the Office of Research and
Development at the National Computer Security Center in writing.
National Computer Security Center
9800 Savage Road
Fort Meade, Maryland 20755-6000
ATTN: C33, TAR request
DEFINITIONS
BETA TOOL VERSIONS - In order to ensure the availability of the most
current tool versions, tool enhancements to ETL tools may be released for
production use during the "Beta test" stage of development. Beta tool
versions may undergo evaluation by the NCSC, and if the evaluation criteria
are met, are declared to be the new evaluated version, and are placed on the
ETL. Vendors are free to use such Beta Tool Versions for production use.
ENDORSED TOOLS LIST (ETL) - A list composed of those verification
tools that are currently recommended by the NCSC for use in satisfying the A1
Design Specification and Verification requirement in the Trusted Computer
System Evaluation Criteria and Trusted Network Interpretation of the Trusted
Computer System Evaluation Criteria.
FORMAL VERIFICATION ENVIRONMENTS CRITERIA - A document (currently in
draft) that provides the basis for determining the technical merit and
stability of formal specification and verification tools. The criteria
provides evaluators with a metric with which to assess the breadth of a
verification tool and provides guidance to manufacturers on the fundamental
requirements of candidate endorsed verification tools.
TRUSTED COMPUTER SYSTEM EVALUATION CRITERIA (TCSEC) - A Department
of Defense standard (DoD 5200.28-STD) that was published in December 1985 to
provide a means for evaluating specific security features and assurance
requirements available in "trusted commercially available automatic data
processing systems". The rating scale in the TCSEC extends from one that
represents a minimal level of trust to one for "state of the art" features and
assurances.
TRUSTED NETWORK INTERPRETATION OF THE TCSEC (TNI) - A document that
was published in July 1987 to provide a means for evaluating specific security
features and assurance requirements as well as additional security services of
networks.
VERIFICATION TOOL MEMORANDUM OF AGREEMENT (MOA) - A Memorandum of
Agreement between a trusted system developer and the NCSC in which both agree
on the endorsed verification tool and version to be employed for the secure
system development effort.
FORMAL DEVELOPMENT METHODOLOGY
VENDOR: Unisys Corporation
VERSION EVALUATED: 12.4
EVALUATION DATE: 15 January 1988
PRODUCT DESCRIPTION:
The Formal Development Methodology consists of a set of tools and languages,
as follows:
(1) the Ina Jo language, for writing specifications and
requirements
(2) the Inamod language, an extension of the Ina Jo
language, for writing assertions about programs
(3) the Ina Jo Processor, for examining specifications and
generating logical assertions; the latter state that the specifications meet
the requirements
(4) Ina Flo, a multilevel security flow tool, and the
Shared Resource Matrix (SRM) tools, both implemented as independent modules
within the Ina Jo processor. The SRM generates a matrix for manual analysis
and, unlike Ina Flo, requires no changes to existing Ina Jo specifications
(5) the Interactive Theorem Prover (ITP), for assisting
users in proving the logical assertions generated by the Ina Jo Processor
(6) a Verification Condition Generator (VCG) for Modula
for examining specifications and implementations and generating logical
assertion; the latter state that the implementation meets the specification
(7) an ITP Post-Processor called Short, for generating
transcript files of completed proofs. The post-processor eliminates all steps
not actually used in a proof, converts the contents of the file from the ITP
internal representation, and reformats the text
The goal of FDM is to design, formally specify and produce verified
code for complete systems. However, some of the software tools of FDM are
incomplete at this time. The Ina Jo and Inamod languages are considered
complete; language extensions and new capabilities to aid the user are
occasionally implemented. In addition, the Ina Jo language processor, the
ITP, and the ITP post-processor are complete. The initial VCG, for Modula,
and Ina Flo have not been completed and therefore were not part of the
evaluation or endorsement.
FDM has been used extensively on over a half-dozen significant
systems for DCA, AFWL, RADC, and others. Applications include Autodin II, the
Secure Transaction Processing Experiment (STPE), a Job Stream Separator (JSS),
a kernelized IBM VM (KVM), a Computer Operating System/Network Front End
(COS/NFE), and the Secure Release Terminal.
EVALUATION SUMMARY:
FDM 12.4 has been evaluated by the National Computer Security
Center. The evaluation team analyzed the changes between the 12.3 and Beta 4
version of the tool. The changes fell into the following categories: syntax
changes, bug fixes, new features, and changes to theorems. In addition to the
changes that were identified by the developer, the team examined configuration
management evidence, source code, documentation, and existing problems with
the tool that were identified in the Verification Assessment and Mitre
Reports.
The evaluation was not exhaustive, but was sufficient to determine
that version 12.4 is a distinct improvement over version 12.3. A few of the
most notable enhancements are the increase in theorem proving capability, the
addition of a type checking facility, and improved error reporting. A
complete discussion of the changes to the tool can be found in the Technical
Assessment Report.
GYPSY VERIFICATION ENVIRONMENT
VENDOR: Computational Logic Inc. (CLINC)
VERSION EVALUATED: GVE version 13.16 (Gypsy dialect 2.05)
EVALUATION DATE: July 1987
PROJECT DESCRIPTION:
The GVE consists of a set of tools and languages, as follows:
(1) the Gypsy language, which is used for both system
design and specification
(2) the Verification Condition Generator, which translates
specifications into problems in first-order logic
(3) the Gypsy Theorem Prover (GTP), for determining
whether first-order logic statements are theorems
(4) the Gypsy to Bliss translator, which converts Gypsy
code to Bliss code
(5) the Gypsy to Ada translator, which converts a subset
of the present Gypsy language into non-standard Ada
(6) the DataBase Manager, which is used to track the
status of various scopes and theorems the user is maintaining
(7) the Gypsy language parser, for determining the
syntactic and semantic validity of a design
(8) an interface to the ZMACS editor for ease of text
entry
(9) a program optimizer which proves the validity of
efficiency-based decisions in compilation.
The Gypsy Verification Environment (GVE) is designed to be a
complete verification system supporting both a specification language and a
programming language. The goal is to formally specify and verify design and
code for computer systems and applications. However, some of the software
tools of the GVE are incomplete. The Gypsy to Ada translator currently
converts a subset of the Gypsy language to nonstandard Ada. The dependency
tracking mechanism of the GVE currently does not provide complete and proper
tracking of dependencies between specifications, code, proofs and lemmas.
The GVE has been used in a number of prior efforts, including the
only A1 system (SCOMP), the largest examples of code verification (Encrypted
Packet Interface), and is presently being used in several very large projects
which are candidates for A1 evaluation.
The GVE has also received acceptance throughout the verification
community, not only for its applicability and convenient approach, but also
for its unique capabilities. The GVE is currently the only evaluated system
which can handle concurrency or do code level proofs.
EVALUATION SUMMARY:
The Gypsy Verification Environment version 13.16 using Gypsy dialect
2.05 has been evaluated by the National Computer Security Center (NCSC)
against the requirements specified by the Verification System Evaluation
Factors. The NCSC has determined that the GVE satisfies all of the
requirements at the minimum level. However, it was noted that there is an
obvious need for better documentation for system users, especially for new
users. In addition, the lack of a formal basis and formal semantic definition
is a serious shortcoming that needs to be addressed in the near future. While
the GVE is not without weaknesses, it has received acceptance throughout the
verification community, not only for its applicability and convenient
approach, but also for its unique capabilities. The GVE is currently the only
complete system which can handle concurrency or do code level proofs. These
are important features which make the system worth examining.
Verification Evaluation Factors
1. Specification Language
2. Theorem Prover
3. Implementation
4. Documentation
5. Features
6. Assurance and Soundness
7. User Interface
8. Methodology
For a complete description of how the GVE satisfies each of the
evaluation factors, see Technical Assessment Report for GVE 13.16 using Gypsy
2.05.
