Symbolic Value-flow Static Analysis of Ethereum Smart Contracts

We present a static analysis approach that combines concrete values and symbolic expressions. This symbolic value-flow (“symvalic”) analysis models program behavior with high precision, e.g., full path sensitivity. To achieve deep modeling of program semantics, the analysis relies on a symbiotic relationship between a traditional static analysis fixpoint computation and a symbolic solver: the solver does not merely receive a complex “path condition” to solve, but is instead invoked repeatedly (often tens or hundreds of thousands of times), in close cooperation with the flow computation of the analysis.

The result of the symvalic analysis architecture is a static modeling of program behavior that is much more complete than symbolic execution, much more precise than conventional static analysis, and domain-agnostic: no special-purpose definition of anti-patterns is necessary in order to compute violations of safety conditions with high precision.

We apply the analysis to the domain of Ethereum smart contracts. This domain represents a fundamental challenge for program analysis approaches: despite numerous publications, research work has not been effective at uncovering vulnerabilities of high real-world value.

In systematic comparison of symvalic analysis with past tools, we find significantly increased completeness (shown as 83-96% statement coverage and more true error reports) combined with much higher precision, as measured by rate of true positive reports. In terms of real-world impact, since the beginning of 2021, the analysis has resulted in the discovery and disclosure of several critical vulnerabilities, over funds in the many millions of dollars. Six separate bug bounties totaling over $350K have been awarded for these disclosures.

Read more

Related Posts

VIEW ALL
The CPIMP Attack: an insanely far-reaching vulnerability, successfully mitigated
Tech Deep Dive

The CPIMP Attack: an insanely far-reaching vulnerability, successfully mitigated

[by the Dedaub team] A major attack on several prominent DeFi protocols over many blockchains was …

15 July 2025
The $11M Cork Protocol Hack: A Critical Lesson in Uniswap V4 Hook Security
Tech Deep Dive

The $11M Cork Protocol Hack: A Critical Lesson in Uniswap V4 Hook Security

On 28th of May 2025, Cork Protocol suffered an $11M exploit due multiple security weaknesses, …

30 May 2025
The Cetus AMM $200M Hack: How a Flawed “Overflow” Check Led to Catastrophic Loss
Tech Deep Dive

The Cetus AMM $200M Hack: How a Flawed “Overflow” Check Led to Catastrophic Loss

On May 22, 2025, the Cetus AMM on the Sui Network suffered a devastating hack resulting in over $200 …

23 May 2025