Skip to content

Adding Formal Proof of Confidentiality as Mitigation for Stored Data Confidentiality

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

Clause/Subclause: 5.2.7 TR-CDST: Confidentiality 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.7 TR-CDST: Confidentiality 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 confidentiality of data of user software it is running.

5.2.7.3 MI-FCST: Formal proof of enforcement of confidentiality 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 access.

The sufficiency of the formal verification tool, the formal definition of confidentiality, 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-CDST
  • Objective: Confidentiality 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 confidentiality, 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 confidentiality convincingly demonstrates the enforcement of confidentiality of data stored on the product, the formal verification tool successfully outputs a proof of that the confidentiality 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 confidentiality, and the formal argument that it applies to a formalization of the product's source code
Edited by June Andronick
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information