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(04) Informal Correspondence

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

Title

Informal Correspondence

Control

Require the developer of the system, system component, or system service to:
(a) Produce, as an integral part of the development process, an informal descriptive top-level specification that specifies the interfaces to security-relevant hardware, software, and firmware in terms of exceptions, error messages, and effects;
(b) Show via [Selection: informal demonstration, convincing argument with formal methods as feasible] that the descriptive top-level specification is consistent with the formal policy model;
(c) Show via informal demonstration, that the descriptive top-level specification completely covers the interfaces to security-relevant hardware, software, and firmware;
(d) Show that the descriptive top-level specification is an accurate description of the interfaces to security-relevant hardware, software, and firmware; and
(e) Describe the security-relevant hardware, software, and firmware mechanisms not addressed in the descriptive 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 additional code or implementation detail has no impact on the behaviors or policies being modeled. Consistency between the descriptive top-level specification (i.e., high-level/low-level design) and the formal policy model is generally not amenable to being fully proven. Therefore, a combination of formal and informal methods may be needed to show such consistency. Hardware, software, and firmware mechanisms strictly internal to security-relevant hardware, software, and firmware include mapping registers and direct memory input and output.

Parameters

sa-17.04_odp: [informal demonstration, convincing argument with formal methods as feasible]

Related controls

ac-25, ac-3, ac-4, sa-4, sa-5

STIG rules that implement this control 0

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