[Music]
so I guess we all agree that uh it's
really really hard to write 100% uh
correct
code regardless of whether this is a
smart cont contract or any other piece
of code and but what does it actually
mean to write correct code what what is
the word correct mean and uh I think the
the best explanation is that uh code is
correct when it does exactly the same
thing as the the programmer intended it
to do so the the mental model of the
programmer about smart contract or about
the the program is the same as the what
the the actual machine does with the
program and for ethereum uh this extends
even more because we do not only want uh
the the expectations of the programmer
to match the actual program but we also
want to match uh want to match the
expectations of the user to match the
the actual execution of of the
program and so how do we get to that
point uh and there are of course several
uh well established techniques and one
of them is to to to uh yeah write use
testing unit tests
um and that that's quite easy easy to do
you just think about uh a certain input
and make up your mind about what you're
expected to happen and then run the
program and see whether that actually
happened and that's good to to check
whether uh desired behavior is actually
there but it fails to show that under
desired behavior is absent so you cannot
use unit testing to show that it's
impossible to uh withdraw money from
your smart contract by a malicious actor
and the reason is because you would have
to check all possible ways to call the
contract and that's an uh infinite
number uh and yeah testing can only do
uh Finly many cases
uh let's let's so yeah and but there's a
solution to that and it comes in the
form of formal verification and let's
take a look at an example there so this
is an this is an easy token contract
which has a balances mapping and uh a
function that allows transferring uh
yeah balances from one account to the
other account there is a tiny error in
there and not sure if you see
that and I would argue
that so yeah testing can detect that
error but most people probably won't
think of this specific input that is
required to trigger the test or trigger
the trigger the
failure so
uh yeah what's the problem
here it looks correct but uh it probably
also will work correctly for most of the
token contracts out there but what it
fails to test is whether there's an
overflow in the in the in the two Fields
so if
uh if the amount you want to transfer
and the amount that is already there in
the Target account sums over 2 to the
256 then we get an overflow there and uh
the the mechanics don't work
correctly
[Music]
um yes so uh
and formal verification allows us to ask
questions like uh is the sum of all
balances unchanged by the transfer
function considering all possible states
of the contract and all possible
possible inputs to the
function
next so how does it work in general
um so you you provide formal statements
formal mathematical statements about the
the behavior of a contract and then you
use mathematical proofs to show that uh
the code satisfies these statements you
can do that manually but since we live
in 2016 there are there are of course
automated provs to help you there and
find the the mathematical
proofs um but
so one thing I want to stress here is
that formal verification is not a silver
bullet the reason is that um
so the the source code so a programming
language is already a formal description
of a program so and
adding adding formal statements in
another
language uh or completely formalizing
the behavior of a smart contract will
not really help because as I said in the
beginning it's all about the mental
model of the humans so um the
the key goal in using formal
verification is to reduce the complexity
of the smart contract we use source code
uh to describe how an algorithm works
and how a smart contract works and then
we use formal verification to describe
what it
does and the idea is that this what it
does is easier to understand then how it
does
it and another another great uh thing
about formal verification is that we can
ask questions about the behavior of the
program so it's not only about
formalizing it in in a kind of a
specification but we can also just add
to that and ask questions like is the
sum of all balances fixed and if there
is some way to modify the balances so
that the sum is not fixed between two
calls then uh the system will tell us or
uh yeah we can also ask questions like
will I smart contract get stuck so is
there any way to uh to send messages to
the smart contract to call functions in
a way that at some point it's not
possible to move forward in the in the
states of the smart contract or it's not
possible to to get the money out at all
anymore so uh yeah form verification is
coming to ethereum there are
already uh a lot of research papers on
that topic um
and the reason for that is that
blockchains are actually a paradise of
Home verification because uh yeah the
the model is that simple but uh U later
will tell you more about
that um okay
and formal verification tools also exist
for kind of a common languages like C
and Java and Adda and uh
these there are and the way it works for
these tools for pharmacy for Kato and
for spark is that you write your your
program in the the ordinary language
you're used to like like C and then you
annotate this uh source code with uh
formal statements so like solve balances
is a is fixed between two function calls
and then there are
tools which compile both the source code
and these annotations into to a language
that can work with the annotations this
is often Y3 uh and more recently we have
fstar and then um automated provs are
used to verify these formal statement on
the translation of the source code let's
take a look at an example so this is
this is from a
c and you see
that no no pointer um so you see that
there at the top there is a block of
comment with these formal statements and
then at the bottom you have regular C
code and uh you also have comment inside
the C code where you can refer to uh the
state of the program at that
point
so yeah let's not get into detail there
and uh yeah now uich will take over here
it is here he is and uh so uichi is uh a
formal verification engineer who
recently started at the etherum
foundation and he will focus on uh
extending the formal verification uh
features of
solidity hard yes
uh so Christian started this solidity to
Y3
translator um that's similar that flami
but for the smart for our smart contract
language
solidity I extended the framework so
that it can deal with the arrays and it
can deal with the simple token contract
with just one transfer
function um the contract itself is easy
um it has a transfer function
uh you can specify the from address to
address and the value and some balances
are changed um this is the same thing as
Christian showed before um it has the
same problem with the buffer over no
integer
overflow um the tool correctly complains
if I don't specify that the total
balance is less than a certain big
number otherwise the to complains
next slide please um when the smart
contract has a problem we see a window
like this um this is Y3 GUI Y3 is a
front end for dozens of automatic and
manual theorem
provs and on the left side you see lots
of conditions
desired conditions like no integer
overflows no buffer overflows and so on
you see many green chicks the green
chicks are on the verified conditions
and Y3 can automatically verify most of
the properties but you also see some
blue question marks the blue question
marks are on
unverified conditions uh wisely still
doesn't know if these blue questioned
properties hold or not um when you click
on one of these question marks on the
right pan you see a yellow highlight on
the suspicious piece of code um the code
is a translation of the solidity
contract into Y3 yml language that's a
language for Y3 and here the highlighted
line is uh
subtraction um so in this case this
might underflow um and when you see such
a problem you can either modify your pro
program or
annotate your program more and more um
annotation is like putting assertions in
the program and if you put enough
assumtions
to um satisfy the automatic provs the
automatic provs will say green check but
in many cases you just find problems in
your specification so it's about
adjusting your own mental model next
slide
please
um so before finding slm I was looking
for a place where formal verification
actually makes sense um before the I
joined the research institute my job was
to spread the formal methods into the
industry but I didn't have any access to
any company's source
code so it was hard for me to do that so
I joined a company that hired former
verification
Engineers that was a US company I had
eight colleagues writing proofs were a
wonderful
environment but I I was not happy
because our proofs were not about the
real
thing um the fundamental problem is the
real CPUs come with documentation
2,000 pages long and nobody has ever
translate translated the whole thing
into any theor and provs so that was a
huge problem we couldn't solve um I
found eum I saw the eum virtual machine
I saw the yellow paper the specification
uh it has only 32 pages long and I I
thought I can actually translate this
thing into a theorum Pro and I can write
proofs about smart contracts I was doing
that and I was posting the partial
results on vit and Christian found me
and I ended up here
um
so the V machine is wonderful because it
has a small specification and this small
specification really matches the reality
because all clients try really hard to
match this specification otherwise one
of these clients would behave
differently from others and that's the
worst thing they want so they really
want to be conformant to the
specification and a small definition
that that matches reality is the
fundamental necessity for formal
verification engineer I found it in E
next slide
please um we have some future steps um
so when I'm extending the solidity wi3
framework um there are some immediate
problems like or we don't have the Cora
instruction yet in the ation or we
cannot deal with mapping to mapping in
Y3 in a short and elegant way um because
of this we are thinking of moving to F
star fstar is something similar to Y3
but it has more advanced
features um I want to thank Microsoft
for open sourcing F star and also G3 smt
solers and we extensively use it um
thank you very much
um but feature wise um we have more
problems to solve than just verifying uh
one solidity
contract
um I think we are moving to many small
contracts than one monolithic big
contract so we have to be able to reason
about multiple cooperating cond contract
[Music]
and and then just reasoning about
solidity code is not enough because what
runs on the blockchain is not a solidity
code but a compiled B code and sometimes
the compiler has a bug so somehow we
have to know how the bite code behaves
whether it's evm or the evm 2 the second
one um
so somehow we have to do that but um
that's easier than most CPU
architectures out there so I think this
is a solvable problem um the next one is
uh multi transaction conditions So
currently the precondition post
condition in variance on the contracts
uh just on one
cord um it can already deal with the re
entrance but uh from the first call to
the last return and that's the range of
verification we need to extend
that um and then yes and combination
with offchain protocol um this is harder
because the moment we get off the
blockchain um
people's behavior or yeah are not
constrained
by clear rules so what's good for people
is not very well defined but somehow we
have to Def Define a game where it's in
the players's interest to be to
coordinate with the rules
um and the formal methods can help here
because it can explore all possibilities
of interaction
um the last point is rather practical um
so you saw some blue question marks but
just a question mark is sometimes not
enough for me to understand the problem
so it would help if we can see counter
examples like with this input with this
state this is broken and then um it's
more easily
understood um
but I see I believe
many more formal verification
researchers are coming to the
verification of vum smart
contracts because of the reason I
mentioned thism virtual machine is V
Paradise for formal verification
engineer thank you very
much thank you
[Music]
Yi and