Skip to content

Adding Formal Proof of Integrity as Mitigation for Stored Data Integrity

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: 1272

Clause/Subclause: 5.2.10 TR-IDST: Integrity of data stored on the product

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.10 TR-IDST: Integrity of data stored on the product. This correspond to a demonstrated state-of-the-art method to ensure that software (in particular operating systems) enforces integrity of data of user software it is running.

5.2.10.4 MI-FIST: Formal proof of enforcement of integrity of data stored on the product

A formal proof, in a formal verification tool, shall demonstrate that the product protects data stored on the product from unauthorized modification.

The sufficiency of the formal verification tool, the formal definition of integrity, and the formal argument that it applies to a formalization of the product's source code shall be documented. The process to run the formal verification tool to produce a formal proof shall be documented.

  • Reference: TR-IDST

  • Objective: Integrity of data

  • 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 definition of integrity, and the formal argument that it applies to a formalization of the product's source code

  • Verdict: Sufficiency documentation is acceptable, the formal definition of integrity convincingly demonstrates the enforcement of integrity of data stored on the product, the formal verification tool successfully outputs a proof of that the integrity statement is satisfied by the product => 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 definition of the integrity, and the formal argument that it applies to a formalization of the product's source code

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