CVL from ERC20 to Read Only Reentrancy

Transcript

try what okay okay hi everyone thank you for joining me today I'm Gila castellnuevo I'm a director of engineering at sertora and I'm going to show you today how you can use the sertoric words to protect your code and we are going to go over some examples from some basic property checking on erc20 protocols to detection of common vulnerabilities such as the read-only

re-entrancing see before I start I'm not sure if you are familiar with sir Torah sir Torah is a security company and we implemented the sir tour approver which is actually a tool which is based on a formal verification and the goal of the tool is to improve properties and detect bugs so before I even start I want to ask here who heard about formal verification before this talk okay cool that's cool and how many of you know what formal verification actually is Okay cool so for those who do not know a

formal verification actually is a technique to prove properties on code a property in the area of D5 can be for instance then for every transaction I want to make sure that no user is spending more money than his balance and the way that it that the way that it works with our prover is that you define the property in the specification language which is for the insertor approver the CVL which is a circular verification language and then you take your code written in the solidity and you then let the formula formula verification engine try to prove the property or find a violation the way

that it works behind the hood is that the specifications and the code are translated into a mathematical formula and then math and formal methods are used in order to prove the property or found a violation so now that I said that I have another question how many of you whoops sorry are actually using formal verification as a tool for security so nobody that's my point actually and I want to ask you why and maybe this is because you think that you need a PhD in order to use formal verification

or maybe because you think that for formal verification is nice but it can only prove trivial properties and another option is that maybe you think that formal education is good for like some a property check-in but you do not think that you can prove or find sophisticated vulnerabilities in your code so in my talk today I want to break this myth with the third tour approver I want to show you some examples of circular specifications and usage of the sertor approver and we will go from immediate properties on protocols to some detection of

vulnerabilities such as read-only re-entrancing so I will start with the first myth as I said before some people think that you need a PhD to use formal verification this is actually a joke but there is some some truth behind it because people think that since it's based on math and it's based on theorem checking so you actually need a special background which includes mathematics and logic and I want to show you how actually it looks in with the sertora prover and with our language so let me start with a simple example which is an implementation of the erc20

protocol and I Implement my own version of the transfer function and I want now to check some properties on it one property for instance can be the Integrity of the transfer I want to make sure that every time that I'm sending money between the center and the receiver the sum of the balances is not affected and this is actually something quite basic but I want to start with this with this property just to exemplify how it works so let me show you how I wrote my rule with the CVL language as I said as I told you before the CVL is the circular verification language and you just need

to write rules and then run the sertor approver to check the rules on your code so this is how my spec looks like okay this is my role this in the Integrity of transfer I have the uh I have some parameters in it and I have this sender the recipient and the amount and then what I do I just sample the balance before calling the function of okay so I said before we are sampling the balance of the sender and the receiver in the beginning of my role and afterwards I'm just calling the transfer from function asserting that the sum of the balances said before

say the same so as you see here this actually looks like unit testing it's very similar to the solidity code it's quite straightforward but this is not unit testing this is formal verification which means that I'm checking any options any arguments that can be sent to the transfer form function will be checked and also any amount will be checked this is because formal verification is exhaustive it takes into account all the possible valid inputs and just proves mathematically that the rule holds so once the rule is proven you can you can be certain that this

specific Rune will be true for all the specific the specific path and inputs that can be given to the transfer function so okay maybe this was not enough maybe now we are thinking okay so this was a trivial property or C20 and you are not convinced yet I want to tell you a story okay so a maker is one of our customers and one of the implementation of one of the things that maker did they implemented they make her die a stablecoin and one of the most important properties of the maker die a stablecon is the fundamental equation of dye this equation actually makes sure that the

the balance of the dye are always back by depth okay this equation actually says that the sum of the balances of the user is equal to the sum of the collateral plus some fixed amount which is in the responsibility of the token itself to to to cover it so the maker dice tablecon was actually um deployed in 2019 and what happened it then when maker started working with us they wanted to use the territor approver in order to check this environment with our language and what happened is that surprisingly they found out that this environment did not hold on their own

