foreign
[Music]
yes so this came out of like a fun
project I wanted to write like a full
like an end-to-end
um symbolic execution engine in solidity
with including the the solver that we
usually use in the in the background
and this is actually pretty fun so I
want to share with you what this does um
so a few questions for like audience
adjustment who yes who here was at
Harry's talk yesterday about
symbolic computation in your
okay who knows what symbolic execution
is
okay nice I am prepared to tell you what
it is though for the ones who don't know
so I'm quickly going to go over some
slides and then we're going to move to
code this word or these expressions are
thrown around a lot like what symbolic
execution what's constraints what's sn2
silver what's all that stuff and
a lot of people know what it is but if
you don't know what it is they kind of
like you feel left out and these words
are used very
um trivially even though they're not
really they're simple but not trivial so
first I want to tell you what's not
symbolic execution
and that's concrete execution so let's
say you have oh yeah last question who
can read assembly like this
nice okay that's very good
um so let's say we have this assembly
here from evm and we want to run the
concrete execution over it
so let's say we have this call data
um it's 12 in hacks I don't know what
that is and what is that in decimal like
20 no
18. yeah it makes sense
so if you run this program without call
data what do we get
um what's like there's no return here is
let's just consider the top of the stack
as sort of a return
in this case we get a 12 we're going to
push zero
um and the stock could call data load
that position we get to 12 push three
multiply that's going to give us 36 in
HEX we add one so we get this number top
of the stack right so this concrete
execution you have a program you have a
concrete input and then you execute the
program that input you get an output so
now what is symbolic execution we just
said what's not so t11 actually has a
pretty good explanation of what it is so
it turns the program into math and then
solves math formulas
that's actually a very precise although
very vague description of what it does
we have the same program here but now
instead of a concrete called Data we're
going to have a symbolic called Data
what does that mean to be symbolic is
that you just use a variable instead of
concrete number that's really all you do
you look you keep looking at variables
so our entire call data is going to be
CD now it's just a variable the top of
our stack is going to be a variable
called top that's all we're doing so
here we're going to collect constraints
which are things that must be true when
we run the program so
when we run call data load of zero we're
basically doing CD of zero right and
then we can also call it X we can call
it side we can call it whatever it's
just a symbol
um and it happens that that thing must
be greater equals zero because we're
trading we're dealing dealing with evm
words and they're unsigned right the
second part is that we are assigning
that to X we just make a variable out of
out of that when we do the call data
load next thing we have this
multiplication we can make another
variable for it called Y which is now x
times three finally for this ad we can
make another variable for it called top
and then which we just did the previous
top of the stack which is y plus one
um so you see that for every operation
we add a new variable we add a new
symbol that represents that expression
and we collect all these Expressions so
we end up with what we call these
constraints and this is what is our
symbolic encoding so we take the program
in evm bytecode and assembly here we
transform it into a set of constraints
and that's our symbolic encoding they're
different there are many many different
ways to write these constraints from a
program
which means we have different ways to
symbolically encode your program
why do we want to do this so we
obviously walking code is going to turn
into a system of linear inequalities so
this was our set of constraints
that's going to turn into the system of
linear inequalities there are equalities
here but they can be very quickly
translated into inequalities
um so we just keep them as they call it
for Simplicity
and why do we do this the reason why we
do this because we know how to solve
these things with algorithms that you
might have seen in high school or
University or you still will see it when
you finish high school and what can we
do with it we can for example did the
same thing we did before we can give a
concrete call data in this case the same
called Data as we we had before and run
it symbolically what does that mean
we're gonna in this case a simple
substitution does it we can substitute
CD by
visitorical data which then substitute
CD of 0 by 12 and so on and we get
at the top is going to be this number
when we solve that with gal Jordan
illumination or Gauss elimination or
there's tons of ways of solving it a
simple substitution here will do it not
only gives us the value for top it gives
us values for every single variable in
this system we could have read it that
it before with the concrete execution so
the cool things we can do with this we
can ask many many things so you can ask
for example can top be greater than 10
000. how do we ask that we simply add a
constraint that represents that
statement in this language so can top be
greater than 10 000 basically gives us
this constraint here and then but here's
the answer it is possible in which case
such a solver such a math solver will
tell us that the system is satisfiable
meaning that there is evaluation for
every single variable in the system that
makes this the the the set of
constraints satisfiable it is possible
that all the constraints are true at the
same time and it also gives us what we
call a model which is the actual values
that make the whole the whole set of
constraints valid and similarity before
we have a value for top and and we also
have values for every single variable
that appears in the in the system
we can also ask n top be zero
what do you think so we can represent it
for this constraints pretty simple by
the way where all these variables are on
the integers there's no reals or
rationals here everything's integers
um in this case this oversized the
system is unsatisfiable it's
inconsistent there's there's no way all
these constraints can be true at the
same time they may be true in separation
but they will never be true
um at the same time what we want to do
is basically
do exactly that in solidity so but what
exactly do we want to do
you can do several things you can
try to prove that a certain assertion is
true you can prove that a certain thing
always happens or never happens kind of
things
for our use case we're going to try to
find unreachable branches so here's a
piece of solidity we're going to analyze
the VM byte code but this is just to
show an example
so we have this functional X and integer
X and first we require that X has to be
last or equal 10.
then we have the branches as if x slash
or equal 50 does something and then the
rest does return is false
so this Branch here basically the false
branch of the f
it's unreachable right because
ax we know that X is less or equal 10
from the beginning of the function
which means it's always less or equal
50.
meaning that it will always enter the if
and it will never come to this part of
the of the code so if you take the true
Branch this is reachable because these
constraints are
together
but these are not right so if x has to
be less or equal 10 it cannot be greater
than 50. so this branch is unreachable
we can remove the whole thing well not
the whole thing just the the bottom the
cool thing about trying to do that stuff
is that we need very little support from
the evm of course if you want to write
if you want to write a symbolic
education engineer to write an
interpreter in the first place right you
need an NVM interpreter
but we don't want to deal with every
object because it gets really big really
complicated and we don't want to do
things like call create and storage and
all these complicated stuff which of
course you could and a lot of tools do
that we don't want to do that in
solidity the cool thing again about this
encoding we we only have to care about
the stack operations
um control flow so it jumps and
opcodes that stop the execution
and relation upgrades
and so basically we're going to Care
mostly about as I saw before ifs with
relation operators inside so less than
greater than and the negation of these
so that you can get less than or equal
and greater than or equal the symbolic
encoding we're going to use is also
pretty simple
so for every evm expression that we saw
before we're going to transform it into
math constraint of the form a minus B
less or equal K where A and B are going
to be variables and K is going to be a
constant so this is also what Harry was
talking about yesterday in in his talk
and we got things like like this for
example whoever was in Harry's talking
together is this uh system satisfiable
yeah so if you sum everything on both
sides then you get basically zero last
Oracle minus two which is a
contradiction so this system is
impossible to be satisfiable
um the reason why we like this encoding
is because
we can use a difference logic solver and
again as Harry explained yesterday a
difference logic solver is very simple
to write what does it do it basically
takes these constraints these math
constraints and it tells you
whether it's possible or not that these
things are satisfiable at the same time
and if it is possible it's going to give
you values for the variables that make
it satisfiable otherwise it just says
it's not possible at all for these
things to be satisfiable together
um the solver is much simpler than the
things you need like ILP or smt when you
need to solve with linear combinations
or even non-linear expressions and the
sorts of things that you end up with
when you start encoding arithmetic
expressions and other things and as also
higher explained yesterday this runs in
employ normal time
on the graph generated from the
constraints using the volume four graph
algorithm not going to go much into that
if you want to learn more about that
please re-watch
um Harris talk
and this algorithm is super simple this
is basically almost the whole thing and
most of it is comments um so now all we
need to do is
put it all together so this is the whole
project
so these are two tests files one for the
solver itself just like you need to test
for the solver and one for the symbol
execution engine and then you have all
those files for the
um for the whole engine
so
what we want to do is like write an
interpreter how do we write interpreter
we need so by the way please if you have
questions just like try to you can ask
questions right now just to make sure we
we go and um in a good flow
um actually it's not here so usually
when you write this interpreter for evm
you have this context what is the
context you have the code that are
executing you have the program counter
like what which upgrade are you
executing right now we have a stack in
our case it's going to be a symbolic
stack
um don't worry about that now
we have a path which basically it's a
it's a path of all the program like of
the program counters that were visited
in the in the jumps and we're going to
use this to detect loops and exit
because we don't want to encode loops
we have
um an array of constraints this is what
I showed before like when you see the
require it says require a class or equal
10 we go into that Branch so we keep
that constraint because that thing needs
to be true for the rest of the execution
um and this counter variable is just a
um accounted to help create new
variables so when we were creating new
variables for the Expressions X Y and Z
and so on here we're going to be
expression one expression two expression
three and so on and they need to be
different in the branches that we
execute
so that's it we have the context
um ignore the rest for now let's jump
right into the
execution engine so we have this
recursive function called run from
which takes our context so here you see
it's basically gonna Traverse all the up
codes select the opcode
this is just a check
um that we just exit early in Loops we
it becomes an under proximation but we
don't want to do loops
we extend the path
with the Disney opcode
and here is the part that the first part
of the what I mentioned with The
Interpreter we need to care about Stack
Up codes
because they're going to add some
numbers and a bunch of different things
jump locations jump destinations that we
will need when when building our
constraints
so this just does the usual
um stack handling so if it's a swap
you're gonna go into the stack and swap
the numbers if it's a dupe you're going
to duplicate whatever it needs to
duplicate it if it's a push you just
push that number into the stack
here the only thing we do is apply
a function on
the stack arguments which is so for
example if you have an ad we're not
going to encode the ad precisely here
but we do need to consume the stack
slots and put a new return value there
right so this basically just uses these
handlers we have internally it's like a
bunch of function pointers
um
to if you have an ad so this is generic
for like all the all the up girls we
don't care about it takes the number of
arguments this op code takes pops all of
them from the stack creates a new work
what we call symbolic variable so like a
new expression 13 or whatever here and
puts that expression on the stack
um and we don't really have we don't
really care what it looks
um what it looks like right now we don't
really care what kind of constraints we
have over it
and and here's a part of the that we
actually care about the where we do the
check so if we have a jump every time we
see a conditional jump
we take the the argument of that jump we
take the condition that makes it jump
and we ask the solver is it possible
that we can't jump to that location
because this is before we had this this
required an if right so we have require
access or uh
X Plus then or equal to 10. so we have
that saved X must be less or equal to
10. and then we see if x greater than 50
and then we ask is it possible though
that is that X is greater than 50. so at
this point that's when we
um
we have all the math things encoded
already in here
as you'll see this make symbol this is
like internal helpers not important
right now
so here's where we
do the check
so we check if the op code is relational
so if you have a less than or greater
than or if it's an e0 because if if we
needed a greater or equal we don't have
greater or equal in the VM so we need to
do is zero
um less than right so and similarly for
um less than or equal so if it's one of
these we basically take the the
condition which is here we transform it
into an DL expression difference logic
expression
um and basically call this over so we
have this check here which will take all
the constraints and we'll call this
little DL server that I mentioned
um
which and this is the check
we call this over and if the server says
unsut then we say this branch is
unreachable why unsat because if the
branches if the branch conditions are
unsatisfiable
together it means that
um the silver will say unsatisfiable
right and this means that that part is
not reachable because there's something
in in the middle that is not allowing
that will not make the code the code the
code path is basically going to be
inconsistent
um and what the silver looks like is
yeah this is the entire silver
so you take the constraints so here you
just build the graph so this is built in
the graph here you just need to know how
many variables you have
um this is still building the graph
and then Here We Run The this single the
single source for this path algorithm
which is the first part of the solver
which is basically yeah it's a very
basic graph algorithm then we did a
negative cycle detection and that's
really all the silver does this is and
20 lines of code it's really simple and
um
yeah it's a it's a logic that I really
like because it can do a lot of things
while being very very simple
um the last thing that I want to show is
how do you use this so
here I have this contract unreachable
that has a bunch of functions and that's
like some unreachable branches in each
of these functions
all we need to do to test that is really
just this we call the Sim run function
from the library from the symbolic
symbolic execution Library
with the runtime code
from the contract that's really all and
here's a simpler thing just like
manually
um just a simple test
with somebody care that I know what it
does and if you run this
yeah so here you'll see that
um this is the complicated case with all
the solidity high level functions and
it's not the best way to report the
things but it reports it emits an event
that says unreachable Branch with the
pc255 this tiny example so it's this is
the same as I showed in solidity just
like in written quickly in yule and this
is the bytecode
that it generates
um well that I wrote manually and
um
so we can quickly
compute This Together keeping track of
the stack
and then you see what it
what it actually does in execution so
push zero
we're going to push zero then we just
called it a load of zero it's going to
give us some X
then we push 10.
we duplicate the X
we do less than so this is going to turn
into this
this is the stack by the way
and the top is the higher position so
now we push tag 0b
and we do the like a conditional jump
where the false Branch stops so we don't
care about the first Branch all we do is
just so you're gonna pop
um we're gonna pop this first two
arguments right because of the jump but
because we go into a branch this
condition must be true for the rest of
execution right
set of constraints
so we keep going in tag one jump Dash
dup we duplicate X again
we push 50.
we do an LT now
and which consumes the X and this
becomes top of the stack just a symbolic
expression like Y equals X length less
than fifth less than x
we push 14 and then we jump 2 and then
at this point when we see the jump we're
going to ask the solver is it possible
that this new condition 50 as an X is
consistent with what we already have X
less than 10 and it's always going to
say that's not possible and at this
point here precisely at this jump I
that's where we basically stop and say
this Branch here is is the true Branch
like where you're jumping next is um
unsatisfiable so you can actually remove
that entire Branch right
but yeah so
there's a lot of code behind that
there's a lot of helpers the main
intuition was basically this algorithm
of just like run an interpreter caring
about if you're killed not caring about
other up codes
and yeah I'm happy to take questions
uh super cool talk this is wild you can
do this in solidity I'm wondering about
overflow though uh because your
researching at the beginning was that
that one example you showed was
impossible but it is very possible in
the presence of overflow no that one
wasn't because you need the answer to be
minus one-third so it's not going to be
possible
um okay sure yeah but it doesn't look
like you handle overflow anymore yeah no
right yeah exactly so that means that
your results are not correct yeah
exactly there's a bunch of soundness
stuff you have to add to this okay all
right thank you sorry I didn't see but
is this code somewhere available to uh
yeah this repo github.com
um that thing and there's probably bugs
in there though so feel free to fix them
um so since you wrote this in solidity I
do you have any thoughts on why you
would want this to be executed on chain
not at all okay
should not run this Unchained yeah well
actually so if I wait let me quickly
just look how much gas this takes
for this tiny program
you said that for a given program
there's a lot of different encodings you
could have can you give a few other
ideas of other encodings and what would
be the trade-offs
yeah so this encoding uses
um this encoding basically chooses which
has a difference logic because the
solver is very simple so we could write
in solidity right so the the encoding is
tailored to become systems of
inequalities that look like the
constraints that a DL solver would take
but where is it now
um in Harris talk actually which I have
here
there are different
so if you wanna if you actually want to
encode add mold div all these kind of
things you will need more complicated
constraints like linear combinations
where is it Harry
yeah you'll need linear combinations
like this for example and more
complicated constraints and you'll need
like a Simplex or integer linear
programming thing or
even in non-linear is over depending and
these things are a lot more complicated
so Simplex is well it's
it's an exponential algorithm that kind
of happens to run mostly in polynomial
time these days but in all linear
non-linear Earth if you're trying to
solve nonlinear constraints that's an
undetable problem and you're going to
have a hard time solving it so