AttestedTLS

Formal Analysis and Verification of Attested TLS Protocols 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)

• IETF SEAT (formerly IETF SEAL)
• IRTF UFMRG
• IETF RATS
• IETF TLS
• CCC Attestation SIG
• CCC TAC
• Open Compute Project (OCP) Security
• GlobalPlatform
• GIF TRE Open Suite at The Global Alliance for Genomics and Health (GA4GH)
• Data Security Work Stream (DSWS) at The Global Alliance for Genomics and Health (GA4GH)
• GENXT, Cocos AI, Pacific Analytics, JetBrains, Nebius, ELIXIR Europe, GA4GH
• Industrial partners at Arm, Linaro, Huawei, Siemens, Intuit, Intel, Nokia, ...
• Researchers at TU Dresden, University of Applied Sciences Bonn-Rhein-Sieg, Aalto University, University of Turku, ...
• Team Lead: Muhammad Usama Sardar

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? Which entity generates the LTK and how is that entity trusted?
3. Can CSP really be out of TCB?
4. How to augment authentication with attestation rather than replacing authentication with attestation?
5. What does "freshness" mean for highly dynamic and long-lived workloads?
6. 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.)

• Latest Pre-prints
  • Technical Concepts
  • Validation of TLS 1.3 Key Schedule
  • General Approach
• Papers
  • Pre-handshake attestation
  • Intra-handshake attestation
  • Attestation in Arm CCA and Intel TDX
• Code
• Internet-Drafts
  • TLS-attest
  • Using exported authenticators (Latest editor's version)
• Description of discovered impersonation/diversion attacks
• Recent tutorial at IETF 122
• Some recent slides, videos etc.