Testing Your Code on Arbitrary States (aka Formal Verification)

Transcript

so the next speaker is yaroslav bendik who is a researcher from sartora and he's going to be talking about testing your code on arbitrary States AKA formal verification please give a warm welcome to yarislav thank you thank you for the introduction uh can you hear me you can hear me right um so uh I want to basically show you how you can use formalification to improve the security of your code um I'm sure that we have heard about many bugs that have appeared they might have appeared in small contracts they might have appear in big contracts in many cases they led to losing millions of US dollars but it's not just about

money the contracts are losing trust of the community packs are issues and I think we all agree that uh we're going to get rid of a box we want to prevent bugs from being exploited from being even appeared in the smart contracts and the question is how to achieve this there are many techniques that are usually used like testing fuzzing everything you know these techniques these techniques are actually used also in other areas of software development process so like testing is used in almost every software company right but in this talk uh we are not talking about these classical techniques we are talking about formal verification and familiarification might not be so well known and it might not be so widely

used it is the case but I hope that uh after this talk uh you will see that it has some value and it can be beneficial to use it especially in the area of D5 so what is formal verification um there are many definitions this is one from Wikipedia and it says that formal verification is the act of proving or disproving correctness of algorithms with respect to certain formal specification using some formal methods in mathematics important parts here are proving or disproving this basically means that you should get some guarantee mathematical guaranteed there are no bugs but what does it mean no bugs this is the area definition formal specification you need to properly without any ambiguity Define

what are the properties that you want to verify then you verify it so if you write wrong specification and you run some form of verification it says there's no there are no bugs might not be the case because you might have wrong specification so you need to write specification and then you can apply the formal verification and the specification is not written in English it has to be precise okay so um there are many myths and claims about formal litigation maybe we have heard about these I don't know how much you know actually about foreign can be only used to prove things or that the artist problem is

computational meaning that follow irrigation does not scale for real programs okay because you are really providing this guarantee there are no bugs like no execution can lead to a buck another claim um you get a bulletproof code if you run from verification or claims that formula replication can replace auditing or testing or that you apply for verification once at the end you are done pretty cool and then you verify so these are some claims maybe myths and during this talk I'll try to shed some light on this and yeah deliver is the reality at the end of this talk good um there are many existing tools that are using some kind of formal methods this

slide is showing just some of them and you can classify this into two groups one can be called proof assistance and basically these tools are for instance Isabel Daphne cook cake uh they can be used to uh prove very interesting properties of your program but on the other hand the user has to be very experienced so you need to know how to use these tools you basically go over your code we are providing some lemmas about neural instructions in our functions in the code and then you can prove complicated stuff but it takes a lot of time okay and if you change your code you need to adjust the improve so very powerful

tools but hard to use on the other side we have a fuzzing and static analysis tools so these tools are easier to use they are running quite quickly the user does not need to really know how these tools works and yeah if you change your code you can just run it all again and it gives you some quick answer but these tools are limited in some sense they can give you some positive sorry false positive or false negative answers meaning like they tell you there is a bug but it might not be a real bug or they might miss it back they are not exhaustive okay and at our company we are developing something called certain approver they

are trying to be somewhere in between so basically our Tool uh should give you the guarantee that there's no back but the hard part is that the user does not need to know from verification but the user needs to write a specification so you really need to understand the underlying contract and you need to properly specify all the behavior and all the possible bugs that might happen you don't need to say like Alex is stealing 1 000 etiers okay but you specify some properties I will show you some examples later so in the rest of the talk uh I will illustrate how formula orientation can be implemented

following the example of software program the input of our tool is uh your program and some specification and the output is either a execution of the program that Viral is the specification or you get some mathematical guarantee that there's no violation and since this problem for notification is quite hard we are really checking every possible executionary program then uh sometimes it I'm out this problem is really hard we are trying to find the box or give you recruits but sometimes you time out it can happen so uh two things to explain now um how to write a specification and how does detour work so let me start with the

