Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
summary
A static analysis combines a Datalog fixpoint engine with a tightly integrated symbolic solver, invoking the solver tens to hundreds of thousands of times to keep full path sensitivity while avoiding state explosion. Applied to Ethereum, it reports much higher completeness and precision than prior tools, achieving 83-96% statement coverage in experiments, producing per-contract dependency tables reaching 11 million dependency rows, and contributing to real disclosures that earned $350K in bug bounties.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:28Symvalic (Symbolic + value-flow) Analysis
- 1:30Smart Contracts?
- 3:16Ethereum Smart Contracts Impact
- 4:36The Dirty Secret of Program Verification (for security)
- 5:42Execution-Based Approaches (symbolic execution, model checking) Are Horizontal
- 7:32Value-Flow Static Analysis Approaches Are Vertical ("sets of values")
- 8:25Symvalic Analysis Adds Dependencies
- 8:50Symvalic Analysis Basics: Symbolic Expressions + Values
- 9:54Symvalic Analysis with Dependencies
- 12:04Architecture
- 12:39Controlled Experiments
- 14:03Concluding
related talks
33mSymbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontracts
15mPrecise Static Modeling of Ethereum “Memory”
22mHow Decompilation Uncovers Smart Contract Vulnerabilities
13mAdvances in Automated Smart Contract Vulnerability
01h 10mHow Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
23mThanks for all the bugs!
58mSecurity Static Analysis - Avoiding an Angry Mob of Engineers
48mD1T2 - Smashing Ethereum Smart Contracts for Fun and ACTUAL Profit