protocol which was actually deployed for three years okay so fortunately I want to say that this specific invariant and this specific bug was not exploitable so and no rates were at no funds were at risk and of course maker fix it pretty immediately but is it is actually exemplifies and emphasizes why formal verification is so important because sometimes even this 0.001 percent of inputs that you are not checking can hide behind them like a very important bag can can lead to a steal of million of dollars okay is so this is actually how the rule looks like in CVL this was actually implemented by maker themselves

there is a public repo that you can go and find it yourself the way that it works here where Implement their Implement an invariant which is actually a rule which is checked for all the status in the contract which means that we are like proving the invariant by induction every time that the function is called we will check that the variant still holds and you can see here that uh they just implement the same equation as a as they as they wrote before this is the fundamental equation of die there are some technical details here that you can find in our public repo but like very briefly we are you there they are using here what is called the ghost which is like a function which is not

implemented in the protocol itself but actually you can Implement yourself into your specifications and you just need to to write the code which updates the function to model the to model the behavior of the contract so this is what's actually a very important example but it's still about property of a specific protocol we did not get into like common vulnerability that you might might be interested in checking and for instance one vulnerability was what was very hair during the last year was there is the read-only re-entrancy one which was actually presented last year by the chain security and actually what happens when you have

a read-only re-entrancy there is a bug here in the presentation so what happens here is that a a bad intermediate state is exploited through an external call to another contract this actually happens when a when a contract is calling an external call while having a dirty State and a malicious attacker can actually use it to mislead another contract regarding the state of the vulnerable contract and this will happen using a view function so in this vulnerability actually put in Risk one more than 100 million dollars

so it's a very important vulnerabilities it was actually also reported it dragged several times but I wanted to to think together with you how you can actually in Define this this protection in in specifications what do do I want to want what should I want here I want to make sure that every time that I'm calling an external call my intermediate state is valid okay but what does valid mean because it can be it can also be to lead to to false positive because I can also update my internal state but it does not affect anyone okay so what I want to make sure that every time

then external function is called sorry there is okay every time an external function is called all the view functions are returning a valid State and one what I mean by valid I mean that this is equal to the beginning of the transaction or to the end of the transaction this is something how I Implement my properties in words but when I when it comes to CVL this is also quite simple okay this is my rule this is the read-only real no read only re-entrance Rule and what I do here I just sample all my view functions external view functions that I have in my contract afterwards I will call any

function external function that I have in the contract and in the end I will sample view the same view function again and what I want to make sure is that in the end the value of the intermediate state that might be returned by The View function is either equal to the beginning of the transaction or to the end of the transaction of course I'm omitting here some technical details but of course you can find it in our repo and the result explicit all the explanation regarding that we actually implemented it in the our own version of the curve protocol and of course this ruler found the vulnerability and the the most interesting thing that first of

all as you can see here we are testing all the external functions that we have in the contract and all the view functions but more than that in once we find a violation we can say exactly which view function is the problematic one and once we have it we can also explain to the user how to fix it because we know that gas is kind of expensive but you can put actually a re-entrancy guard all in the the in the vulnerable view functions and not in all the view functions that you have in your contract so and this is actually um the end for the read-only re-entrancy and this is actually a I'm getting to

the end of my talk but I wanted to give you some takeaways okay first of all I I hope that I kind of convinced you that writing CVI specification is not as difficult as you may think and secondly and I also we also saw here a real example one formal verification is applicable on complex protocols and lastly we saw here also an example on how formal verification can find sophisticated vulnerabilities such as the redolery entrancy one so you can find a bunch of more examples in our public was that we are updating all the time in these very days and you can also start using our tool there is a

barcode here which does not work and I'm not sure why because I see it here but actually we just really debate as you go option which is actually you can start using a trial version and just pay for the usage of the approver so this should make the proverb much more accessible to whoever wants to try it and I hope that you enjoyed I'm very sorry about the technical issues that we had here and if you have questions I'm not sure that we have time but uh [Applause] foreign

[Music] [Music] thank you