Formal specification of attestation mechanisms in Confidential Computing
Talkat Confidential Computing Mini Summit at Open Source Summit Europe 2023 · on Monday, 2023-09-18·
summary
Formal symbolic models and mechanized checks produce reusable verification primitives that cover provisioning, initialization and attestation phases for ARM CCA and Intel TDX, with artifacts proving key properties in minutes. Work yields an open source CCA spec for the composite attester, a planned attested TLS integration and a vTPM verification effort, and delivers a formal proof of insecurity for Intel’s claimed TDX TCB which prompted specification updates; specifications span hundreds to thousands of pages and require clearer, stable wording.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 4:44Attestation overview
- 11:45Attestation diversity challenges
- 17:11Formal methods approach
- 26:42CCA composite attester case
- 28:54Threat model and properties
- 31:24Verification results for CCA and TDX
- 34:34Specification verification challenges
- 35:36Key takeaways and future
- 38:06Q&A
related talks
19mA Verification Methodology for the Arm® Confidential Computing Architecture: Fr...
30mDevice Attestation in Hardware TEE based Confidential Computing
28mSecure bootloader for Confidential Computing
35mChains of trust in Confidential Computing
37mIt's All About Trust: Why Confidential Computing Matters
34mCoCo-as: First Confidential Computing Attestation Solution of CNCF
24mShrinking The Elephant - A Confidential Computing Attestation Sequel
36mSecurity for AI and Multi-Party Collaboration with Confidential Computing (Oh, and...