Towards End-to-End Verified TEEs via Verified Interface Conformance and Interfa...
summary
Framework formalizes TEEs as isolated compartments (Uber objects) with exclusive memory and verified pre/post interfaces, verified in isolation and compiled with interface-preserving compilers so source-level invariants hold at the binary. CASCompCert is proven interface-preserving, a memory transform must be injective, and a Chasm DSL plus a C verifier are used for low-level and C parts. Theorems show any concurrent execution preserves specified invariants and is data-race-free, demonstrated on x88 and R platforms.
AI-written summary · about
chapters (15)
- 0:00End-to-end verified TEEs
- 2:54Limitations of full correctness
- 4:17Lightweight security verification
- 5:22Verified compartments for TEEs
- 6:24Sequential verification and composition
- 9:58Concurrency and interrupts challenges
- 10:41Uber objects concurrent example
- 12:44Sequential guarantees per Uber object
- 15:11Proving concurrent safety
- 15:51Compiler requirements for guarantees
- 17:14CompCert interface-preserving compilation
- 18:23Handling assembly in compartments
- 19:29Threat model and related work
- 20:36Case studies and results
- 21:21Q&A
related talks
38mDeveloping Trusted Applications for Trusted Execution Environments and vTEEs
39mFormal specification of attestation mechanisms in Confidential Computing
40mDoing the Safety Dance: Will Trusted Execution Environments Protect Us?
30mDevice Attestation in Hardware TEE based Confidential Computing
47mThe Rise of Confidential Computing, What It Is and What it Means to You
28mMemory simulations, security and optimization in a verified compiler
27mHasTEE: Programming Trusted Execution Environments with Haskell
15mMy Journey in Secure Compilation