specification um this is a simple uh solidity smart contract example um that is back in this example so let me just briefly explain this this code we have some mapping uh called balances so this is basically like storing the information about balance of literal users or the smart contract and then we have these two functions transfer take some address from and some others too and some amount and it should transfer the amount and then we have another function balances off we just take some address and tells you the balance on that address another question is what is wrong about this uh about this function transfer so let's just explain how it works we

require that the from account has at least amount which makes sense if you want to transfer that amount and then you compute the new balance from the New Balance to store it to some variables then you upgrade your balances using these two variables so what is wrong can we see some back in this function didn't go wrong right so uh this is actually back that uh appeared already several times and I'm showing this one because uh one of our customers just introduced this back

uh in their like it was not in production it was during the development this customer is using our tool so they are writing some specification and running a tests during CI okay so we have a row that can catch this back that's why I'm talking about this one and here in debug is that uh if you send money to yourself you can increase your balance and yeah it's because you first compute the new brands like you're adding the amount and then you decrease your Burns but then you override it again so I hope you can see this Behavior okay and now the question is how can you find this bug using R2 so as I said you need to write a specification and this specification might not be saying that

when you send some money to yourself you will increase your balance it might be saying something else but it should reveal this back okay so here's the rule that was used in the CI tests um what is the rule so our specification consists of several rules every rule is like a single piece of specification you want to verify with our tool okay uh this rule is called the sum of form and two balances stay the same so basically it is saying that if you execute the transfer function then the sum of balances before the execution and after the execution is the same so no tokens Can appear basically or disappear how does it work um

you say that you have some address too and you have some amount you are not saying what is amount we are not saying what is the address just that we have some address and some some amount then you say that you have some uh environment e what does it mean this basically represents the solubility Global variables like message sender message value block time stamp okay so we are basically saying we are at some state of the smart contract we have some amount we have some address too then we compute the sum of balances of message sender and two okay by calling the solidity functions and then we call the transfer so we are transferring amount from message sender

to two and then we check that the new sum of these two balances is the same as before the transfer and our tool is basically checking if there is like any assignment to to amount e that violates this assertion okay and there is one in this case not just one their money okay and then Alice is one of these examples because the initial sum of Alice is 14 like 7.7 and then after the um transfer it becomes 24. so this rule will be violated and it can get you to understanding this kind of example okay

um let me show you another example so this is something like a generic uh boiler applied how to write specification in our specification language so typically it goes like this um instead you are at some state of the contract so you have some like message sender message value um you have some storage State you do not say what is the current state of research storage then we can have some requirements some assumptions about the message sender for instance or about this storage so you might for instance require that there are at least 10 accounts in your smart contract okay energy sum of balances is lower than 100 you can have some assumptions then you invoke some function from solidity and this function might return some

value some X for instance then you connect some requirements some assumptions about the result of this execution like assumptions about X or assumptions about the storage that was changing because of the location of the function then you can call another function for instance maybe using the same e variable maybe you can Define new variable so you have like two people that are calling this smart contract and they are somehow interacting and then again you can require something about the execution of that function and at the end you have one assertion or maybe with more assertions that are talking about the effects of the execution of the function like in case of Alice okay the sum has not

changed so you kind of like arbitraryological reasoning about the effects of the interrogations of the functions and yes I said before R2 check this for arbitrary value of e arbitrary values of you know state of the smart contract but we follow the requirements that you provide and this is not not everything uh our verification language can you know allow you to do more crazy stuff so you can Define some Hooks and goes these are basically um you can modify the underlying solidity code so whenever you invoke some function you can go uh count invocations or functions or you can summarize some functions meaning you can

override some functions in solidity which might be very useful for instance if you are verifying some property that does not depend on some function you just override its function just say this is something simple I don't care what this function does okay you can use quantifiers like for every LS there is some John that does something if Alice already know you can have muffins meaning we are not limited to using 256 you can have arbitrary numbers and many other features and actually tonight we have a session of Thomas so this is all about the specification from my site today I would be happy to answer some questions after later but now uh let's see how the tool actually works

um so this picture summarizes the steps that we do to any verification and I will now go individually over these steps and just tell you briefly something about them the first step is that we take this solidity and we compare it to event bytecode and the reason is that different compilers produce different bytecodes they might behave differently with respective specification and sometimes the compilers even contain some bugs and we've actually identified some bugs that are fixed also because of us we are very proud of this but the important information is that we need to verify the bytecode that is uploaded to the blockchain to make sure that you know device order is used by our customer

