Symbolic Value-Flow Static Analysis
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete
Modeling of Ethereum Smart Contracts
Pavel Šimovec
468914@mail.muni.cz
Faculty of Informatics, Masaryk University
November 19, 2021
Yannis Smaragdakis et al. Symbolic Value-Flow Static Analysis: Deep,
Precise, Complete Modeling of Ethereum Smart Contracts (Artifact). Sept.
2021. DOI: 10.5281/zenodo.5494813. URL:
https://doi.org/10.5281/zenodo.5494813
Symvalic analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 2 / 15
Symvalic analysis
a precise, path sensitive static analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 2 / 15
Symvalic analysis
a precise, path sensitive static analysis
mixes values and symbolic expressions
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 2 / 15
Symvalic analysis
a precise, path sensitive static analysis
mixes values and symbolic expressions
scalable precision through dependencies
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 2 / 15
Symvalic analysis
a precise, path sensitive static analysis
mixes values and symbolic expressions
scalable precision through dependencies
applied to ethereum smart contracts
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 2 / 15
Why smart contracts?
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 3 / 15
Why smart contracts?
correctness is crucial
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 3 / 15
Why smart contracts?
correctness is crucial
code and execution of high value contracts is publicly available
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 3 / 15
Why smart contracts?
correctness is crucial
code and execution of high value contracts is publicly available
code is compact
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 3 / 15
Success of symvalic analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 4 / 15
Success of symvalic analysis
authors were able to find 6 major security vulnerabitilites
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 4 / 15
Success of symvalic analysis
authors were able to find 6 major security vulnerabitilites
$350k in bounties
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 4 / 15
Precision/completeness of common approaches
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 5 / 15
Precision/completeness of common approaches
symbolic execution - precise but incomplete
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 5 / 15
Precision/completeness of common approaches
symbolic execution - precise but incomplete
static analysis approaches can be complete but imprecise
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 5 / 15
Example - symbolic analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 6 / 15
Example - symbolic analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 6 / 15
Example - value-flow static analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 7 / 15
Example - value-flow static analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 7 / 15
Symvalic analysis adds dependencies
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 8 / 15
Symvalic analysis adds dependencies
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 8 / 15
How does symvalic analysis work?
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 9 / 15
How does symvalic analysis work?
datalog-based analysis rules
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 9 / 15
How does symvalic analysis work?
datalog-based analysis rules
top-down reasoning - solving equations
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 9 / 15
How does symvalic analysis work?
datalog-based analysis rules
top-down reasoning - solving equations
bottom up reasoning, up to bounded expression size
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 9 / 15
Completeness and soundness of symvalic analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 10 / 15
Completeness and soundness of symvalic analysis
neither sound nor complete
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 10 / 15
Completeness and soundness of symvalic analysis
neither sound nor complete
aim for a good balance between completeness and precision
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 10 / 15
Completeness and soundness of symvalic analysis
neither sound nor complete
aim for a good balance between completeness and precision
incompleteness - overapproximation, but prefers concrete values
(in favor to precision over completeness) not guaranteed to
model all values in real execution, but values that analysis
considers are likely to be realizable
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 10 / 15
Completeness and soundness of symvalic analysis
neither sound nor complete
aim for a good balance between completeness and precision
incompleteness - overapproximation, but prefers concrete values
(in favor to precision over completeness) not guaranteed to
model all values in real execution, but values that analysis
considers are likely to be realizable
precision - aim to get high precision without losing scalability
avoiding state explosion symvalic analysis computes
dependencies only on small subset of variables, therefore the
analysis can be imprecise (false positives)
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 10 / 15
Domains of analysis
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 11 / 15
Domains of analysis
t, u, v ∈ V, a set of variables,
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 11 / 15
Domains of analysis
t, u, v ∈ V, a set of variables,
fun ∈ F, a set of functions,
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 11 / 15
Domains of analysis
t, u, v ∈ V, a set of variables,
fun ∈ F, a set of functions,
i, j ∈ I, a set of instruction labels,
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 11 / 15
Domains of analysis
t, u, v ∈ V, a set of variables,
fun ∈ F, a set of functions,
i, j ∈ I, a set of instruction labels,
n ∈ N, the set of natural numbers.
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 11 / 15
Instruction set
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 12 / 15
Notation used in rules
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 13 / 15
Analysis rules
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 14 / 15
Analysis rules
P. Šimovec ·Symbolic Value-Flow Static Analysis ·November 19, 2021 15 / 15