BaselineWatch
Desk
Your fleet and your work Fleetyour releases and the hardware they run onTriagewhat needs a decisionWatchlistthe products and platforms you runSaved searchesthe lists you come back to
This instance Sourceswhat is read, how often, under what termsDigestthe daily or weekly summary, and alerts
How it is drawn Appearancethe look and the colour schemeBrandingthe mark this instance wears
Owner sign-in

SA-17(01) Formal Policy Model

NIST SP 800-53 (controls) 5.2.0 against 5.2.0
All changes in this version
unchanged SA part of SA-17

Title

Formal Policy Model

Control

Require the developer of the system, system component, or system service to:
(a) Produce, as an integral part of the development process, a formal policy model describing the [Assignment: organization-defined elements of organizational security and privacy policy] to be enforced; and
(b) 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.

Discussion

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.

Parameters

sa-17.1_prm_1: organization-defined elements of organizational security and privacy policy
sa-17.01_odp.01: organizational security policy
sa-17.01_odp.02: organizational privacy policy

Related controls

ac-25, ac-3, ac-4

STIG rules that implement this control 0

No followed STIG rule cites a CCI indexed to this control (CCI list 2026-07-14).