and I might be saying like this is something not nice it's not nice so there is some drawback and the drawback is that if you find a violation of the specification we need to show to the user what is the evaluation like what is the execution of the smart contract so we need to map it back from the byte Pro to resolidated and this might be hard another issue is that the byte code is uh complicated it's not easy to read it is using so many basic instructions and this code is really hard to automatically analyze and we are trying to automatically analyze the program so even bytecode is not good for us and hence the next step we take this bytecode and we convert it to our custom program representation

and we call this one uh three other schools I'm not sure what we have heard about some three horoscopes before um and uh yeah is our custom one and um basically the three horoscope is using only small number of unique instructions and it's quite simple which means that it's easy to analyze and also if you can translate another language like Solana maybe two or three hours code you can run out to own it so there are other advantages of this good [Music] um other part of the input is the specification so basically we also think

the specification and we somehow merge it with the byte code and form together the three others code the program representation and we take the assumptions and specification put these associations to the tech program and then actually it's about trying to find so you're trying to reach and violate an assertion in data program this is the verification task now okay uh what is the next step um we have this stack program that represents the input basically and now we try to analyze it and simplify it using some static analysis so the goal is uh yeah identify user information so for

instance we run some pointer analysis for example if you have some two functions in some cases we can identify this that these two functions do not touch the same memory so they do not interact with each other and this can really simplify the verification process because you know that there is no interaction between these two functions or we do a program slicing or to explain this on an example sooner you also do some value range analysis meaning that you kind of you and 256 variable meaning so many possible values perhaps this variable is actually bounded in your program it's always between 0 and 10. if you get this information the verification is much easier because you don't need to assume so many combinations of values of variables so we reveal very important

information about the program and we also try to simplify it we change it so that it's like you know suitable shape for the following pipeline now the slicing example I don't know if you know what is program slicing so a very small example uh we have a program with two structures X and Y both have internal variable f x f is one y f is two then we change the value of YF to a three and then we have this assertion that XF is one now let's say that this is the specification already assertion is the specification and you can see that this holds I mean it's trivial program the program slicing is about observing

that the value of y does not matter it does not affect the assertion so you can basically remove this part from the program and you can work with just with this program it's equivalent program with respect to the specification so we are trying to do automatically these simplifications of the program before we continue with the following pipeline okay um good uh Next Step so uh we have this three Rs code it's a program it's really nice it's simple and now we generate something that we call verification condition so where is verification conditioner it's a logical formula you can imagine

like a mathematical formula some equations or some variables and this formula is satisfiable if and only if you can violate the specification and also the variable summary formal is somehow correspond to where I was firmly solidity and so if you get a like satisfying assignment of that formula you actually get execution of the smart contract that shows you the evaluation I'll show you an example later but the question is okay how do we build this formula let me state it in English so reformer says that uh there exists initial values of variables of the program suggest after execution of that program with those variables various values uh you follow the assertion

okay if this formula is true then you have the execution would balance the specification we are done um right but this is English we need to use some some logic gear uh the important properties I have said you need to ensure this mapping back to solidity so the like variables that will appear in the formula earlier have to correspond to variable family program and you'll also need to someone encode the execution like which branches are taken in the program which functions are called you need to encounter all of these so how do you turn the program into logical formula that's the question uh the answer is uh you have so much time so answer is very simple

and that's because the three hours code is almost a formula so uh let me explain it serious code means that you are using only three instructions per uh sorry three addresses per instruction so they are very simple okay uh second thing uh it's in a so-called static single assignment form this means that you cannot change values of variables in your program but you want to do that right so if you want to increase X by 5 you create a new variable X1 and you say that X1 is X1 sorry X plus five and yeah this now looks like a logical formula

like mathematical formula because you are not changing values of variables they have like a unique value not a unique like given value you can express the value of variable in different ways but it's like one value so assignments in the program looks like logical formulas right uh what else do we have several other instructions for instance branching so you have some condition if C doesn't do Branch a I'll do Branch b these are implications logical implications every condition holds then we perform a what is a maybe some assignments logical formulas right so this works and yeah then we also need to deal with loops and some assumptions some assumptions I will not cover these

