uh now I talk about this scary topic of
formal
verification when people say formal
people usually talk about formal attire
formal speech formal
ceremony p uh
but the formal informal verification
comes from formalized
mathematics uh in usual
mathematics something is written on
paper
and the mathematician read it and she
gets an idea some idea and she can say
perhaps correct but
boring in formalized mathematics uh
something is written in computer file
and the Machine Vis
it the machine has no idea I guess but
it says correct by just looking at the
form of what's written
and this for is what this form
mathematics is
about this is great for smart contract
verification because usually when you
try to prove smart contracts correct
it's a massive case analysis if any data
is sent from the quer if any value is
sent from the C if the center data
matches function signatures or not um
what's in the storage but not in the
storage so it's massive case analysis
and usual mathema to
be enabl to read read it because it's
too boring for her
um for proof on um so this foral for
something you can access it on Twitter
you can so there is a b it's here it's
IPC board uh you can send a message you
can tweet to it uh you can send a
formula and it says provable or not
provable and when it's provable it shows
you
some roofs in a figure did you write it
the IPC uh a friend of mine
okay but
this the same figures are there in 1934
this is originally a German technology
by
the um every mathematical
Lans have um and then yeah the the
figure there was this thing that thing
so there are rules
like um so it's called
and introduction because on the upper
side there's no and symbol on the bottom
side we have an and symbol and it's it's
saying that if you have a proof of a and
if you have a proof of B you have a you
can construct proof
of and this
is and you can remove
this this
is so on the side we have an
uh on the bottom part you don't have it
and when you have a proof of a b you can
have you can construct a proof of
uh if you wish whichever you wish and
similarly there's all when you have a
proof of R you can construct a proof of
R order B from
it um so this guy is great because G
this system and this is still used today
this is the most common proof system
used today this is the Bas basis of
H and almost all modern LS no I went
back
sorry yes so there are good rules and
bad rules uh
[Music]
this they are good rules because they
don't allow you to smuggle things into
your proofs when you have a proof of a
then you have a proof of B you can get a
proof of r b but the only thing you can
do with it is to introduce b or R and
you already had it in the beginning so
nothing new happened here but on the
right hand side right side there are bad
rules uh it's called TK TK introduction
is the same as or introduction you have
a proof of a you can have a proof of a
tonk B and tonk elimination is the same
as and elimination and when you have a t
b you can get a proof of B and this this
rules allow you to smug the new
propositions into your proof and you can
prove foral from truth or something like
that and it's all about Harmony of
introduction and elimination and
then um what would be the pro rules
imper rules for solidity programs and
here I meet a
problem because usually okay people read
solidity code and get an idea and says
this works or this doesn't work but um
who who told you to who told you that
solidity programs are executed from top
to
bottom that 3D documentation does not
say might be bottom to top
maybe you say from experiences you
tested lity codes and so on but then you
are actually ring on the compiler
so well so the problem here is you when
you read the solidity code you might get
a different idea from what
happens actually when you compile and
deploy the code so I chose just to use
the solidity
compiler as my guidance so the solidity
compiler knows the meaning of a solidity
code I get an EV B code then I meet a
similar problem what are inference rules
for no ebm B code then actually I can
answer um rules would look like this um
when if you
know if your
EDM machine is at the second
position and the set stack element is 0
[Music]
x60 if you know this state does not go
wrong then from this you can imper
that Anan machine at the first position
with stock empty does not go wrong
because the only thing it can do is
either go out of gas or go one step to
the original the second position I about
so this kind of inance rules are good
for
machine I cheated a bit on why did
I treat solidity and the virtual machine
differently and it's because just if
there is a spec or not and if the spec
is written in a more machine readable
way it's better uh there's one
programming language who spec
authorative is written for theor provs
it's called
KPM that's the best language to prove
programs on and then there are some
programming languages for
spefications are translated into proof
Checkers C
11
JavaScript there are some languages with
speak with mathematical definitions
maybe they are easier to translate into
proas and there are language for English
on the specs and so on
and I found the evm a little bit or
maybe more easier to deal
with of course um
there are problems in the evbm
specification the paper so I I've been
opening some requests to the yellow
paper repository but this is manageable
and this is manageable I knew that
because many client implementers already
looked at it and found problems
and the document is
arrived uh so I just had to implement
another I virtual machine in
aover uh it took like 50 pages in type
set in a papers but it's kind of easy so
hope removes the top element of the
stack and changes the the B the St is to
the TA of the St and
so and then when you want to verify a
program you have to past your program in
proof Checker this there's nothing deep
in it it's just huge and you you just
have to copy and paste it actually this
POS some problems in the proof check
isabo because
um yeah looking up an instruction from
this this took so too much time so I had
to transform it into a binary tree
but it's just
bureaucracy and then this is the most
important question when you want to the
formal verification in the end what do
you
want and you have to say what you want
and uh the first option is the account
should do expected things and for that I
have to interview the people who wrote
this and what we expect
and this is not easy because the
question is very informal what do you
want but my requirement for the answer
is very detailed I have to type it into
a proof Checker so I ask a very informal
question and I expect a very detailed
answer and that's uh not easy to conduct
um at least I have to show something
working before I do something so the
second choice is the account shouldn't
do things wrong and usually for smart
contract the balance shouldn't decrease
unless an authorized account there
so and with this a non-authorized
account cannot make itself authorized or
make any any anybody else authorized
because that's kind of makes the first
point meaning
this uh so I have to type these
conditions in the proof check it's it's
straight for
um the us more but yeah
here saying um the storage index zero
does not contain the cor's address this
part is for non
authorized and the the contract is still
marked active and so on under these
conditions the expectation is that the
balance does not decrease I tried to to
prove this Mon and I failed because
I forgot to say one condition in the
precondition so I forgot to say the
account is still active and then the
proof fails so I know that something is
wrong um and then after typing in your
requirement what you
wish um you have to prove that thing you
um this is just straight forward
you you you you have to type things on
the upper pain and the lower pain is
just the machine's respones and here the
machine is responding some very long
proof gold but I find a ni sentence in
the middle of the go saying okay well
now it wants to do case analysis on if
the Cent data is empty or not empty
actually whenever you try to verify a
smart contract generated by solidity
it's the first question the Cod C data
is empty or not um so I tell it do a
case analysis on this and it splits the
cases and then I have to prove two
goals if the Cent dat is empty the
requirements hold if the sent data is
non empty the requirements hold and with
this with the usual inference rules I
get the result so I have to just repeat
this case analysis until all cases
finished and then the post conditions
hold and then after I finish this
um okay now the machine is convinced
that the the hold um there's still a
question does this match the reality um
I the next thing I have to do is I have
to test my own evm
implementation against the usual
standard virtual machine
tests for which um CPP client uh go CLI
and last all variated so they were
compared with the standard test and I
have to use this virtual machine test
to try
my evm implementation in this theorem
Pro if this is wrong I and this this
theorem is garbage because it's uh some
about some other machine so I have I
really have to do
this um if you think you can do
better there will be a workshop about
actually this is not just about program
verification this is