FIPS Standard

All software and firmware components within a cryptographic module shall be implemented using
a high-level language, except that the limited use of a low-level language (e.g., assembly language
or microcode) is allowed if essential to the performance of the module or when a high-level
language is not available.
•
• If HDL is used, all hardware components within a cryptographic module shall be implemented
using a high-level specification language.
SECURITY LEVEL 4
In addition to the requirements for Security Levels 1, 2, and 3, the following requirements shall apply to
cryptographic modules for Security Level 4.
• Documentation shall specify a formal model that describes the rules and characteristics of the
cryptographic module security policy. The formal model shall be specified using a formal
specification language that is a rigorous notation based on established mathematics, such as first
order logic or set theory.
• Documentation shall specify a rationale that demonstrates the consistency and completeness of the
formal model with respect to the cryptographic module security policy.
• Documentation shall specify an informal proof of the correspondence between the formal model
and the functional specification.
• For each cryptographic module hardware, software, and firmware component, the source code shall
be annotated with comments that specify (1) the preconditions required upon entry into the module
component, function, or procedure in order to execute correctly and (2) the postconditions expected
to be true when execution of the module component, function, or procedure is complete. The
preconditions and postconditions may be specified using any notation that is sufficiently detailed to
completely and unambiguously explain the behavior of the cryptographic module component,
function, or procedure.
• Documentation shall specify an informal proof of the correspondence between the design of the
cryptographic module (as reflected by the precondition and postcondition annotations) and the
functional specification.
RECOMMENDED SOFTWARE DEVELOPMENT PRACTICES FOR ALL LEVELS
Implementation of software and firmware components within a cryptographic module using recommended
development practices listed in Appendix B will facilitate the analysis of the components for conformance
to the requirements in this standard and will reduce the chance of design errors.
4.10.4 Guidance Documents
Crypto officer guidance is concerned with the correct configuration, maintenance, and administration of the
cryptographic module. User guidance describes the security functions of the cryptographic module along
with instructions, guidelines, and warnings for the secure use of the module. If a cryptographic module
supports a maintenance role, user/crypto officer guidance describes the physical and/or logical maintenance
services for operators assuming the maintenance role.
Crypto officer guidance shall specify:
38