🛠 Finding Bugs With Formal Verification: Hands-on Workshop - Yura Sherman

foreign [Applause] [Music] prover and tools and what is the idea of the whole thing our next step is to do something more technical to dive into how actually working with sir Torah looks like and we would like to explain you how to how to define these properties of the code how to give them how to feed them to the approver and hopefully we'll have the chance to actually use the tool and write rules of your own so like I mentioned before the part the Practical part will require Docker desktop and downloading our Docker image which might be a bit slow with with the with the Wi-Fi because many people are here but we'll see we'll we'll manage it so how will the workshop look like first we will talk about the sector approval technology which is uh mooli already discussed it at length from the from the high level high level point of view then we will talk about uh we will give some introduction to the CVL where CVL is the territory verification language is it's the rule that the the custom language that we use to define the properties to define the rules of how the code should behave and then we will dive deep after the introduction to severe we will dive deeper into into some civil features like parametric rules and invariants don't worry if you don't understand this terms we will explain everything in detail and after we finish explaining all the CDL and the features we will move to the exercise maybe we will have a short break and we have to install some the docker image for the exercise so the exercise will be you will try to really provide the erc20 token code and you write simple rules and basically you find this bug and then here's the idea that you can get a feel get a test of how it is to do formal verification just pretty interesting all right so let's start this example I said we discussed it how what does historical do so I will not talk a lot about it here is the good code so we will we give the correct code and the invariant total Supply equals to the summable balances we give both of them to the prover and the prover says it's fine the property the environment always holds and when we give the buggy code to the prover and with the same environment the program will find a counter example which is the self-transfer like somebody mentioned here 7 from equals to two then the property doesn't hold because kind of new new tokens are being minted out of thin air so everybody understand this part so now let's uh give a high level view of certain approver architecture how how the whole process works so like like we see first of all we take the smart contract code and the rules the specification how the code should work so there is some kind of transformation of the smart contract code we will not discuss that in detail and eventually the smart contract code and the rules they both are combined by the sertora prover into a VC and VCA here is not the Venture Capital it's a verification Condition it's a big logical formula that combines both the smart both the code and the and the and the rules and this huge logical formula is being fed into the into several open source constraint solvers now the job of this constraint solvers is to find the variables which do not do not satisfy the The Logical formula so when this set of variables it doesn't satisfy the formula is found then it's the counter example then it means that the rules don't are not don't describe the code properly so it means either there is a bug in the code or the rules are not written properly and if the concerned solvers don't manage to find any variables that violate the formula then it means that the formula is correct and it means the rules are correct that means that the rules describe the code correctly and we call that we prove the correctness of the code so this is the big big scheme how the how the circular prover is built okay so after all this abstract [Music] abstract diagrams let's dive in and start to talk about CVL how how actually we how we How We Do how we write this part so our idea in in this Workshop we work with the rc20 code which is probably the most common smart contract in existence and we want to start by proving that the transfer function works as expected right so this is this is severe this for most of you probably for your first view of the CDL and civil is very similar to solidity it's it's been it's been designed to to resemble solidity so that the solidity developers will find it easy to work with and this keyword rule is it's like like it says it describes one property about the code so what we want to express what do we want to express we want to express at them a transfer functions properly that after the transfer is called on the token then the sender's balance is reduced by amount and the recipient's balance is increased by amount so this is the basic structure of the Civil rule first we do some operation and then we describe the assertion we describe we assert something we describe what what should what should the state be after the operation has been executed or performed so here here we see there is all these variables but you know I guess we're all developers here so we cannot use variables without uh defining them or declaring them somewhere so let's see how we how we declare these variables so my balance will be balance of message sender which makes sense message sender sends the tokens and recipient balance is the balance of the recipient then we call we call the we call the transfer and with we check the balances again my balance after the operation recipient balance after the operation and we do the assertion right so if these assertions are true then it means we've proved the correctness of the transfer function we prove at least that the balances are increased and balances are handled correctly maybe maybe you can see something some some definition is missing in the code right anybody can see which variable is a just is mentioned but is never declared um yeah the contract also and the summons more some local variables we see the recipient and the amount they're not they're just mentioned here but actually the the compiler would not know what what is this variables so let's let's handle that let's let's let's pass this recipient and the amount as parameters to the rule so basically the rule is similar to a function syntactically and we can we can pass any any parameters to this rule so now when we use the recipient and the amount in in in the code to Smart contracts transfer a compiler knows what it is this parameter to the rule and the the various territory approver works you can think about it as if certain approver will try all the possible combination of these parameters all the possible amounts all the possible recipients of course it's impossible to actually try all the possible amounts it will take long time but because we use a logical formulas then we can think about it as if trying all the possible values here but there is still another thing which is not which we didn't declare and this is the message sender so what is this message sender how I mean we all know message sender from solidity but in civil it's just a little bit different uh before we talk about that we should mention that these variables like recipient and an amount they can also be declared inside the function inside the rule and it's a identical syntax just to different syntaxes to to express the same thing just to tell the comp declare this variables for the compiler so we see we can pass this we can pass it as parameters to the rule we can declare them inside the rule we can pass something as a parameter and declare some another variables inside the rule it's all the same doesn't matter so now let's talk about a message sender yeah so the actual syntax in CVL so in civil to refer to the environment variables we use a we use a data type called the EnV struct and this struct contains all this built-in all these variables that are built in in solidity so in solidity you can you can use msg.sender msg.value block number Etc in a CVL because it's not solidity it's not a it's different different execution model so we use this EnV struct and we we can refer to a message sender message value and block number and the others as fields of e of this EnV struct so Envy is the data type and E is the instance right so so to take the message sender balance we just say balance off e dot msg.sender we just have to make sure that the E is declared so the compiler knows what to refer to and another thing another thing where we another important way we use the environment we have to pass it to the to some smart contract functions yeah so when we call transfer we need to give it the environment as well yeah because the transfer is a is it depends on what is the message center value what is the message what is the MSG value what is damage descender so we need to give the environment and then what happens as a prover tries the transfers with all all different environments different message sender it will try everything uh so this so now so now a rule is complete but there is still something is missing what is missing is the Declaration of this smart contract calls yeah so we know that erc20 includes balance off we know that your C20 includes transfer but we also need to to declare them for the Civil compiler right so how do we do that we use a methods block so here is an example of a small methods block and in this methods block we have a declaration of a balance of now you will see some keywords that you're not familiar with from solidity which is env3 what does it mean yeah nv3 means that we declare functions that don't use the environment that they don't care about a message sender don't care about message value usually it's going to be view functions yeah like here we have balance off we have allowance this these are the functions they don't change anything they don't care about the environment so we declared we declared them in methods block as env3 and it means that when we invoke these functions when we call these functions from the rule we don't need to pass the environment of these functions that's why you can see here that when we call balance off we don't send the environment we just send this parameter with the address the you know MSG centered at the end of the day it's an address but when you call the transfer we need to pass the environment on top of the um the usual transfer parameters which we all know which is the recipient and the amount okay so now we wrote the message block now we have the message block now we have the rule and let's see what happens when we actually execute this rule with the sertora approver this is the output this is the output of the tool so when we run the when we run the rules it gives it it gives you a web page which is dynamically updated with the execution results and we see here we see on the left side then the name of a rule was trans transfer here it's it's called transverse pack it should be transfer and we see that the rule failed yeah we see this scary red scary Red icon so what could be what could be the problem in this rule can anybody say why is this rule why is this rule incorrect why is there counter example self-transfer um yeah there is a problem here with uh with self-transfer yeah because yeah maybe let's Let There is a problem with self-transfer but let's see how sertorial approver helps us understand the problem helps us understand the counter example so if you look at the local so when it shows as a counter example it shows what what is the what is the state of the local variables in this counter example so if you see if you see here we look at the recipient and we look at the message sender we see there one and the same yeah it's 0x401. so it kind of gives us a hint that the problem here is with self-transfer right if you zoom in on the local variables yes we see the same thing so the problem is yes that if we send the token to ourself the assertion says my balance after should be my balance before minus the amount but obviously if you send the token to ourselves my the balance stayed the same and this assertion is is incorrect so this is how the territory approver shows as a counter example in this situation of course the problem is not with the smart contract code the problem is with the rule it's just not written correctly it doesn't take the self-transfer scenario into account how do we handle that it's very common very common scenario and because a rule is mostly correct there's just one one situation where it's not correct so uh what we do we had the require you say uh let's only look at the scenarios where the message sender is not equal to recipient Let's ignore completely the scenario where message sender is equal to the recipient because it's not interesting for us and for this we use the require require keyword it's basically kind of a precondition yeah so here we have a precondition here we have the operation and here we have the post condition and when we were when we run when we run the rule with this requirement it will it will succeed because now it's correct so this is this for most of you it's the first first introduction to CVL this is how rules look like this is how we write the rules the event of a rule declaration variable definition methods block and what is the NVA variable so this is basic intro to civil uh congratulations now you you can you've already seen civil and know the basis of it now let's do something a little bit more complicated now let's move to another rule where we want to say that whenever transfer is called the recipient's balance always increases yeah so this we what we do is we take the balance before balance balance of the recipient and will transfer to some tokens to the recipient some amount of tokens then we take the balance again and then our our assertion is that the balance after should be greater than balanced before so I guess most of you already see the what can be problematic with this rule yeah when the amount is equal to zero then this this inequality will not hold here because the balance after will be will be will be equal to balance before so what do we do about that like we mentioned before we we cannot require yeah so we can you just require the Assumption we can we can say okay let's require that the amount should be greater to zero and then the sertora prover will ignore the scenarios where amount is equal to zero will not will not look at these cases another thing we can do is use an if statement which is a little bit clumsy but it also works so you say if the amount is greater greater than zero then balance after the assert button software is greater than balanced before if the amount is not greater than zero then we don't care we just return true but there is a but there is a more elegant way and civil to express this if statement and this way is to use an implication which we use uh basically it's it's quite common to use with civil implication is a logical operation which is not not present in solidity but it's very useful for assertions so just a reminder implication this is the truth table of implication yes so it's always true but only if false predicate implies implies true predicate then the whole implication is uh sorry if the true predicate implies false predicate then the whole implication is false it's true in other cases so this is the Syntax for implication and it's it's uh it's short and it's elegant way to express this kind this kind of assertions so we say if the amount amount is zero implies that the balance after is greater than balanced before I think we all can agree that it's more elegant syntax and more readable than using IF statements and it simplifies simplifies the rule because we don't need to use the requires at the beginning so basically we we com we use we define oral logic in this implication right but what happens when we run this we will still get some error and what is there yeah the self transfers that we had before when the recipient is equal to message sender so how do we fix there um yeah we can now we already knew know a few ways how to how to how to fix this kind of error so again you can you can add the require that says recipient is not equal to message sender if you could also use an implication uh it's not inside it's not in the slide but also implication could better here it just would make it a bit more clunky this assert in the end so basically implications like an if statement where the else block contains a third rule and just to summarize the ways to work with assumptions either there is a require as a precondition or we use implication in the assert okay so questions until now everything everything could everything seems clear awesome so now let's move to another syntax another part of civil syntax which is revert yeah so in general in general if we if we use the syntax that we looked at until now like precondition operation post condition the prover only looks at non-reverting path so if during the execution of smart contact it did the revert then the approver completely ignores this execution path it will only look at the passes where there was no revert so in this example this is a counter a bit counter-intuitive so let's let's look at this function Foo which reverts if the parameter is 10.

