FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
summary
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the Steel F DSL and proven correct against the original FastVer spec. The monitor finds and fixes multiple bugs in the prior unverified code, runs multi-threaded and scales linearly, achieves about 10M op/sec (verified) versus ~45M with an unverified monitor, and emits signed receipts to detect tampering.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:05Correctness in complex systems
- 3:31Limitations of verification
- 4:58Cryptographically monitored executions
- 7:44Monitor architecture and performance
- 9:46Performance results and goals
- 11:10Proof structure and verification
- 14:23Anchored monotonic counters
- 18:56Key takeaways and future work
- 20:03Q&A
related talks
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
25mSafe Replication through Bounded Concurrency Verification
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
32mVerifying Constant-Time Implementations
21mSecuring Verified IO Programs Against Unverified Code in F*
14mUniStore: A fault-tolerant marriage of causal and strong consistency
32mFormal Verification Made Easy (and fast!)
50mImmutable Values in the Big Wide World