DID FinderBack
Source
DI-MISC-81346

Formal Security Policy Model

A Formal Security Policy Model is a mathematically precise abstract representation of a security policy and the abstract protection mechanisms that enforce it.

Approval DateJuly 2, 1993
AMSC NumberG6936
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.
Supersedes
—
Related
—

Description & Purpose

A Formal Security Policy Model is a mathematically precise abstract representation of a security policy and the abstract protection mechanisms that enforce the policy. To be acceptable as a basis for a trusted computing base (TCB), the model must be supported by formal proof. This Data Item Description (DID) describes both the requirements for the model itself and the document in which the model will be delivered.

Application & Interrelationship

7.1 This Data Item Description (DID) contains the format and content preparation instructions for the data product generated under the work task described by 3.1.4.4, 3.1.3.2.2, 3.2, 3.2.3.2.2, 3.2.4.4, 3.3.3.2.2 and 3.3.4.4 of DOD-5200.28 STD, Department of Defense Trusted Computer System Evaluation Criteria.

7.2 This DID is applicable to any computer acquisition that calls for a formal security policy model as specified by DOD-5200.28 STD, Department of Defense Trusted Computer System Evaluation Criteria (TCSEC) for TCB Classes B1 (Labeled Security Protection), B2 (Structured Protection), B3 (Security Domains), or A1 (Verified Design) products or their equivalent systems. The Formal Security Policy Model is an optional requirement at TCSEC Class B1. If an Informal Security Policy Model is required and available at TCSEC CLASS B1, then the Formal Security Policy Model is redundant and not necessary. The Formal Security Policy Model is based on the Philosophy of Protection Report.

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 a Formal Computer Security Policy Model 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, and any other appropriate descriptive data.
10.2.2Errata Sheet.Errata sheets shall contain 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 definitions.
10.2.6Executive Summary, not to exceed two pages, that briefly describes the security model, including its assumptions and limitations.
10.2.7Introduction.
10.2.8Body of the Report.
10.2.9Attachments.
10.2.10Appendices.
10.2.11Bibliography.List reference sources and applicable documents.
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.Black 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.4Column headings shall be repeated on subsequent pages if tabular material exceeds one page.
10.2.13.5Fold out pages shall be kept to a minimum.
10.2.13.6Paper shall be standard 8 1/2 x 11 inches, white, with black type.The type font shall be standard 10 pitch pica or courier, 12 pitch elite, or equivalent font. Either blocked text (left and right justified) or ragged right (left justified only) shall be used.
10.2.13.7At least one inch margins shall be provided all around each page to allow for drilling and binding.
10.2.13.8The report shall be provided in standard three-ring notebook binders for ease of maintenance.
10.2.13.9The report shall be provided in standard three-ring notebook binders for ease of maintenance.
10.3General.The formal Security Policy Model document shall contain the formal security policy model, its associated proofs, and the supporting explanations and documentation for both the model and proofs. The model contained in the Formal Security Policy Model document consists of two segments: 1) the mathematical representation of the policy which is to be enforced by the TCB, and 2) a mathematical representation of the abstract protection mechanism(s) within the TCB which enforce the described policy. The model shall include the representation of subjects, objects, modes of access, and security labels; the set of security properties enforced by the TCB; the representation of the initial state of TCB; and the representations of the operations performed.
10.4Content.The Formal Security Policy Model document shall provide background information supporting the modeling effort. All of this background information is informal in nature and may be presented in English text, and graphic representations where appropriate. The following items shall be included as part of this information:
10.4.1Summarization of the security policy to be modeled, how this policy relates to the overall security policy (if the policy modeled is some subset of the overall policy), and the source of the policy.This discussion shall be in enough detail to form the background for the model.
10.4.2Discussion in detail of the type of model chosen, and explanation of why this type was selected over other types.
10.4.3Identification of the modeling technique/methodology chosen, and why it was chosen.
10.4.4Expansion of the security policy into security policy statements.These security policy statements may be brief, but they must explicitly and thoroughly describe the security policy. Each policy statement shall be mapped to the Philosophy of Protection Report.
10.4.5Policy segment.The Formal Security Policy Model document shall provide a formal mathematical description of the policy enforced by the TCB. Also, an English language description of the formal security policy model and each of its segments shall be provided. Supporting material should be provided in the following sequence:
10.4.5.1All assumptions used in the model, provided as both mathematical statements (if any) and an English language description.Sufficient supporting rationale to prove the validity of the assumptions shall be provided. An explanation of why the assumptions are necessary to the model and the consequences of violating the assumptions shall also be provided.
10.4.5.2All axioms used in the model, using both mathematical statements and an English language description.This discussion shall include the rationale as to why these axioms are needed and how the axioms are justified. Supporting rationale for each axiom shall be provided by describing its relationship to the model's segments and specific security-enforcement abstract mechanisms in the model.
10.4.5.3The actual model of the policy.Graphic representations of the model's segments may be included (e.g., diagrams and tables). These graphics shall be annotated with English language descriptions. Supporting material shall be provided to describe each of the following:
10.4.5.3.1The classes of subjects and objects controlled by the TCB.Examples of subjects are people, processes, or devices; and objects are records, blocks, pages, components, files, directories, directory trees, and programs, as well as bits, bytes, words, fields, processors, video displays, keyboards, clocks, printers, network nodes, etc.
10.4.5.3.2How subjects are related to users.
10.4.5.3.3How subjects are assigned privileged conditions (trusted subjects).
10.4.5.3.4How users identify themselves to the TCB.
10.4.5.3.5How the TCB records events.
10.4.6Abstract mechanism segment.The actual model of the abstract TCB protection mechanism(s). Graphic representations of the model's segments may be included (e.g., diagrams and tables). These graphics may be annotated with English language descriptions. Supporting material shall be provided to describe each of the following:
10.4.6.1All the rules that permit, as well as constrain, how a subject is allowed access to an object.
10.4.6.2All privileged conditions under which certain kinds of subjects are allowed to bypass the identified mandatory and discretionary access control rules.
10.4.6.3All controls on assigning privileged conditions to subjects.
10.4.6.4All the controls on identifying users to the TCB.
10.4.6.5All the rules that generate an audit event.
10.4.6.6All TCB responses to failures.
10.4.7Class B1 products and their equivalent systems.The following shall be included in this section:
10.4.7.1General.There is no change to the general requirements of the Formal Security Policy Model document for TCB Class B1 products and their equivalent systems.
10.4.7.2Policy segment.There is no change to the policy requirements of the Formal Security Policy Model document for TCB Class B1 products and their equivalent systems.
10.4.7.3Abstract mechanism segment.The Formal Security Policy Model document shall identify the abstract TCB protection mechanism(s) and explain how these mechanisms satisfy the security policy model. Each abstract mechanism shall be discussed separately. Cross-reference these mechanisms to the policy portion of the Philosophy of Protection Report. The explanation shall include a description of how each element within a mechanism supports other elements of the mechanism, if any.
10.4.7.4Segment integration.The integration of the policy and abstract mechanism segments of the model shall include the following:
10.4.7.4.1An explanation to show that the formal security policy model is consistent with its axioms.The explanation shall provide rationale sufficient to demonstrate consistency.
10.4.7.4.2A description of the relationship of each axiom to the model's segments and specific security-enforcement mechanism(s) in the model.
10.4.7.4.3An explanation that shows that the TCB is sufficient to enforce the security policy.The explanation shall provide rationale sufficient to demonstrate consistency.
10.4.8Classes B2 and above products and their equivalent systems.The following shall be included in this section:
10.4.8.1General.The TCB is based on a clearly defined and documented formal security policy model that requires the discretionary and mandatory access control enforcement found in Class B1 TCBs to be extended to all subjects and objects.
10.4.8.2Policy segment.The Formal Security Policy Model document shall provide all theorems used in the model for each security policy segment, using both mathematical statements and an English language description. Supporting rationale for including the theorems shall be provided. The Formal Security Policy Model shall discuss how these theorems represent enforcement of the security policy.
10.4.8.3Mechanisms segment.The Formal Security Policy Model shall provide all theorems used in the model for the TCB protection mechanism(s), using both mathematical statements and an English language description. Supporting rationale for including the theorems shall be provided. The Formal Security Policy Model shall discuss how these theorems represent the TCB protection mechanism(s) and their enforcement of the security policy.
10.4.9Segment integration.The Formal Security Policy Model document shall include an introduction to the kinds of proofs that are provided, along with a rationale that explains why these proofs are sufficient to demonstrate that the TCB is secure with respect to the security properties modeled. The integration of the policy and abstract mechanism segments of the model shall include the following proofs:
10.4.9.1Proof that the model is consistent with its axioms, providing both the mathematical proofs and an English language description of the proofs.
10.4.9.2Proof that shows that the TCB represented in the model is sufficient to enforce the security policy.The Formal Security Policy Model document shall trace each of the following:
10.4.9.2.1The security policy statements in the Philosophy of Protection Report to a formal mathematical statement.A cross reference matrix chart with detailed explanatory text may be used.
10.4.9.2.2The formal mathematical statements back to its security policy statements in the Philosophy of Protection Report.A cross reference matrix chart with detailed explanatory text may be used.
10.4.9.3Proof for each of the theorems used in the model, both the mathematical proof and an English language description of the proof.

References

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