ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
summary
ParDiff statically extracts protocol-format constraints from C implementations, extracts finite-state machines ordered by buffer indices, and uses bisimulation with SMT solving to detect semantic mismatches between implementations. Built on LLVM and three SMT solvers, it analyzes two implementations per protocol in about 50 seconds each, finds 41 real-world bugs (25 confirmed by developers) with a 7% false-positive rate, and reports precise source locations for each inconsistency.
AI-written summary · about
chapters (17)
- 0:00ParDiff introduction
- 1:24Network parsing background
- 3:53Babel bug case study
- 5:17Traditional bug limits
- 6:20Why differential analysis
- 8:07ParDiff core idea
- 10:20Extracting protocol formats
- 11:48Transforming formats into finite state machines
- 13:39FSM simulation comparison
- 14:22ParDiff implementation
- 15:24Evaluation results
- 15:45Summary of contributions
- 16:05Q&A: Generalizing ParDiff
- 16:48Q&A: Format comparison methods
- 17:50Q&A: FSM design
- 18:55Q&A: FSM from constraints
- 21:03Closing remarks
related talks
25mDataplane equivalence and its applications
41mfn_fuzzy: Fast Multiple Binary Diffing Triage With IDA
34mCan your diff(1) do this?! Improving software review and QA with diffoscope
17mDifferential Network Analysis
27mBinSim: Trace-based Semantic Binary Diffing...
42mContemporary Automatic Program Analysis
23mPrecise and Accurate Patch Presence Test for Binaries
27mDep-scan