Smart Casual Verification of the Confidential Consortium Framework
summary
Specifies CCF's distributed consensus and client-consistency model in TLA+, instruments the C++ code to emit tiny JSON state traces, and repurposes the TLC model checker for trace validation by matching execution steps to the spec. The project integrates trace checks into the CI pipeline, surfaces mismatches caused by differing action granularity and logging limits, and discovers six subtle bugs in design/implementation before any customer impact.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:20Confidential Consortium Framework
- 3:46Verifying CCF’s protocols
- 5:55Verification requirements
- 7:19Choosing TLA+
- 9:03TLA+ specifications
- 11:55Execution traces from CCF
- 12:58Validating traces
- 14:03Results and bugs
- 14:44Trace validation challenges
- 16:30Coverage and improvements
- 17:13Summary and Q&A
related talks
39mFormal specification of attestation mechanisms in Confidential Computing
15mTLC: Temporal Logic of Distributed Components
19mA Verification Methodology for the Arm® Confidential Computing Architecture: Fr...
01h 13mDesigning distributed systems with TLA+
01h 12mWorkshop: TLA+ in action (Part 4)
41mDesigning software with complex configurations
29mTowards End-to-End Verified TEEs via Verified Interface Conformance and Interfa...
34mTLA+ at Microsoft to build planetary-scale systems