Formal Verification of Smart Contracts - Yoichi Hirai

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