thank you
corrupted good afternoon everyone and
welcome to this talk about sacrify
Sakura is a smart contract verification
tool which was developed by the people
that you can see on this slide
it was developed at ETH Zurich which is
leading Technical University in
Switzerland and you can learn more about
sacrified by visiting the various links
that will appear in these slides and I
will make the slides available
afterwards after this talk so first let
me let me tell you the reasoning behind
Sakura Phi and motivate the creation of
Sakura Phi so most of you are aware
assume in this room of the various
security flaws that have plagued the
theorems in the beginning so the most
famous one remains the dowel bug which
eventually led the developers to do a
hard fork of the chain so as to river
the state the state change is created by
the attackers another more recent
security flaw was a multi security bug
which resulted in 30 Millions
in a theorem robbed by by attackers so
let me go into details of this second
floss more more precisely so it was a
case of in privileged right storage here
I have a really simple example of this
kind of flaw so just keep in mind for
all the examples that are going to come
that these are meant only to illustrate
the flaws and not are not meant to to
have a real logic in themselves so as
you see here it's really a toy example
so this is a wallet contract which
contains the storage viable honor which
specify the owner of this wallet and
there are two functions this
initialization function init wallet
which can change the honor and this
withdraw function through which the
owner can actually withdraw money so you
can see here this works so you can see
here that there is actually a check to
prevent anybody else from from from
withdrawing money but the problem in
case is that anybody can actually change
the the owner viable which is a problem
since because it makes the check useless
so this is this is in a sense the the
mystic peyote bug that is you allow
anybody to write to your storage even
though you rely on it for crucial
operations so of course the exploit in
the multi sick party bug was much more
complicated because the contract itself
was more sophisticated but the basic
vulnerability is the same so there are
many more security bugs that are
possible with the etherium platform one
of them is the category of unexpected
ether flows for instance when you expect
ether to go to your contract but don't
provide any means to withdraw it so you
end up with locked it ether in your in
your contract in secure coding such as
the mystic party bug so providing ways
to write your storage without checking
whether the user should be able to do
that or not the use of and safe input
whenever you use for instance timestamp
or block numbers and pretend that these
are random variables and even feed them
into cryptographic functions for
instance to create a pseudo-random
generator then this is bound to failure
because these variables can be biased by
miners so for instance a miner can
decide to not to process your
transaction right away and this is going
to be delayed by at least one block
which gonna result in a higher timestamp
reinsured method call so this is
basically the DAO bug and manipulating
ether flows by a transaction reordering
so this is a bit specific to the a
theorem platform where all the
transaction can African where all the
transaction can can be processed
concurrently so for the details of this
one I have another toy example this
token contract where you have two
storage variables one is the price of
this token and the other is the the
owner of this contract and so you can
set the price where only the owner can
can can change this price and
the second one is a cell token where
some ether is transferred as you can as
you can see here a user can can call
this function according to a given price
so what happens in practice that a user
can read the price variable on the
blockchain everything is public and you
don't even you don't even need to create
a transaction to read the value of this
variable but what happens here is that
once a user decide to call this function
the owner can still call another
function so what would happen is that
the owner would realize that there is a
transaction pending with this this
function and then this side okay maybe I
want to increase the price or lower the
price depending on what he wants to do
so the thing is when you have a
transaction pending you have no
guarantee that it's going to be executed
within the context that you that you
just read and so in a sense the two
operations do not commit and you
shouldn't expect them to commit either
so how to detect this kind of bugs I'm
going to talk about automated security
analysis as a way to make sure that
these bugs are not implemented in your
contracts so if I were to draw a big
drawing of all the possible behaviors
and I would I would have some something
with all the possible behaviors and
within them a lot of security bugs that
you want to avoid when implementing
smart contracts the problem is that you
cannot enumerate all possible behaviors
for instance if you have an earning an
integer argument in your function it's
going to be you cannot call this
function with all possible integers and
just say ok this this trace is faulty so
at one point you have to make a trade
off and decide how to to find the bad
behaviors so the different security
analysis approaches that you can have
are here represented so the first one
would be testing where you actually try
to cover one path and from this one path
you can extract one trace and try to - -
to check whether or not it's faulty and
whether or not it corresponds to what
you expected
dynamic symbolic analysis which is an
improvement on basic tasting because
you're not able to cover way many more
paths so this is a bit testing plus
purse if you want and so you have the
same kind of guarantees that is testing
and dynamic analysis report through bugs
that actually exist in your in your
codes and say they provide you with
traces of what happened and put the can
still miss bugs because your evolution
of code coverage which is not equal to
100% so this is a problem because you
can never be sure unless you have caught
you have covered all your on your codes
and that is 100% coverage you can never
be sure that your code doesn't contain
any of these bugs and the last one in
the focus of my talk today is automated
verification which makes a different
trait of that is it can report false
alarms but it has no missed bugs so it
is a current state of the art for the
Ihram platform what do we have what
tools do we have and why do i suggest
today so on the testing side we have
truffle in populous which are
respectively JavaScript and Python
frameworks and help the developer to to
implement that constructs and associated
test and deploy them efficiently on the
local dead chain and this way that
developer can run these traces and check
their assertions in an efficient manner
on dynamic analysis sad you have a Yenta
which was just presented in which allows
the developer to cover when many more
many more paths in his code execution
and on the automate automated
verification side we now have sakura
Fida i'm presenting today and which as i
said makes a different trade-off that is
it provides you with strong guarantees
at the bug that you are trying to find
doesn't exist in your code on the other
hand it can also report that the by the
bug might exist in your code and then
you have to look at it on your own and
tell whether or not it's it's here so
this is really a different trade-off
from the two previous categories so if I
were to summarize sakura in a few words
I would say that Sakura is fully
automated one click for more
verification system for a 3m smart
contract so I prepared a short demo and
so I hope it's gonna work so this is
recorded so here you have the interface
of Sakura Phi you can see that by
default there is some example of
solidity code so this is the website
itself so here you have a some solidity
code that you can input tech so that you
can verify it afterwards you can also
feed some byte code or you can also
input the address of a contract already
deployed on a main chain so the thing to
keep in mind here is that Sakura
actually works on byte code so even if
you give solid it could what is this
gonna do under the hood is this gonna
compile this code and work on the EVM
code so now if we look at this simple
example of a simple bank you can see
here that you have a storage variable
balances which contains the balances of
the users you have a deposit function
which allows a user to the pose to
deposit some money and you also withdraw
function so there are many things that
are wrong with this code and I just want
to show one of the code so here you can
click formally verify and your you know
have a security report with various
patterns that are checked or not so the
ones that I'm interested in right now is
gas dependent reinsurance II so
basically basically the DAO bug so if we
click on the the matched line to find
out where the the faulty code is we're
gonna see that here there is actually
some ether which is sent and some
storage value which is which is set to
another value at after the course so
this means that the attacker through is
fallback function can call this function
and this dysfunction is gonna be
executed within the same state which is
the DAO bug so one one solution for this
Posey's bug in this particular example
is just to remove this line and put it
before which is a quick and dirty
solution let's say so if we click
formerly verify again we're going to get
another security report and in that case
you can see that the pattern is not a
gun check so you have made sure that
your contract is no longer a victim of
gas dependent s dependent reenter NC and
this is a strong guarantee that is
you're 100% sure of that there is no
national code coverage here or they said
that the code coverage is 100% so
another example now is this flow the
wallet contract so here you have a
storage Bible which is owner which is
the owner of the contract so this is
example I showed earlier you you can
initialize the owner of the contract
through the first function in it wallet
and the second function allows some
transfer of ether if the message sender
is the owner so we're not going to try
to to get the security report out of
this contract so if you remember it's
the multi sick party bug so you see
different patterns and here the one that
I want to focus on is I'm privileged
right to storage so I explained it
earlier this that you allow anybody to
write to your storage without any check
so if we click on a match line we're
gonna see that the faulty line is where
you assign the owner to another viable
without any any check so here's a
solution that we can that we can use and
that work that was actually used in a
multi-state party bug was to have a
modifier only honor which is gonna make
sure that the function will be actually
executed only if the
if the message sender is the owner so
basically having the same check as you
had in this function but for the
initialization function so here you
click formally verify again and if you
look at the patterns nights it's safe
and so now your contract is guaranteed
to be to be deprived of any and
privilege destroyed to storage one last
example quickly is that of the token
with the changing price so this is a the
other transaction reordering example
that I showed earlier where you have
this set price function through which
the owner can change the price and you
also have this sell token which is meant
to be used by the by the user so if you
click formally verify you can see here
that the that that transaction may
affect either amount so this is a case
of transaction reordering because the
unknown that can be sent depends on on
the variable which is not constant so
here a quick fix would be to just decide
that the price is constant and remove
any ability to to change the price in
the future so if we click formally
verify again we can make sure that this
pattern is checked so of course in that
precise case it it removes one feature
of the of the of the contract that is
changing the price so you will need to
do a bit more to keep this feature
that's it for the demo
so now let's talk a bit about what's
under the hood of sakura phi so first as
I said earlier Sakura fireworks on the
EVM code so you can exit the idiom
binary that you obtained for instance by
combination of the obvious solidity code
and using this Sakura is going to obtain
an intermediate representation this
intermediate representation is only
meant to be easier to process by static
analysis the static analysis provides
you with a set of basic facts about your
code for instance you have you you know
that this variable is a constant or you
know that this variable is a balance and
so all these basic facts are the number
0 of your iterations that you can run to
have more and more facts so basically
you have a set of inference rules that
is for instance if a is a constant B is
a constant and C depends only on a and B
you will know that that C is a constant
as well so you can imagine this sort of
infants rules that we have in Sakura Phi
to obtain more and more useful facts
about the code so iterating over this
you finally obtain a set of facts which
is a fixed point with respect to these
inference rules and so from from all
these facts you can infer the security
report that I showed to you earlier and
which so basically you match the facts
against patterns security patterns so we
have a few now and we hope to increase
the number in a coming in the coming
months so what is what is important to
remember here is that you this is fully
automated that is the only thing you do
is at the beginning providing the source
code of of your contract and then
sacrifice is gonna do all this part and
provides provide you with the security
report and this is easily extensible
because you can add new patterns along
the way so in our experience so far it
was easy and quite quite quick to add
new patterns because the the platform
provides any sufficient primitives so
our hope is that we won't have to modify
sacrified that much in the future to
provide to provide a new new patterns
so following this experience we Sakura
fine automated tools to analyze smart
contracts a story was created in
Switzerland to audit block chains and
and smart contracts and the loop is
really between auditing contracts and
seeing the common patterns and try to
extract the the routine out of it and so
this is release this feedback loop that
we try to to maintain to develop new
tools that will they will improve on the
current state of art so you can check
out the information about chain security
if you're interested on this website so
to summarize a presidency clarify which
is fully automated provide strong
guarantees that is when it tells you
that you're the bug doesn't exist they
didn't means that it really doesn't
exist in your contract and it's also
extensible via a domain-specific
language to create new patterns using
the primitives already implemented
following the experience we secured if I
contact chain security was was created a
startup that specializes in audit of
small contracts and automated program
analysis and with this thank you for
your attention
[Music]