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 complexpath 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.