but basically you can convert all the instructions from three years code to logical formulas and somehow compose them and then you form the sentence from the previous slide and you check it that's the idea okay uh so uh what is the next step in the next step we take this verification condition and we convert it to something called smt so SNT stands for uh satisfiability modular Theory and the theory might be integers reals it might be using non-linear operations linear operations so basically uh and then that tools that are syllables there

are solving like these problems expressed in SMD that was the difference between verification condition and smt the verification connection we we do not say how we represent the numbers if we use bit vectors or if you use integers and uh yeah in the smt we do and there are many solvers we are trying to somehow combine them communicate with them run these rollers in parallel so this is basically about maybe verification condition is algorithm smt solving might be program that solves your verification condition many people work on this at our company but I will not go into details about the SMD solving it's a different chapter

okay uh so we are getting to the end of the pipeline you successfully run the verification and you either have a proof or you have a back okay uh I'll be done no we are not done definitely not done um so what happens if you find a kind example this is an example of a report that our tool is providing so let me explain uh this is a report from the uh RS example like the transfer where you can send money to yourself okay on the right hand side you will see all the rows that you have verified in this case you're just dealing with one rule on the right hand side you can show the values of variables family specification

so remember in the rule you just Define some variables but then the tool is trying to find some values of these variables that would value the assertion okay so here you can see the message sender you can see the two they are the same it's some Alice and you are sending a five amount was five and this sum was 14 meaning that Alexis bonds was seven at the start of the at the start of the computation okay so this helps you understand a bit what was happening and then we have this call Trace so basically in the code Trace we first tell you what was the initial value of the storage what was the massive sender and so on and then we perform the actions from the specification from the

solidity and then we have the assertion so what can you see here um this storage so initially we had just one user in the account and it was just this Alice hair bronze was seven then if we Zoom a bit you can for instance see what was happening during transfer with the balance is mapping so we have loaded three times seven then we have start two because we have you know yeah remove the M15 and then we have start 12 which is the like wrong wrong result right this is evaluating the specification and this is how Alice got from 7 to 12 by just invoking the

transfer function this helps to understand the current example so uh are we done do you understanding an example in this case yes in general no and uh in practice the issue is that you might get the country somewhere it's not real and I have said that this should not be happening from verification it might if your specification is wrong because you need to specify what is the state of your contract so for instance if you think that the sum of balances never drops to zero but you do not say that it's not initial zero then you can value the specification so you need to specify correctly okay uh good uh so we are closing the maps now um formulation is used for uh proving things

it can be used to prove things but it's also very good at finding box violations uh second myth the biggest problem is to compute it sometimes we time out but the biggest problem is to try the specification this is really hard maybe easier than for modification but it takes some effort for verification produces bulletproof code no you need to write the right specification okay it's all about the specification from notification replaces everything it does not it's something else the front verification should be done just once at the end no way you should write a specification at the start as we have heard at the previous talk and then you should integrate promotification in your

CI and run it with every change of record because you have the specification and then it's fully automated once you have the specification you can just run it repeatedly okay uh so what is better how do you think for modification no one just just use both okay uh and this is my almost closing slide uh we hope that the community will start using uh our tool actually the company is already using our Tool uh we are organizing several competitions uh where you can actually join us you can start writing the specification we can give you some money if you write some specification that catches sandbox this might be real box might be injected box there's a guy how you can start using our tool how you can

align online specification and for instance it can also help you to deal with this HD flag that we have just started today you can use certain approver to solve these challenges and finally it's not just about competitions actually we have this something called pay as you go but it's like a trial version you can start using our tool without paying any money just use it try to find some valuations this is QR code please try it and if you have any questions reach me out I'll be happy to talk thank you [Applause] thank you Alice love that was some fantastic insights into formal

verification so we've run out of time for this session but yaroslav from suratura is going to be around for the whole weekend DSS so if you have any questions I'm sure you have a lot of questions on formal verification so please reach out to Yaris love he'll be around so thank you