Agora: Trust Less and Open More in Verification for Confidential Computing
summary
Agora implements a prototype verification platform that pushes heavy static analysis and SMT solving out of the TCB, replacing them with a tiny in-enclave validator (a few hundred LOC) and a blockchain bounty manager that outsources counterexample search; overall trusted code is almost two orders of magnitude smaller than general-purpose frameworks. Policy encodings use a generic assertion language; policy-specific verifier sizes reported: 625 LOC (SFI), 335 LOC (IFC) and 77 LOC (LVI). Evaluation verifies SPEC2006, nginx and OpenLDAP and detects every injected data-leak case.
AI-written summary · about
chapters (12)
- 0:00Agora verification framework
- 0:22Confidential computing limits
- 1:24Problems with verification
- 2:50Trustless and open goals
- 4:14Program analysis out of TCB
- 6:01Policy-agnostic assertions
- 7:07Removing SMT solvers
- 8:34Blockchain bug bounty
- 9:18Prototype TCB comparison
- 10:26Evaluation across policies
- 11:51Summary and future
- 12:53Q&A
related talks
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
35mVeracruz: Privacy-preserving mutliparty computation using trusted hardware
40mDon’t Trust Opaque Clouds, Cryptographically Verify Instead!
26mTrust Is the Next Bottleneck: Why the Agentic Economy Needs Confidential
37mIt's All About Trust: Why Confidential Computing Matters
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
01h 04mSoftware Verification meets Real-World Cryptography
42mSponsored Session: Confidential Computing - New Capabilities for New Workloads