SA-17(3) Developer Security and Privacy Architecture and Design | Formal Correspondence

Require the developer of the system, system component, or system service to: (a) 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; (b) 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; (c) Show via informal demonstration, that the formal top-level specification completely covers the interfaces to security-relevant hardware, software, and firmware; (d) Show that the formal top-level specification is an accurate description of the implemented security-relevant hardware, software, and firmware; and (e) 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.

Source: NIST SP 800-53 Rev 5, SA-17(3). The statement above is our statement of the clause, read from the published text and cited so you can check it against the official text, not the instrument verbatim. Open NIST SP 800-53 Rev 5 in the compliance library.

Base controls and their enhancements. Which apply follows the baseline you are assessed against (for example FedRAMP Moderate or High, or the low, moderate and high baselines of SP 800-53B). Text in square brackets is a parameter your organisation sets.