Let's Build a Symbolic Analyser And Automatically Find Bugs
summary
Shows how to build a Python symbolic analyser using Z3 to prove reachability, generate concrete inputs for each satisfiable path, and automatically find unreachable code. It disassembles CPython bytecode, builds a bytecode control-flow graph, enumerates basic-block paths, encodes SSA-style variable versions and path constraints, and queries Z3 for satisfiable vs unsatisfiable paths. Demonstrations include deriving a concrete number of pies that meets constraints and explaining limits like path explosion and aliasing.
AI-written summary · about
chapters (24)
- 0:00Start
- 3:18WHAT'S STATIC ANALYSIS
- 3:59WHAT'S SYMBOLIC EXECUTION
- 4:17PROVE THAT THE LAST LINE CAN RUN, WITHOUT RUNNING THE CODE
- 6:19THE Z3 THEOREM PROVER
- 6:57WHAT CAN YOU DO WITH Z3?
- 11:04THE CODE REACHABILITY PROBLEM
- 11:42HOW DO WE PROVE THE BUG?
- 12:29CODE GRAPH ANALYSIS
- 13:05PYTHON BYTECODE
- 15:15FINDING THE BASIC BLOCKS
- 15:51HOW TO FIND A BASIC BLOCK
- 17:18CONNECTING THE BASIC BLOCKS
- 21:30FIGURING IT OUT, STEP BY STEP
- 21:40FAKE VARIABLES
- 22:16ASIDE: VALUES NEVER DIE
- 23:23SINGLE STATIC ASSIGNMENT
- 24:03SETTING VARIABLES
- 24:33CONDITIONAL JUMPS
- 24:58OPERATIONS
- 25:20DETECTING IMPOSSIBLE PATHS
- 25:43GENERATING INPUT FOR CODE COVERAGE TESTS
- 26:38ADD INVARIANTS TO YOUR CODE
- 28:11FURTHER READING
related talks
55mCode Analysis with Zero False Positives in Java
24mSymbiotic: finding bugs in C programs
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
14mStatic Analysis for Zero-Knowledge Programming Languages
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths
43mOmg, how do I write software that isn't a ticking timebomb!?
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools