yeah he's heading Leo work with on
foundation aetherium foundation on the
solidity team doing language design work
and compiler work and also doing formal
verification which is what this talk is
about I'm going to talk about so ladies
SMT checker which is a formal
verification component that gives
compile time results about safety safety
checks so have two questions so how many
people here are a solidity developers
okay cool and how do you feel about
audience participation okay cool you
asked how so request the answer is
you're gonna help me solve this so I
want to first introduce what is SMT
what's why SMT checker so the SMT comes
from satisfiability modular theories and
Assam to solver is a tool that will take
a formula like this a first-order logic
formula and try to answer this questions
can we find integer values for a b c
such that this formula when we
substitute the values for these
variables evaluates to true so just two
I can go together over the formula just
to give a little bit of context to
whoever is not familiar with electrical
activity this kind of things okay so
it's a boolean formula right it's a
conjunction of constraints so this
formula kind of returns true or false
right a boolean value this constraints
are satisfiable together or not so first
we have this part of the formula which
basically says it's kind of like a
function definition right so there's a
lot of same sex abuse here but we're
gonna ignore that for now so this says
that for whatever acts f of X equals x
times 42 okay the next we have two
constraints over the input variables we
chose so we're saying that a has to be
greater or equal B and B has to be
greater or equal C and then last
we applied function f we defined before
over a and C saying FFA has a be greater
or equal F of C so now the question
again can we find integer values that
evaluate the formula to two true yes
okay can you give me values for ABC yeah
so now you told me that it's possible
right it's possible to give values for a
B C such that the formulas true 0 0 0
does that work it works right zero
greater equals 0 true same thing for BC
f of a 0 F F is f of C 0 it's true right
but unfortunately that's not the one
that I had here so anyway so this one
works right also this one works and this
one works how many do you think how many
solutions how many different sets of
values for ABC do you think we can get
for this formula infinite right now a
slightly different question what happens
if we change this we could change the
comparison of FA and F of C to this and
repeat the question is there a set of
values for ABC that make the formula
true so there's a consensus saying no
and that's correct and when that's the
case we say that the formula is
unsatisfiable
because there is no set of values that
satisfy the formula so in the previous
case were satisfiable now we have
unsatisfiable and why did I choose this
formula could have chosen many other
formulas so the reason is we can read
this formula in many ways right it can
be just a logical formula but this
formula happens to we can't we can also
read this formula as this part here
highlighted right now being a property
we want to prove
to function right application of the
function that part being local
constraints say on input variables and
here basically a function definition so
this is basically how we just prove
correctness of this smart contract here
we have a function definition which
would be encoded in the SMT language as
the first term of the conjunction here
we have two local constraints right that
evaluate that or encoder Tory as those
those circumstance and here we have the
application of the function but you will
probably notice notice right now that in
the code I have assert F FA greater or
equal F of C because it's a property I
want to prove right and here in the
logical formula that we give to the SMT
solver it's actually last then so it's
the opposite operation right the reason
why we actually ask for the opposite is
if this is unsatisfiable if we try to
prove the negation of the property and
the solver says is unsatisfiable this
means that there's no behavior there's
no values for local rivals with that
encoding that actually break the
assertion right so in this case the
solver will tell me it's unsatisfiable
which means that certian is safe again
because there's no way you can go
through the program and break the
assertion so for all cases you can ever
come up with the assertion is true but
let's change a little bit so is that
assertion true is that assert correct
for every input it's not right so for
our query to the SMT solver we negate
the property right so I want to find
values I want the SMT solver to give me
values for my variables that actually
break the certian so one FFA to be
different from F of C and in this case
the solver will tell me it's satisfiable
and here are some values and this is
exactly the output that solidity
compiler will give you at compile time
when it's Y when you run exactly that
code
so here we see that compilers say
assertion violation happens here for its
assertion for a1 b1 c1 c0 sorry so the
SMT checker as a summary after Jack
symbolizes saw it's a SMT based so we
use SMT solvers so it's an SMT based it
smart contract form of verification
framework it's built in a compiler which
is for us one of the one of the big
advantages compared to other ways to
formally verify your code the way it
works the way the approach our approach
is that we encode program logic from
solidity into SMT statements and use SMT
solver to run those queries that I just
mentioned and we use those to check for
assertion failures overflow underflow
trivial conditions and reachable code
and all of that happens automatically
when you run the compiler one
characteristic of this approach which is
close to from the fortification
community called bounded model checking
is that this approach is sound but not
complete and what that means is if it's
sound which this approach is whenever it
says the assertion is safe it is
actually safe but whenever it says the
assertion is not safe here's a counter
example it might be that might be not
true so you might have to verify it and
see that this this might have been
caused by an abstraction of some
unsupported features or functions which
is the case for our approach but then
being sound but not complete also gives
advantage that it's pretty fast and
light compared to other approaches and
it gives useful counter examples because
it's applied directly on solidity code
instead of EVM bytecode which then you
would have to map back to solidity
program variables which doesn't
necessarily work so here's some other
frameworks that have been already in
indigo system for for some time in EVM
formal semantics I'd have Isabel and KVM
which are
or KVM specially is pretty established
as a really good framework for
fortification of smart contracts it's
more expressive but it also means that
it it's harder and takes longer to give
you proof so these two approaches have
pros and cons caleb is a really nice
debugger for a cape for K proofs wit and
they will have a workshop tomorrow so
make sure to check that out for a vm
byte code verification there are tools
like int me through in mayan which do
symbolic execution on the byte code and
try to find bugs basically and there
were other projects that were
translating solidity to language that
were whatever verifiable like y3f star
and zoos that with LLVM if I'm not
mistake so how do you use it you just
need one line of code right now it's an
experimental feature it's a very
experimental feature right now so if you
use it you will find internal compile
errors they will find and supported
features and all kind of things but we
are working on it to make it of course
much more usable and hopefully
non-experimental one day but then the
next question is how do I actually use
it so if they just insert this line of
code there then sure it's gonna enable
the run of destiny checker but what is
it what is actually doing so you need to
write formal specifications right so
whenever you prove your program safe you
only prove it with respect to
specification at the regional proving
anything so you need to specify what
properties you're actually proving in
solidity or with the SMT checker you
don't need anything extra you use the
normal require and asserts from the
language itself so requires and asserts
in a compiler or translated into runtime
checks right when it's compiled to
bytecode but here in the SMT checker we
use them as as the formal specification
so ease requires as assumptions and
asserts as verification targets so
whatever conditions you write in a
require the SMT checker has been assume
it's true and whatever you write has had
an assert it's going to try to prove
okay so how to use a require actually so
there's a lot of debate for quite a
while already on requires and asserts
and when to use each or what it what
which one means so I just copied it I'm
gonna read it from solute docks the
require function should be used to
ensure valid conditions on inputs and
contracts a tribals or to validate
return values from calls to external
contracts so here in this example we
have a contract that has stayed forever
a a bunch of functions G and H which
suppose like that we don't know right
now what they do and we have this
function f that takes an integer X so
here we're using requires requires two
filter values for a and ax right so we
want for some reason a to be 0 and ax
would be less than 100 then we sum both
we put it in a and then after that we we
know that al as then and 100 is true
right because of the requires before so
if you want to prove that the last
statement should actually have been a
require sorry in a certain order require
because it requires just going to assume
it and with this with the assert we're
actually using passed knowledge to prove
a new property about your code in the
end of the function so what about
asserts the third function should only
be used to test for internal errors and
to check invariants a properly
functioning code should never reach a
fail in a search statement and this is
really important if this happens there's
a bug in our contract which you should
fix same example now just using asserts
everywhere
can we assert a equals zero over there
very likely not right of course it
depends on what what G and H are doing
but if we don't really know what it's
doing
we cannot say assert a equals a because
they can be whatever right and
especially for ax here if you say assert
ax less than 100 it's a public function
so anyone can call this function with x
equals to a hundred and your assertions
already wrong right so this is really
important to notice like you should only
assert things that you're really
are true at that moment for every single
execution path that rich is that point
and here the assertion is correctly
placed at the end because the new
property are proven yeah yeah this
moment yeah so for example we have I'm
gonna talk about this later but if you
call an external function for example
which don't have control over or they
know the code then when a function comes
back we have to reset all knowledge
about state variables right because you
might have this contractor called might
have called your contract back which
changed a so you can't really keep the
knowledge about it
but yeah but modular verification one of
the research goals that we have is to
actually infer properties from different
functions and see what state invariants
we can come up with automatically this
is not done yet but it's under to do
list what about false positives so I
mentioned earlier that the approach is
sound so if it's a safe it's safe but it
gives count it gives false positives
which is basically false counter
examples so your assertion might be
correct and safe by the tool says it's
not safe why does that happen it happens
because we have to abstract the encoding
sometimes so for example for complex
types and functions say like
cryptographic Elections we it's not our
approach not expressive enough to
actually implement it so we have to use
symbolic variables on on the application
of the function and that's as far as it
gets so we don't really know what the
actual value of the function call is
going to be so in these abstractions
might lead to false positives also if
you call external function if you do if
you yeah I call external functions we
might have you we do clear the knowledge
after the call after a function call so
it might not have been the case that the
that state variable a got rewritten
but you never know so to be safe again
we have to clear the knowledge also the
contract state invariants you as the
developer of the contract might know
that certain properties are valid
throughout your contract but the SMT
checker is not yet smart enough to
deduce those properties automatically so
and one point that I wanted to mention
in this talk is you can actually help
the SMT checker you can help the tool to
actually find it proofs and it's a very
simple way to do it you can flood your
code with requires so every assumption
even very simple things that you know
are true at that point even if it's if
even if it might sound redundant to you
it might help the solver because the
more constrained to give the last false
positives the tool is gonna it's gonna
issue so I'm gonna run a couple examples
right now think of how like eight
minutes
can everyone read not in general but
screen what I did push yeah and it sorry
this one like okay so this is like a
very tiny token and not very interesting
so we have a map in with balance
constructor initializes the balance of
the message center with a bunch of
tokens and accounts can transfer tokens
which other right so there are few line
a few extra lines in this piece of code
right compared to normal token
implementations so first of all this is
a normal one right we required that the
message sender actually has the amount
in their balance but here I'm actually
storing the old values for the balances
for the person sending the transaction
and the person receiving and yeah the
person received the account receiving
the amount here the balances are updated
right and here we have an assertion that
says that the sum of the balances before
the transaction before the operations
have to be equal the sum of the balances
after the operation oh sorry
yeah this should be the right assertion
but I want it to break so okay so here
the tool tell the compiler tells us the
assertion is broken and gives a bunch of
values for for our variables right so
but there's something weird right so
it's saying that it gave zero to both
two and message sender which commonly
people prevent right so we can just add
that here I want message sender to be oh
this is actually gonna work so I'm just
gonna say they have to be different it's
fine if there is zero
so okay now it changed right so two and
two one before was zero mass percentage
to zero but that's fine because they're
different and the assertion is actually
saying that the balance before was
greater than the balance right now which
means that some tokens vanished right so
the assertion is basically saying every
time there's a transfer tokens vanish
which hopefully is wrong and the tool
set is wrong can say balance from plus
balance to is actually the same as
balance of serum plus balance of one
which are the accounts so if we actually
fix the assertion there you go if
there's no if it doesn't complain it
means it's safe I'm gonna move on to
it's likely a better example with a
bunch of false positives oh not this
this okay so here we have yeah this
contract see this there's external
contract this matter for now oh sorry
about that it's not the one I want to
show this one so we have just like kind
of an account but some it stores the
some the balance of like it's its own
balance and here it counts how many
transactions how many times the fall
back function was called increasing the
value increasing the balance of this
account so here we have the fall back
function that says that the value sent
to be greater than zero and this is just
to give a constraint for an avoider if
cause later requiring that this account
cannot have more than 1 million the
balance cannot be greater than 1 million
so here we just increase the sum and
increase account right and here we have
a function called average that computes
the average the average value that was
sent per transaction
all right so here I put is required
because if if there was no transaction
doesn't make sense compute the average
but here we have an ax so here we
compute the average and we assert that
the average has to be greater than zero
right because if you did have a
transaction because of this line we
cannot compute we cannot we don't count
zeros in a transaction so the assertion
is true agreed
okay so it's telling us that the
assertion is actually not true and give
some value so it says that if count is
one and sum is zero then the average is
zero which is correct right but then the
question is can this ever happen can
count can it have ever happened that
count is 1 and sum is zero why
exactly so message Valley is an integer
right with this require is a message
value is actually at least one here and
count only increases by one so this
property here is true right
it's an invariant it's true like at any
point of the contract right but it's
hard for the SMT checker to figure that
out on its own and that's what I meant
with you as a developer of the contract
know this kind of thing then you can
help you can help destiny checker by
adding those invariants whenever you
have these harder checks let's see okay
now it's fine so I have one last example
which was the one that actually closed
here yeah it's the same it's the same
contract just with the extension that we
have this exterior contract and we call
some function f next we know contract
and what what happens here is that when
we call the external function the
knowledge gets basically erased and you
would need to add new constraints after
the after the after the function call
you maybe even need to repeat
unconstrained sue in order to help us
over to actually prove it and not get
false positives
and one last thing that I wanted to say
is future plans that we have for for the
tool yeah we have more examples and I'd
be glad to talk about the tool more
offline if you guys want I want to talk
about it as future plans we have what I
mentioned which is this sort of function
modular verification part which is kind
of involved with the state invariant
automatic deduction which is a very hard
thing to do but we want to try it anyway
and also one other thing we want
introduced rudder soon is actually the
ability to let that developers give this
variance so something like you could
write something like declare your
invariants and this would be one of them
and with this invariant is invariant
would be applied as a require in the
beginning of every function and asserted
in the end of every function in Diani we
could even use that to get inductive
proofs and yeah just get give more power
mm jacquard and actually get harder
properties proven anyway even though
they're pretty hard so yeah open for
questions not sure how much time there's
left yeah no time left so we can discuss
offline time is gone thank you
you