Model-guided Fuzzing of Distributed Systems
summary
An implementation of a fuzzer for TLA+ models drives scheduler-controlled seed schedules into real systems, maps runtime events to model actions, and uses TLA+ model-state coverage (not line or trace coverage) as feedback to mutate schedules via a coverage-guided loop and model checking. Evaluated on Two-Phase Commit, Etcd-raft and RedisRaft against random, trace, line coverage and RL baselines, it achieves higher coverage and finds 12 previously unknown bugs, four of which are only detected by model-guided fuzzing.
AI-written summary · about
chapters (11)
- 0:00Model-guided fuzzing intro
- 1:07Coverage metrics challenges
- 2:13Code coverage vs concurrency bugs
- 3:39Mazuk trace limitations
- 5:42Coverage-guided fuzzing basics
- 6:25Fuzzing with abstract models
- 7:29Evaluation results and bugs
- 9:11Related work in testing
- 10:36Mallerie comparison
- 11:57Model abstraction limits
- 12:39Conclusion
related talks
19mCAFault: Enhance Fault Injection Technique in Practical Distributed Systems via...
39mMaking Fuzzing Part of Your Software Development Lifecycle
14mFeedback-guided Adaptive Testing of Distributed Systems Designs
52mStructure aware fuzzing
24mTLA+: Your Secret Weapon Against Concurrency Hell
53mFuzz Testing for Fun and Profit
20mKFuzzTest: Targeted Fuzzing of Internal Kernel Functions
53mFuzzing 101