Skip to content

Adding Formal Verification as Mitigation for Secure design and development

Vertical Standard Comment

Please complete the below fields. Further instructions can be found in the repositories README.md Do not forget to add a Label, using the sidebar on the right.

Standard Version (see README.md for info): 86de5c77

Line Number: 759

Clause/Subclause: 5.2.3 TR-SSDD: Secure design and development

Paragraph/Figure/Table: N/A

Comment: Technical Comment

Proposed Changes:

(This is a Technical Comment proposal. I can't add a label for some reason.)

I propose to add the following new mitigation for the requirement 5.2.3 TR-SSDD: Secure design and development. This correspond to a demonstrated state-of-the-art method to ensure that software (in particular operating systems) has been designed and developed in a secure manner.

5.2.3.7 MI-FVFC: Formal verification of functional correctness

All security-relevant parts of the product shall be formally proved correct with respect to a formal specification using a sound formal verification tool that produces a formal proof of conformity between the source code and the formal specification. Such a proof may imply the absence of common memory errors, such as:

  • buffer overflow
  • out-of-bounds
  • use after free
  • double free
  • use of uninitialized variables
  • dereference of invalid pointer

The sufficiency of the formal verification tool and the formal specification shall be documented. The process to run the formal verification tool to produce a formal proof shall be documented.

  • Reference: TR-SSDD

  • Objective: Ensure the operating system source code behaves precisely as its specification mandates (potentially including prevention of unauthorized memory access)

  • Preparation: None

  • Activities: Review the documentation on why the formal verification tool is sufficient, how it is run, the source code for the product, the formal specification of the product, and (depending on the formal verification tool used) the output proof of the formal verification tool.

  • Verdict: Sufficiency documentation is acceptable, the formal specification is a convincing abstract description of the product, the formal verification tool successfully outputs a proof of conformity between the source code and the specification => PASS, otherwise FAIL

  • Evidence: The documentation on why the formal verification tool is sufficient, how it is run, the source code for the product, the formal specification of the product, and (if applicable for the chosen formal verification tool) the output proof of the formal verification tool

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information