Skip to content

AttestedTLS

Jump to bottom Edit New page
Muhammad Usama Sardar edited this page May 18, 2025 · 11 revisions

Formal Verification of Attested TLS for Confidential Computing

Short description of the challenge

  • Formally specify and verify the protocols combining TLS 1.3 and remote attestation for Confidential Computing use cases

Research team/s involved (or communities)

Main issues / open problems related to the challenge

The main challenge is the extraction of the attested TLS protocol to be formalized, as all the vendors (including Intel, Arm, AMD and IBM) describe the protocols informally. The main issue is that the protocols are either unspecified (leading to security through obscurity), or if specified, they fall in at least one of the following:

  • Issue 1: Incomplete specs (e.g., see here)
  • Issue 2: Vague and outdated specs (e.g., see here)

Open problems

Confidential Computing (CC) workload may refer to, for example, a container in Virtual Machine (VM)-based Trusted Execution Environments (TEEs).

  1. What is the "long-term identity" of the CC workload? How is "long-term identity" assigned to the CC workload? Which entity supplies this "long-term identity"? How is that Identity Supplier trusted?
  2. How is CA-certified Long-Term Key (LTK) injected in the Confidential Computing workload in the first place?
  3. How to augment authentication with attestation rather than replacing authentication with attestation?
  4. What does "freshness" mean for highly dynamic and long-lived workloads?
  5. How to verify the Verifier?

Techniques and technologies related to the challenge

  • Symbolic security analysis
  • Architecturally-defined attestation
  • TLS 1.3
  • Confidential Computing

Example(s)

Other relevant information (external links, references, etc.)

Add a custom footer

list of tools

list of challenges

Clone this wiki locally