DI-MISC-81350
Trusted Computing Base Verification Report
The Trusted Computing Base (TCB) Verification Report documents the results of verifying the correlation between the Descriptive Top Level Specification (DTLS) or Formal Top Level Specification (FTLS) of a TCB and its implementing programming language source statements.
Approval DateJuly 2, 1993
AMSC NumberG6940
Preparing Activity—
Project Number—
OPRG/C71
DTIC Applicable—
GIDEP Applicable—
Limitation—
Applicable Forms—
Approval Limitation—
Form VersionAPR 89
DID Formatdd_form_1664
963C CompliantNo
DISTRIBUTION STATEMENT A: Approved for public release; distribution is unlimited.
Description & Purpose
The Trusted Computing Base (TCB) Verification Report documents the results of verifying the correlation between the Descriptive Top Level Specification (DTLS) or the Formal Top Level Specification (FTLS) of a TCB and its implementing programming language source statements.
Application & Interrelationship
This Data Item Description (DID) contains the format and content preparation instructions for the data product generated under the work task described by 3.3.4.4 and 4.1.3.2.2 of DOD-5200.28 STD, Department of Defense Trusted Computer System Evaluation Criteria.
This DID is applicable to any computer acquisition that calls for the verification of the correspondence/mapping between an implemented TCB and a TLS as specified by DOD-5200.28 STD, Department of Defense Trusted Computer System Evaluation Criteria (TCSEC) for TCB Classes B3 (Security Domains) and A1 (Verified Design) products and their equivalent systems.
The information required by 10.3 is required for all class products and their equivalent systems applicable to the DID as a whole. In addition, the information required in 10.3.1 and 10.3.2 is necessary for various classes of products and their equivalent systems.
Preparation Instructions
10.1Source Document.The applicable issue of the documents cited herein, including their approval date, and dates of any applicable amendments and revisions shall be reflected in the contract.
10.2Format.Document the outcome of a verification of the implementing source language statements to the TLS as follows:
10.2.1Cover Sheet:Shall contain Title, Contract Number, Procuring Activity, Contractor Identification, Acquisition Program Name, disclaimers (as provided by the procuring activity contracting officer), date, version number, security classification, and any other appropriate descriptive data.
10.2.2Errata Sheet.Shall contain sheet delimiting cumulative page changes from previous version(s).
10.2.3Table of Contents.Shall contain paragraph numbers, paragraph names, and page numbers.
10.2.4List of illustrations, diagrams, charts and figures.
10.2.5Glossary of abbreviations, acronyms, terms, symbols, and notation used, and their definitions.
10.2.7Executive Summary.Not to exceed two pages, that briefly summarizes the TCB Verification Report.
10.2.8Body of the Report.
10.2.11Bibliography.List references and all applicable documents.
10.2.13Specific format instructions.
10.2.13.1Abbreviations acronyms shall be defined when first used in the text and shall be placed in the glossary.
10.2.13.2Pages shall be numbered separately and consecutively using Arabic numerals.Blank pages shall be numbered.
10.2.13.3Paragraphs shall have a short descriptive title and shall be numbered consecutively using Arabic numerals.Numbering schemes beyond the fourth level (e.g., 4.1.2.5.8) are not permitted.
10.2.13.4Chapters shall begin on an odd-numbered (right-handed) page.
10.2.13.5Either single- or double-sided printing shall be used.If double-sided, the document shall be printed or typed head-to-head, front-to-back.
10.3Content.At TCB Class B3 level, the TCB Verification Report provides the correspondence between the Descriptive Top Level Specification (DTLS) and the TCB implementing source code to demonstrate that the DTLS has been correctly and accurately implemented. At TCB Class A1 level, the Formal Top Level Specification (FTLS) is mapped to the source code to demonstrate that the FTLS has been accurately implemented in the selected programming language (and hardware). The TCB Verification Report shall include.
10.3.1The TCB Verification Report shall briefly describe the TCB whose implementation will be verified in the report.
10.3.2The TCB Verification Report shall describe and illustrate the techniques and rules used.
10.3.3Class B3 products and their equivalent systems.The DTLS is a top level specification informally written. From the design in the DTLS, the implementing program is written using source language statements. The correspondence called for here shall show that these source language statements correctly and accurately reflect the DTLS.
10.3.3.1The TCB Verification Report shall informally show that the TCB implementation (i.e., in hardware, firmware, and software) is consistent with the DTLS.
10.3.3.2The TCB Verification Report shall show, using informal techniques, that the elements of the DTLS correspond to the elements of the TCB.
10.3.3.3For every portion of the TCB software which does not correspond to the DTLS, a convincing rationale shall be provided that this "residual" code is consistent with the DTLS, does not violate the design of the DTLS, and has a valid function within the TCB (i.e., the TCB does not contain any "Trojan Horse" code).
10.3.4Class A1 products and their equivalent systems.The FTLS is a top level specification written and verified in a formal language. The following shall be included:
From the FTLS, the implementing program is written using source language statements from the selected programming language. The mapping called for here provides evidence of the accurate implementation of the FTLS to the TCB source code.
10.3.4.1A description of how the specification language constructs relate to the selected programming language constructs.
10.3.4.2A detailed mapping of the TCB implementation in software, firmware, or hardware to the FTLS.This mapping shall demonstrate that the TCB implementation is consistent with the FTLS.
10.3.4.3The TCB Verification Report shall show, using informal techniques, that the elements of the FTLS correspond to the elements of the TCB.
10.3.4.4For every portion of the TCB software, which does not correspond to the FTLS, a convincing rationale shall be provided that this "residual" code is consistent with the FTLS, does not violate the properties of the FTLS, and has a valid function within the TCB (i.e., the TCB does not contain any "Trojan Horse" code).
Schema v3.0Community-maintained · Verify against ASSIST 