Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Confidential Computing
This repo contains the artifacts for formal specification and verification of architecturally-defined remote attestation in the following groups:
-
Vendor solutions:
- Intel TDX
-
Architecture led solutions:
- Arm CCA
The groups are based on the level of customization possible.
Attestation is one of the most critical mechanisms of Confidential Computing. Unfortunately, the attestation mechanisms provided by TEEs are quite complex and thus these are not well-understood even by those who call themselves "experts". This lack of understanding has led to several exploits (such as SGAxe) and bugs (such as those found by Google).
The project aims at a better understanding of these mechanisms and the underlying trust assumptions via formal specification and verification. These mechanisms can then be composed with transport protocols (e.g., TLS and SPDM) to build attestation frameworks.
The main challenge is the extraction of the attestation protocol to be formalized, as all the vendors (including Intel, Arm1, AMD and IBM) describe the attestation protocols informally.
- Challenge 1: Incomplete specs (e.g., see here)
- Challenge 2: Vague and outdated specs (e.g., see here)
Our formal models are based on:
- in-depth reading of Intel and Arm specification documents
- our experience with Intel SGX (on which the attestation architecture of Intel TDX is largely based)
- extensive discussions with Intel and Arm
We use state-of-the-art symbolic security analysis tool ProVerif for the specification of the protocols.
The work is published at open-access journal IEEE Access and should be cited as follows:
M. U. Sardar, T. Fossati, S. Frost, S. Xiong, Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Arm CCA and Intel TDX, IEEE Access, 2024.
BibTeX:
@ARTICLE{Sardar2024CcaTdx,
author={Sardar, Muhammad Usama and Fossati, Thomas and Frost, Simon and Xiong, Shale},
journal={IEEE Access},
title = {{Formal Specification and Verification of Architecturally-defined Attestation Mechanisms in Arm CCA and Intel TDX}},
year={2024},
volume={12},
number={},
pages={361-381},
doi={10.1109/ACCESS.2023.3346501}
}
Authors: Muhammad Usama Sardar, Thomas Fossati, Simon Frost and Shale Xiong
- We formally prove the insecurity of the TCB claimed by Intel for TDX (see here). This was reported to Intel and fixed in the latest specs.
- We formally prove that architecturally-defined attestation does not provide authentication property.
- Ambiguities found during the process of formalization in Arm's and Intel's specification of CCA and TDX attestation are summarized in Sections III.H and IV.H (plus Appendix A), respectively, in the paper. These have been reported to the respective vendors.
- The lead author (Muhammad Usama Sardar) noticed the lack of transparency in Intel's documentation process for TDX where Intel updates all the TDX white papers and specifications on the same URLs (with the older version of specs just disappearing), e.g., Intel TDX white paper and TDX Module base specs. He reported this to Intel privately and later publicly in June 2023.
- See another interesting project where our artifacts for Arm CCA are being used as a foundation for the formal verification of a specific proposal of composition of remote attestation and transport protocols (see corresponding IETF draft).
- Intel is using our artifacts for Intel TDX for the formal verification of vTPM TD solution for Intel TDX.
The symbolic security analysis has the following inherent limitations:
- Cryptographic primitives (hash, encryption, MAC, digital signatures) are assumed to be perfect.
- Side-channels are out of scope.
Complementary approaches and tools (e.g., CryptoVerif) can be used to tackle these limitations.
We would like to thank the following for insightful discussions and helpful feedback.
- Nikolaus Thümmel (Scontain)
- Ante Derek (Univeristy of Zagreb)
- Jiewen Yao (Intel)
Install the latest version (2.05 at the moment) of ProVerif: see https://bblanche.gitlabpages.inria.fr/proverif/ for details. See Section 1.4 of manual for installation options:
- via OPAM: Section 1.4.1
- from sources: Section 1.4.2 or simply try the provided script
- from binaries: Section 1.4.3
- Run as follows:
proverif <filename>.pv
For TDX: proverif TDX/TDX.pv
For CCA: proverif CCA/ArmCCA_RA.pv
- Generation of traces for failing properties: In order to additionally generate a trace for each property which results in "false", create a subfolder for results before executing.
Then to execute: run as follows:
proverif -graph <subfolderNameForResults> <filename>.pv
Subfolder will contain the traces in .dot as well as .PDF.
- Horn clauses: To additionally see the Horn clauses generated in ProVerif:
3a. use command-line option -test as follows:
proverif <filename>.pv -test
OR
3b. add one of the following two settings inside the input (*.pv) file:
-
set verboseClauses = short.to display the Horn clauses -
set verboseClauses = explained.to additionally display a sentence after each clause it generates to explain where this clause comes from.
- Interactive mode: To run in interactive mode:
proverif_interact <filename>.pv
If you are around on any of the following venues of upcoming talks (in reverse chronological order) on the project, you are very welcome to join/meet.
We would love to have your feedback (especially critique! yes, this is how the science progresses, but please be genuine!) and contributions. Contact Muhammad Usama Sardar on CCC Slack Workspace, or by email, or open an issue.