+SA-17(03) Formal Correspondence

SA-17(03) Formal Correspondence

Control

Require the developer of the system, system component, or system service to:
  1. Produce, as an integral part of the development process, a formal top-level specification that specifies the interfaces to security-relevant hardware, software, and firmware in terms of exceptions, error messages, and effects;
  2. Show via proof to the extent feasible with additional informal demonstration as necessary, that the formal top-level specification is consistent with the formal policy model;
  3. Show via informal demonstration, that the formal top-level specification completely covers the interfaces to security-relevant hardware, software, and firmware;
  4. Show that the formal top-level specification is an accurate description of the implemented security-relevant hardware, software, and firmware; and
  5. Describe the security-relevant hardware, software, and firmware mechanisms not addressed in the formal top-level specification but strictly internal to the security-relevant hardware, software, and firmware.

Discussion

Correspondence is an important part of the assurance gained through modeling. It demonstrates that the implementation is an accurate transformation of the model, and that any additional code or implementation details that are present have no impact on the behaviors or policies being modeled. Formal methods can be used to show that the high-level security properties are satisfied by the formal system description, and that the formal system description is correctly implemented by a description of some lower level, including a hardware description. Consistency between the formal top-level specification and the formal policy models is generally not amenable to being fully proven. Therefore, a combination of formal and informal methods may be needed to demonstrate such consistency. Consistency between the formal top-level specification and the actual implementation may require the use of an informal demonstration due to limitations on the applicability of formal methods to prove that the specification accurately reflects the implementation. Hardware, software, and firmware mechanisms internal to security-relevant components include mapping registers and direct memory input and output.

Assessment Objective

    1. as an integral part of the development process, the developer of the system, system component, or system service is required to produce a formal top-level specification that specifies the interfaces to security-relevant hardware, software, and firmware in terms of exceptions;
    2. as an integral part of the development process, the developer of the system, system component, or system service is required to produce a formal top-level specification that specifies the interfaces to security-relevant hardware, software, and firmware in terms of error messages;
    3. as an integral part of the development process, the developer of the system, system component, or system service is required to produce a formal top-level specification that specifies the interfaces to security-relevant hardware, software, and firmware in terms of effects;
  2. the developer of the system, system component, or system service is required to show proof that the formal top-level specification is consistent with the formal policy model to the extent feasible with additional informal demonstration as necessary;
  3. the developer of the system, system component, or system service is required to show via informal demonstration that the formal top-level specification completely covers the interfaces to security-relevant hardware, software, and firmware;
  4. the developer of the system, system component, or system service is required to show that the formal top-level specification is an accurate description of the implemented security-relevant hardware, software, and firmware;
  5. the developer of the system, system component, or system service is required to describe the security-relevant hardware, software, and firmware mechanisms that are not addressed in the formal top-level specification but are strictly internal to the security-relevant hardware, software, and firmware.

Assessment Method

Examine

System and services acquisition policy enterprise architecture policy formal policy model procedures addressing developer security architecture and design specifications for the system solicitation documentation acquisition documentation service level agreements acquisition contracts for the system, system component, or system service formal top-level specification documentation system security architecture and design documentation system design documentation system configuration settings and associated documentation documentation describing security-relevant hardware, software, and firmware mechanisms not addressed in the formal top-level specification documentation system security plan other relevant documents or records

Interview

Organizational personnel with system and service acquisition responsibilities organizational personnel with information security responsibilities system developer organizational personnel with information security architecture and design responsibilities

1. Ħarsa ġenerali

1.1 Referenzi

1.2 Rekwiżiti identifikati

1.3 Regolamenti relatati

2. Rekwiżiti identifikati

Rekwiżiti

3. Regolamenti relatati

Regolamenti

Kwistjonijiet marbuta

Links
is blocked by SA-17(03) Formal Correspondence – Assessment Procedure