Symbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontracts
summary
A static analysis combines concrete values and symbolic expressions into a symvalic analysis that runs as a Datalog fixpoint while calling a theorem prover tens or hundreds of thousands of times; it is path sensitive, models deep program semantics, and keeps precision via a value-tracking mechanism called dependencies. Implementation uses Datalog rules plus a lightweight symbolic solver, and evaluation shows 83–96% statement coverage on Ethereum smart contracts; results include several real-world disclosures and six bug bounties totaling over $350K.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:08Symbolic value-flow analysis
- 8:14Smart contracts ideal for analysis
- 12:09Execution vs set-based analysis
- 16:00Scalable precision dependencies
- 21:58Benchmark and results
- 23:41Conclusion and future
- 26:39Q&A
related talks
15mSymbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
22mHow Decompilation Uncovers Smart Contract Vulnerabilities
13mAdvances in Automated Smart Contract Vulnerability
38mStatic Code Analysis - A Behind-the-scenes Look
01h 10mHow Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
23mThanks for all the bugs!
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths
58mSecurity Static Analysis - Avoiding an Angry Mob of Engineers