The organization requires the developer of the information system, system component, or information system service to:
-
(a): Produce, as an integral part of the development process, a formal policy model describing the [organization-defined elements of organizational security 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 policy when implemented.
Supplemental
Formal models describe specific behaviors or security policies using formal languages, thus enabling the correctness of those behaviors/policies to be formally proven. Not all components of information systems can be modeled, and generally, formal specifications are scoped to specific behaviors or policies of interest (e.g., nondiscretionary access control policies). Organizations choose the particular formal modeling language and approach based on the nature of the behaviors/policies to be described and the available tools. Formal modeling tools include, for example, Gypsy and Zed.