Specifying binding and commitment with ghost outputs and strong refinement
summary
Argues that hyperproperties like binding and commitment become checkable by adding ghost outputs to module interfaces and proving strong refinement (forward-only simulations) so those ghost values are history variables not prophecies. Shows concrete examples: a binding version of crusader agreement that prevents adaptive-adversary bias, a gather abstraction with a guaranteed n−f common core used to implement crusader agreement, and a random-secret-draw pattern; gives simulation-based proofs and failure counts for counterexamples.
AI-written summary · about
chapters (17)
- 0:00Ghost outputs and strong refinement
- 1:24Limitations of spec tools
- 2:26Crusader agreement and consensus
- 5:37Adaptive adversary and termination
- 7:03Ghost outputs introduction
- 10:18Binding crusader agreement
- 13:32Mitigating adversarial interference
- 15:40Refinement and simulation relations
- 18:11Strong refinement and ghost variables
- 19:15Abstraction in randomized consensus
- 21:03Common core and ghost outputs
- 24:57Binding common core and hyperproperties
- 26:03Crusader agreement with gather
- 27:29Correctness proof for algorithm
- 31:39Commitment and secret draw protocols
- 34:30Binding and strong refinement
- 35:16Q&A on binding variants
related talks
01h 12mAn Introduction to Commitment-Based Succinct Arguments
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
15mStatically Verified Refinements for Multiparty Protocols
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
14mA Refinement Methodology for Distributed Programs in Rust
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
45mCorrectness proofs of distributed systems with Isabelle
25mProperty-agnostic base case extension for scalable verification of distributed systems