and now we we write a several rule which is supposed to test Foo so we we invoke full with the parameter with 10 and this is a third false so a third false of course means that the rule will will fail because you know false is never we can never assert false and expect true but the rules will succeed why because oh because when we invoke full this 10 it it always reverts so so the sector approval will always ignore this execution path and it will never reach this line it will never reach this line and the rule will succeed so this is a bit counter-intuitive part which important to remember that it all uh interesting question how do we handle try and catch thank you if the if the revert is caught inside the solidity code right so then we then the internal revert is equal to to normal reverts and then it will consider the reverting path right so we see that the approver normally will consider non-reverting Pathways but sometimes it's very important to to consider reverting passes as well so of course code sometimes you have to verify they have to prove that the code reverts correctly corrects when the expected to reverts when we expect it to revert and doesn't revert when we don't expect it to reward so how do we look at reverting passes as well so civil has a Syntax for that and the syntax is we invoke the function with this little addition add with revert so this this this this keyword is a comma is tells this tells the prover to consider all the passes both reverting and non-reverting and how do we know if this um function called reverted or not so we have this Boolean variable last traverted which is another keyword in serial and this Boolean variable just holds the result of the previous function call it's true if the previous function called reverted it's false if the previous function call did not revert so this is this is an example of a rule that uses this syntax so it says user must not be able to transfer more tokens than they own so what happens is first we have the precondition that says the balance of the sender is less than the amount right so obviously we cannot transfer more tokens than our balance right so this transfer should revert and then we call transfer this ill in invalid amount and we we expect we assert that this call reverted yeah that the last reversion is true again because the amount is is too large because the amount is larger than our balance um but uh when we when you use reverse there is a lot of small nuances because uh function May reward for for several reasons we expect it to revert because the amount is too large but it may revert for many other different reasons and it's important to remember when we work with reverting passes now we will look at different scenarios where the function where the simple function transfer reverse for many different reasons so first of all first of all when we execute this rule we will Okay so now now we do it a little bit different Rule now we say the balance is legitimate right if we transfer with revert and we assert that the call did not revert okay now the balance is greater the amount so we we're allowed to transfer this amount but we say okay let's consider the reverting passes as well as non-reverting and we assert that there was no rewarding because it looks looks good yeah we have our balance is good enough and we transferred we try to transfer tokens but we're still going to get a lot of rewards why so the first reverse will be because message value is zero is not zero sorry right because message value means there was some ether value sent to this function to transfer but the transfer is not payable right so it will revert because it doesn't know what to do with this either sent to it so normally when we don't we don't use this at with reward the proverb would ignore all these kind of scenarios but when we explicitly tell it don't ignore reverting passes it'll start it will find us all the possible rewards yeah so because MSG value is part of this variable of e and like we mentioned before Satori approving will try all the possible combinations it will of course it will try Eve is all diff all values of V including their message values one two whatever is greater than zero so here it reversed because message value is not zero okay so we fixed that we say require message value zero and we expect it to work but no it will not work because it now it will revert due to overflow yeah because when the recipient balance is too large is almost maximum and when we try to to send the recipient three tokens now we get an overflow and now because let's assume that we use the new solidity newer solidity versions which checks overflow by default so it will revert because it cannot it cannot add three to this you know Max unit minus one so it reverts again so now okay let's add this condition let's look let's add this precondition let's circuit balance of recipient plus amount should be less than Max urine so we don't get overflow but now we get a different revert and what is the different reward it says message sender is zero right because most of the Year C20 tokens they they do not allow transferring tokens from 0 or to zero and and certain approval is going is going to try all the possible values of environments so of course it will try the environment where the message center is zero because we didn't explicitly tell it not to try so now we have to add this condition require message sender is not equal to zero but it's still going to get a revert because the recipient is zero and only after we added all these preconditions now we can run the rule successfully and what is the point of all this the point of this is to explain that when we work with reverting passes usually there is many of them and sometimes there is more than we expect so every time we have to look why did we get this reward is it interesting to us this these cases are not so interesting so we just have to add a precondition and filter them out so there's a lot of nuance there's a lot of work involved with uh working with reverting passes it's more complicated yeah how long is the time to how long does it take to run a rule it depends on the code complexity so for example the simple erc20 code running a rule would take maybe 30 seconds or a minute but some when the code is very complex it can take it can take even an hour it really depends and the sometimes even if you can get a timeout like the prover might not be able to to prove the formula if the code is complex enough and then that's a very Advanced topic how to make the code simpler how maybe to split it into modules maybe simplify some code yeah it happens it happens often in real time real code not the demo here C20 token yeah is you mean the the message the no we don't have the message but we use this we use the trace call Trace and the variables to understand why I traverted so the summary of this revert and last reverted so basically when we use at with revert we tell the tool to get to the assert even we know when the no non-reversing passes exist last reverse that can be used to check situations it should reverse fairly easily and checking all this liveness properties is less straightforward like we showed we have to look at a lot of nuances and add a lot of requires it's common so another uh let's say check spot another another another if we finish another part of the of the explanation of civil so we went over transfer spec check addition of transfer rules transfer reverts transfer does not reward we've already seen example of four rules we look we explained the EnV variable in more detail and we explained with revert and last reverted and now Sasha will explain another another parts of civil and other civil features hi everyone I'm Sasha also work at Satora now continue jurors talk about other features of the civil and he explained you like he showed you like the properties that we can verify over the transfer but in ERC we know there are also many other things for example allowance and like how confident we are about the logins that it's correctly well it's RC and we know that it's okay but let's say you got a new token you don't know what what's going on there we also need to check it then we start to write a simple rule we start with the defining the rule then we usually prefer to start it slightly good practice from the assertion uh where you express your formula for example here we want to say that if allowance was changed then the message sender was the owner and pretty simple but also it can help you to understand what do you need for your rule for example we're definitely need to call a proof because the properties we want to verify is for now it's only on a proof we Define the necessary variables to call it and we made a call to approve itself and the only thing that's left is allowance before allowing software simple call simple rule if we run it in in our tool we will get it as verified but what does it mean in general and now it's the time to talk about the coverage it's like one one of the important property of our properties that we try to and to improve this part to make the coverage more like if the contract is covered like 100 as we know it's like the perfect it's not easy to reason about it but we try to do our best so according to that rule uh we can say is it that doesn't increase the coverage is it well written is it passing it's might be objective but we should do our best to improve the coverage and what we can say about our coverage of our allowance the good thing that we proved that it's like a proof is only called by the owner that's good but what about other functions there are many other functions and they can change allowance one approach is like the most straightforward but the most tedious you write specific rule for each function of our contract let's say you you decide that you don't want to check your functions because they don't change anything there are still many electrons to transfer from increased decrease allowance might be tedious and we have a better way a simpler way to do it uh we in we introduce a notion of parametric rule they don't ask if the owner called a specific function uh instead we ask if any function was called and what the outcome of that call this is the rule we have is like very specific we want more generalized and the question how we can do it instead the proof we want to call any possible function of a construct in for this we for this we use method F method is a keyword it means that instead of f the tool will try to use any public or external functions of the contract I want to state that only public and external so if you have something private or internal you need to change the visibility or make another function which calls it like you you create a public function which calls your internal function uh then we need to define the arguments of the function and they can be different here you don't need to specify it because we have another keyword called Data Arc it means that the tool automatically will assume necessary Arguments for each function like if it's like only one address as an argument or it's like you ain't an address we don't care right now the rest we simply copy from the previous version of the rule where we did it only for approval only and now let's try to run and see the magic happens this on the left side you can see all the function that the ours will try to call and we the only one but there is on one red dot that we don't really like because it's a violation I mean if it's a bug it's good because we prevented it but it also might be in feasible state here we see that it's like we transfer from and it's legitimate legitimate way to change the allowance as we know it but let's try to understand what's the real reason of it and in our verification report we can get a call Trace the cold Trace we get only for violations to see the scenario we to understand in in what way we could to relate the property and to understand if it's debug in this in the spec that we wrote or it's in a bug in the code here we see the arguments that we used for transfer from the sender is 401 the same as owner recipient IS F and also we want to check the emessage sender because this is what we use in our assertion and as we can see here is another address it's four to six that's why we've got a violation because the sender is stated in the transfer from the same as owner but the message sender is not a donor right now and what we can do about it because we have a violation but no it's not a problem code we can change our like property a bit and the way to do it that instead of saying that allowance is changing we want to ensure that if allowance was increased then the the message sender should be the owner any questions at this point okay now if we run it we see that it's passing um well that's good we checked something but and we have increased allowance within a allowance but there are still some unverified parts about other functions for example how we can change allowance one proposal that we have is to check if allowance was changed by specific functions and for this thing we use another feature of CVL it is called method selector the most of the rule we take from the previous version but we change the searching a lot here we see if allowance before and after different then we check using the selector F selector equal then the function signature.selector and we know like for example we just we we could write the code and see what changes it briefly like approved transfer form increase decrease allowance we check it here we use we can use them in one block with or we cannot use end because like in any specific Run f can be only one method so that's why we use the or and if we run it it will be verified so we also we again increase the coverage now we're more sure that there is no other way to to change the law to change allowance we are more confident here and uh it's like we we recovered like almost like the main the main things about the rules how we get like but the rule is only one thing which we use uh to explain our properties there is another thing in we call it invariant it's a property of the contract state that is expected to be true whenever a contract method is not currently executing it's as I said it's like another way to write the properties uh like but it's only applicable for several types of them the types of the properties is not a part of this talk about in general uh we can talk about we can reason about various states of a construct and high level Properties by high level properties we usually mean if we reason about external dependencies or not dependent on the implementation on implementation some properties they're not dependent like in ERC the total Supply should be greater or equal at the balance of one user just like the simple example uh like some benefits of an invariant usually it's smaller in the size because it's only the size it's one of the reasons the lights because it's really why it's really comfortable it also covers a bit more than a rule because the rule doesn't cover the state after the Constructor invariant can do it invariant we also can rewrite as a rule every invariant but not every rule can be written as an invariant and one of the main disadvantages if you want to check any specific scenario for example in a parametric rule I showed you that we can call only method F but you can Define method F and Method D and to see some other interesting outcomes of it and this is an example of the properties that I already defined that the total Supply is greater or equal of balance of a user and on the top you see the invariant itself pretty simple like only two lines of code and this is how it looks in a rule and also it can help you to understand what is an invariant invariant it's simply the requirement that we defined then any function call parametric call and then the same assertion uh this is like how it looks like but there are several violations we won't stop a lot about how to fix it because invariant is more like additional topic for this Workshop but I want also to show you the benefits of invariant in terms of the size and uh comfortability to use it because for example we want the first thing that we um we will see in that violation that like in our researching right now we assume only balance of one user and the contract example will be like the total Supply equal to balance of a user but what about all other users they also can transfer do something and this is what happened in the country example for that rules we add we change a little bit our our environment now we assume two invariants but there still will be the violation and transfer because it's a parametric call and two and e-message Center in transfer they can be different from the addresses that we check and this is what will this will be the violation in this case we need the preserved block it's just a set of requirements that will be applied only for transfer this is how it looks in in an invariant we need to make sure that the 2 equal to account from our one parent and the message center equal to our Center that the balance of we check but if we try to write the same in a rule it takes much more space much more lines of code not really comfortable of course you can put this if block inside the rule but then the readability will be awful it's better to make a as a separate function but here we need to use again selector Define variables write write some constraints and then we need to to call the transfer so like you you write the transfer two times instead of one time here for example the but it's it doesn't mean that if you define this function it's always the bad thing for for example with good in your usability if you need to use this function in several rules like welcome to do it it's a really good thing because you optimize the size of your code and as I said not all not everything we can explain Express as an invariant so and this was an example uh just only for transfer for all other functions which had violations that kind of the same the main point is just to show you another feature of civil how to just how to explain the properties and why it might be good to use it for now that's it we covered many things there are still more things to do but they're more advanced and it's Advanced topic not of this Workshop because we're all the simple rules we saw how it can be written we talked about environment variables methods block and what doesn't mean an environment and then free we considered reverting paths parametric rules how we can select methods in parametric rules we talked a bit about the coverage which is kind of the subjective thing and the last feature was the invariance now I think the Euro will take over to take about talk about the workshop the Practical part of it thank you so we wanted to do a lot of civil features a lot of theoretical stuff and now let's try to do some Hands-On work yeah so we're going to work on open Zeppelins there C20 token contract in which we inserted some bugs a really simple box so if you look at the solidity code you will see the bugs immediately they're not super interesting the interesting part is to try to find the bugs using formal verification so the task will be to write a unit test rule which verifies transfer in the parametric rule and then there is a bonus task which is a bit more complicated parametric rule and yeah so what we're gonna do so first of all uh you should have the docker desktop on your laptop and you should clone this uh our tutorials Repository so can the people people who participate in this exercise raised hands um okay so the people who will participate in the exercise so follow this step so start the docker desktop then clone the the repo and wherever you run into some issues so we have Sasha Armand here Emily will help you with with anything so clone the repo and just follow the steps in this on the slide so again people who followed the exercise please raise your handling if you run it to some any issue we will we will help you yeah so yeah this is the steps you you clone the repo and in the repo there is like a files which is describes what what tasks to do no no no no no no no no it's the on the next I'm sorry there is also the next line that explains that um you have to go to the CVL Workshop folder and um and see the spec okay so this is this is the actual exercise so if you start with the people who follow start with the docker clone the Ripple open the the correct branch of the repo switch check out the correct branch and then you have to open this open the docker open use the reopening container command in Visual Studio code with the remote container's extension this command will ask you to download our Docker image and then from this Docker image you do the exercise foreign so we're going to do a small change of plans because the internet here is a bit slow to download the docker file we're gonna do some live coding demonstrations how we actually solve the exercise so it's going to be more clear for you guys so our task is [Music] um yeah our first task is first exercise is to write a unit test rule that tests the transfer function and we basically need this we need this assert to we basically need to write the rules at the at the end at the end of it this assert will will be checked right so how are we going to do that so first of all like you remember we need to declare the environment and since we do since we test the transfer function so we're just going to we're just going to call it this is some random recipients and amount now we also need to declare this recipient and amount and we need to declare these variables balance center after and balance sender before it's a balance center before will be will be the balance of the message sender so all these functions like balance off and transfer and others already declared in the methods block there is no need to declare them again and the button sender after will be clearly the balance after the operation and now the rule looks ready so according to the instructions we can execute it and it says that we have some mistake here because we didn't declare the type of the variable usually the same way the same time foreign so now we now after the rule compiles after a few iterations now we execute it and what does it mean to execute it we have a we have already script and the script just runs the sertora Run command command command CLI tool and we tell the sector around to verify the erc20 contract with the setup.spec so like we mentioned in the beginning of the talk to the search or approver we have to give the smart contract code and the rules so here this is the Smart contract code and these are the rules so what hap what what happens here is that there is some kind of static analysis happening locally and then and then the tool sends everything to the cloud so the the main chunk of the tool runs in the cloud just some small local static analysis runs on the computer and most of it runs on AWS and here we get some command line outputs at eventually it will give us the link to the web page where we'll see the execution results so now here we have a link to the status page and verification report which is the interesting part so we're going to click on that and see that the transfer correctness function which we written which we've been writing right now has failed so it's interesting to find out why it failed and we open the call Trace okay so in the beginning the balance was two and then we try to transfer 15 tokens right which is not supposed to work because this balance of tool you should not be able to transfer 15. but it still it still did not revert yeah so there's some problem there because uh like we mentioned the territory will only look at um non-reverting paths and normally if the code is good and you try to transfer 15 tokens from from balance of to it the code would revert but here did not revert and now we look at button sender after and it's become huge so it's obviously an underflow here yeah and it's obviously an underflow so this assertion is doesn't hold yeah because now balance center after is huge it's almost Max event and balance center before was very small Zoom so you see the the problem possible problem is with the underflow so now we can go look at the code why what is this bug that you found and it's a very it's a very silly bug so basically what we did is what we did is um we just say unchecked we do this transfer and check we don't we don't check that the sender has enough has enough balance to send the tokens and we do unchecked subtraction so that's why we have this underflow underflow problem and the point is that you found this bug not by not by looking at the code we found this bug by writing this very simple rule it's we call it the unit test rule because it just checks one one function one one particular scenario and we already found the approver found found this uh problematic case for us you just try to send to to too many too many tokens and the code doesn't check that the balance is sufficient so that's why we have this problem so this is this this is the exercise one make sense I think usually the code should should check see if the balance is sufficient for the transfer and I just I think I just removed this check the like we require that the the balance is great or equal to the amount but when there is no check it just it says okay we have enough tokens so let's go now for exercise two we want to write a parametric rule that verifies uh fixed total Supply so like we assume that you work with the token that has fixed total Supply and we want to write a rule that says no function call ever can change total Supply this is a bit more interesting rule so how are you gonna do that so this is the this is this is our final assert yeah so again we do environment and Method method method as we already have let's do call data arcs for the F invocation let's get the total Supply before total before this total Supply function is already defined declared here in the methods block it's just access to the public variable and now the magic part is calling the calling any function with any arguments and again it will take the total total total Supply after the operation and this is a rule oh that's a very good that's very good question but this would require much more much more rule writing than you can do now basically for this we would need to track locally how the if the total Supply variable is updated correctly for this we would use a local state in civil which we call ghosts ghost variable basically like we would have a civil variable which drags the solidity variable it requires a bit of yeah you're right if you want to really work verify everything we need to prove that the total Supply variable is updated correctly after we prove that we can already use this proof and use the total Supply variable and assume that it's it's all it's true it's good foreign and now when it finished checking the this is the total supplies fixed rule also failed and it failed on a few different functions and approve and transfer from an increase allowance decrease allowance so let's let's see the first one white fell didn't approved so when we ran a proof the total Supply was 15 then we executed this generic function f which in this particular case was approved and then we see that the total Supply changed it became 17 so something happened in the in inside the proof function and if we drill down the call Trace into the deep inside the proof we see that for some reason something changed in total Supply so this cultures gives us a place to look in the code it tells us to look at a function underscore proof maybe something growing is going on there so let's check this function in in the solidity code so it it we can see immediately that the total supply has just increased the proof just increase the total Supply by the amount ask asked to approve yeah so it's a very silly silly code again the idea is to show how the how the how we can find the bug not by looking at the code but by writing a very generic rule that the total Supply should not should not change and immediately we see that the proof function does something suspicious it changes the total supply for some reason and obviously the increased allowance decrease allowance and transfer from they also call this underscore proof so it's all the same the same bug and they found that and they found the problem in the code just by writing a very short very concise parametric rule that says Check Total Supply call call do any operation Check Total Supply again and make sure they're equal so this was the second task um questions and now let's do the third third exercise which is the can transfer balance basically it's a rule that says that any user can transfer their entire balance out foreign required that but you can do your way as well foreign we did this transfer with reward which we discussed in the presentation it requires a lot of preconditions to make sure that we don't get reverts on things that don't interest don't interest us all this stuff we don't care that the If the message center is zero the recipient is zero stuff like that so now it's now the execution the verification completed and we can go to the report and look at this can transfer balance rule foreign about the question uh at least from Islam IC characters myself can transform balance is the web page we lose weight in the episode foreign something confused High School sometimes I'm pretty used to look with her these are personalities I mean this isn't resolved a new at least at least in the wood s and transformation related for how can transfer balance valuation oh this is the keys yeah that's correct transfer culture is from freeing a transfer for the creative work case or at least beautiful so our final task was our final exercise was to write the rules that verifies how user can transfer the entire balance out and what we did we added all this requires for all these preconditions that for cases that don't interest us so we don't fail on message gender zero recipient 0 or message value greater than zero so you filter all these things that are are not important and then we just call transfer with revert and assert that there was no reward because all the conditions are correct for a transfer but this we still see that the function failed the function reverted and then it drilled down the call Trace we see that there is a line something about white list in in the smart contract code line 279 so we will go to the smart contract to the line to seven nine and we see that the transfer function in this token it requires the sender to be whitelisted so only white listed addresses can transfer that's why we got a reward because actually this is like an example for a malicious token that doesn't let doesn't let the that doesn't let addresses transfer tokens out unless they are whitelisted so there used to be like rockpool tokens like this maybe a couple of years ago you can buy this token but you can never transfer it out you can never sell it so this is another example that there's like a this is not even a bug that's kind of an example for a malicious code and you can easily detect it with a simple rule that tests that users just can transfer their balance out right and the prover immediately finds a counter example any address like here 401 it's not white listed so it cannot transfer the tokens out this concludes this concludes this concludes the and the Hands-On exercise which unfortunately difficult to do without a with slow Wi-Fi and without installing all this uh Docker or Docker image but you you can see how how it's possible to write this how to possible how it's possible to write the rules on the faulty erc20 token and detect all the three bugs which were inserted into it by the rules which are quite quite simple [Music] um this is it