DID FinderBack
Source
DI-MISC-81347

Formal Top Level Specification

The FTLS is a mathematically precise abstract representation of the trusted computing base that describes the TCB interface in terms of exceptions, error messages, and effects.

Approval DateJuly 2, 1993
AMSC NumberG6937
Preparing Activity—
Project Number—
OPRG/C71
DTIC Applicable—
GIDEP Applicable—
Limitation—
Applicable Forms—
Approval Limitation—
Form Version—
DID Formatdd_form_1664
963C CompliantNo
DISTRIBUTION STATEMENT A: Approved for public release; distribution is unlimited.
Supersedes
—
Related
—

Description & Purpose

The Formal Top Level Specification (FTLS) is a mathematically precise abstract representation of the trusted computing base (TCB). The FTLS provides an accurate description of the TCB interface in terms of exceptions, error messages and effects. The FTLS includes hardware and firmware elements if their properties are visible at the TCB interface.

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 4.1 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 an FTLS as specified by DOD-5200.28 STD, Department of Defense Trusted Computer System Evaluation Criteria (TCSEC) for TCB Class A1 (Verified Design) products and their equivalent systems.

Use & Relationship

—

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 FTLS 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 sheets delimiting cumulative page changes from previous versions.
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 definition.List reference sources and applicable documents.
10.2.6Executive Summary.Not to exceed two pages.
10.2.7Introduction.
10.2.8Body of the Report.
10.2.9Attachments.
10.2.10Appendices.
10.2.11Bibliography.
10.2.12Subjective index.
10.2.13Specific format instructions.
10.2.13.1Abbreviations and 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 hand) 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.3General.The FTLS document shall contain the formal top level specification, its associated proofs and assurance arguments, and supporting explanations and documentation for the specification, proofs, and assurance arguments.
10.4Content.
10.4.1Supporting documentation.The FTLS shall provide background information supporting the specification effort. All of this background information is informal in nature and may be presented in English text, and graphic representation where appropriate. The following items shall be included as part of this information:
10.4.1.1An overview of the FTLS that explains the approach taken, the structure of the specification, what has been included and excluded in the specification, and how the specification relates to the Formal Security Policy Model.
10.4.1.2Identification of the portions of the FTLS that are implemented in hardware, software, and in firmware if their properties are visible at the TCB interface.
10.4.1.3A description of the specification/verification methodology chosen, and why it was selected.
10.4.1.4An introduction to the specification itself, to include identification of the users, subjects, objects, access modes, security labels, security properties, initial state, and operations that are part of the specification.
10.4.1.5Identification of the assumptions required by the specification, an explanation as to why they are required, and the consequences of violating the assumptions.
10.4.1.6A combination of formal and informal techniques (e.g., proofs and assurance arguments) that show that the FTLS is consistent with the Formal Security Policy Model.
10.4.1.7Identification of the axioms used in the proofs, why these axioms are needed, and how they are justified.
10.4.2The formal top level specification.The following shall be included in this section:
10.4.2.1As part of the FTLS document, the specification itself shall be presented in the formal mathematical notation of the specification technique chosen.The specification shall include abstract definitions of the functions the TCB performs and the unified protection mechanism required to satisfy the security policy (TCSEC Section 4.1), to include the following:
10.4.2.1.1Representation of subjects, objects, modes of access, and security labels as they are implemented in the TCB.
10.4.2.1.2Representation of hardware and firmware components of the TCB if their properties are visible at the TCB interface.
10.4.2.1.3The set of security properties enforced by the TCB.
10.4.2.1.4Representation of the initial state of the TCB.
10.4.2.1.5Representations of the operations performed by the TCB, including the effects, exceptions, and error messages for interface operations.
10.4.2.1.6A (possibly empty) set of axioms used in the proofs.
10.4.2.2The FTLS shall include the abstract definitions of the hardware and firmware mechanisms that are used to support separate execution domains.
10.4.3Proofs and arguments.This section shall contain a combination of formal techniques (e.g., where verification tools exist) and informal techniques (e.g., convincing assurance arguments) to demonstrate that the FTLS is consistent with the Formal Security Policy Model.

References

—
Schema v3.0Community-maintained · Verify against ASSIST
Community-maintained — not an official government database.
Verify against ASSIST·GitHub·About·Disclaimer