Finding bugs without running or even looking at code
summary
Demonstrates using the model checker Alloy to find concrete bugs without reading or running code: a 300-line model of multiple portals, SAML flows and tokens generates a 13-step sequence that makes a portal hold a token the identity provider cannot revoke, forcing a release delay. Shows an accounts/users/resources model refined with explicit facts to prevent users in multiple accounts and parent loops. Also cites a study where Alloy found counterexamples to all seven Chord protocol claims, all without inspecting source (no code inspected).
AI-written summary · about
chapters (8)
- 0:00Introduction to formal methods
- 1:29Talking to experts and writing down
- 5:47What is Alloy and model checkers
- 7:12Building a permission system model
- 12:50Design validation with Alloy
- 23:47Real-world Alloy use cases
- 35:00Analyzing the Chord protocol
- 36:45Key takeaways and resources
related talks
41mDesigning software with complex configurations
03mInterview
18mSemantic-Type-Guided Bug Finding
42mContemporary Automatic Program Analysis
50mCracking the Code to Secure Software
46mKeynote: Formal Verification? No, Formal Reasoning!
31mCooperative Specification via Composition Control
31mModel Checking Distributed Software Systems