NIST 800-53 REV 5 • SYSTEM AND SERVICES ACQUISITION
SA-17(1) — Formal Policy Model
Require the developer of the system, system component, or system service to: Produce, as an integral part of the development process, a formal policy model describing the {{ insert: param, sa-17.1_prm_1 }} to be enforced; and Prove that the formal policy model is internally consistent and sufficient to enforce the defined elements of the organizational security and privacy policy when implemented.
Supplemental Guidance
Formal models describe specific behaviors or security and privacy policies using formal languages, thus enabling the correctness of those behaviors and policies to be formally proven. Not all components of systems can be modeled. Generally, formal specifications are scoped to the behaviors or policies of interest, such as nondiscretionary access control policies. Organizations choose the formal modeling language and approach based on the nature of the behaviors and policies to be described and the available tools.
Practitioner Notes
For high-assurance systems, require a formal policy model that mathematically describes the security properties the system must enforce. This provides the strongest basis for verifying that the system behaves correctly.
Example 1: For systems requiring high assurance (e.g., those processing Top Secret information), require the developer to provide a formal security policy model (such as Bell-LaPadula for confidentiality or Biba for integrity) and demonstrate that the system's design enforces the model.
Example 2: Use formal methods tools (TLA+, Alloy, Z notation) to specify and verify critical security properties of the system. While formal methods are resource-intensive, they provide mathematical certainty that the system's security properties hold under all conditions.