Where to Introduce Formal Verification on a DeFi Protocol like Aave - Part II

Transcript

first of all thank you Ernesto um I'm Thomas and I'm a tech leader sartora and I'm going to show you how to use a CVL to improve Security in the oven when protocols like oven um okay let's start so what is even CVL so CVL is a language that is a syntax that is a solidity like solidity it's really like to help developers write properties and for their code that should be more intuitive for developers because it's similar to solidity and why do we use CVL we use CVL to find to write tests that find all of the

states all of the possible edge cases and that might happen as an instructor said and we don't let us to avoid some state that we think about and then we know that we are covered and how do you do it we formalize the property in CVL we write it in Civil Wars we will see right now and we run with the code the the developer the the question of the code we run it through our approver and then and we get a result from the approver um the results might be one of one of the results either we get a verified which is a green check mark which is

pretty fun to get and which means that everything is correct and everything is fine and there is no there is no initial State there is nothing that the malicious actor can do to break your code to break your assertion that you wrote in the in in the in the civil or you might get a violation and when you get a violation it's a red X it's pretty annoying and what it means is there is some states with some inputs that breaks the property and the the proverb shows us exactly what is that site and show us step by step what happens and to to help us to find the exact bug that breaks the property so

um in the stock talk will review some properties that we want the protocol they have a token to have and see how to write them in CVL and what the results that we get when we run them on the other token code and later of course also the governance okay yeah so first before you start writing properties and we need to think what even do we want the code to to have what properties do we need and and as Ernesto said it's an erc20 and so first we need some simple erc20 properties and for example um the transfer function is in any erc20

would expect them we would expect it to preserve the sum of the sender and the receiver the sum of the balances if I I have some X tokens X other tokens and and ernestos Y and other tokens I transfer him my entire amount the sum before we before the transaction is X Plus Y and after it it should always be X Plus y it can be greater than it can be less because if I transfer him tokens then tokens wouldn't disappear and shouldn't create out of thin air also would expect for example that the sum of all balancers of all the users should be less or equal to the total supply of tokens in the system and which I think it's pretty good property and also a user can transfer more funds than

they have and then the imbalance which also it's a pretty simple erc20 property and to be more specific about the other token there are there are more properties that we have such as the delegate function that we want that that it will delegate the power correctly between users if if someone delegate their part of someone else it should increa decrease the first user increase the the receipt the delicate T and truly influence any other user so there is no this hidden address that might still of uh part of your evolving power or someone that you steal from some specific address and because you we run on all possible States and all possible

inputs we know that there is no Edge case specific address that might do any of those things so this is a civil rule which describes the first property the the sum should be preserved when we transfer tokens the sum of the both of the users balances the sender and the recipient and so let's go over it and see and see what what's what's here so first we have on the first line we have the name of the rule and we have two parameters the address two and the un256 amount the address might be any any possible address in in evm any value it's not not

limited to anything and also the amount the amount is any any possible amount so that means that if there is this specific amount of specific addresses to break something we go over all of them so it can't avoid us then we have the N variable which means that we start here from any possible State and any possible initial State and and the transaction that we will run in a few lines in the transfer can have any message sender it can have any message value any block timestamp any block number anything so if there is some specific input that might break or might and we might miss here we run on all of them so we can't miss it

then we save on the side the sum of the balances of the sender and the recipient the message sender and the recipient the two and we call the transfer function um and then we just assert then the sum of the balance or some balances after and the sum of answers before stays exactly the same so this is a pretty simple rules in simple property that would expect of any lc20 to have this property so um of course we run this rule when a development and everything was evalued wait I just and and this is what you get when you write a good property you see the green check mark everything is

correct everything is valid and it's it's pretty you can be happy that you've proven it after we do that we integrate the spec with the CI and whenever there is a PR and for the from the development team they just automatically run the rules on the new version of the code and then we just verify again that it will still hold in some cases it might not happen and then we found either and we have an issue either with the code and with a new code and then it means that

something is broken there so that exact rule it was integrated in in bgd lab in CI and among other roles of course but that specific one just broke recently on one of their PRS and what happened there is that we noticed that there are red X which is of course dead and red is for bad and we can see this violation let's just click on it I think red and and we can see here that this assertion broke and the sound this assertion book is false right so here we we have this assertion the sum of balances before the

transfer was 40 42 and after it was 44 which means that the sum of balances increased and when it happened let's take a look on the side on the variables and we can see that the two address here and the message center here are the same right the same what it mean in in the code there was a bug that if someone send money to themselves transformed to themselves they just get an extra money for free so if this in this case the the message senders transfer themselves one amount one and they just got an extra one a token so it means that if if this code was deployed it wasn't but if it was deployed then anyone can just gain

infinite amount of other token they have to have at least one but then they can have as much as they want you can just double themselves for forever and which is a bad bad thing to might happen especially in a governance token um and of course after the fix we can just rerun the rules and then get the green check mark check mark again and then we know that it doesn't happen anymore okay um some other property that we have the more specific to the other token to the governance part is the Integrity of delegate the delegate function what should happen there is that we have a a delegates to B we expect that A's

voting power will decrease B's voting power will increase and all other users shouldn't be inference by this delegation because if a and b haven't been delegating to anyone previously then the fact that I am delegating to someone else that I haven't been good against to anyone in some in the fact that I haven't been dedicated to anyone and then I started elegant to him no no one else would receive or lose um a voting power because of that operation so let's see how to write a rule for that and we will go over it it's a bit long but the government part by part and see exactly how simple is it it is okay so the start is in the start we

have Alice Bob and Charlie um a b and c so Alice Bob and Charlie can be any address um as I said before any possible address can be there so we can't miss any Edge case if there is a specific you know it's a specific address that might break something a malicious actor or something it it also go over the all of them so especially that also and so that's unconstrained and then we start from any possible State we require we want that Alice will be the message center of the transaction because later here we see that we call the delegate function we want Alice to initiate that

transaction and also the ones that Alice Bob and Charlie will be different than one another because Charlie is the one that represents the third party user who doesn't know the wizard doesn't know anything and just doesn't shouldn't lose or gain anything from this delegation analysis the book can be the same the same person because if someone delegates to themself it doesn't have a meaning and for our rule currently and then we expect that Alice and Bob don't delegate to anyone this is this part the bottom require that there is a Alice delegating to someone or is someone we require that they don't delegate to anyone and then we just save some data on the site so we

can compare it later we save the Alice's balance Bob's balance and then we save the Alice voting power Bob's voting power and Charlie's voting power and later we will have the assertion on it so so we need currently to save the the the the the data before so we can compare it later then we call delegate with a with one specific requirement that Alex is the message sender Alice is the one that's initiating this transaction but the message value specifically here because it's an unpayable function the message value has to be zero but the message value the block block number the block time step can be anything so if there is a specific maybe there will be a specific time in which something will

break even all of those guys that we cover because it's unconstrained it can be anything and then after we call the delegate function the solution delegate function then we again save in the Alice Bobs and Charlie voting powers and we check four assertions that if one of them break we have a counter example we have something that's broke what we expect is that Alice voting power will decrease both zodiq file will increase and we expect also that Bob will be the delegated of Alice and that is another function that we have in would you give your voting power to so Bob should be the one and Charlie didn't

close the internet again anything so Charlie's voting power stage is exactly the same so um when we run this this role let's see what happens right should pass but it fails what failed here let's check which assertion failed the third the search and failed here you see there is false here the one that checks that Bob is the legacy of Alice white failed so we can check here the rule parameters you can check here on the side that Bob in this example is zero why is this important because in the other token whenever you delegate to zero it's a special address whenever you

delegate to zero then it means as if you delegate to yourself so although you're not delegating to yourself from the system perspective you are the login to yourself so Alice Ali says um herself so then Bob is not her delegated so that breaks and which is not not good it means that we missed this Edge case when we wrote the the rule we should have prevented the system from even thinking prevent from this proven to even think about this this option so what is missing here so what do we miss in the beginning what should have required we should have required that Alice Bob and Charlie are

not zero because if there was a zero address we know that zero others can initiate transaction and they can't vote they can't do anything so it doesn't even make sense that Alice Baba Charlie will be zero address so when we require it as following then the rule verifies and everything works and we got the green check mark yeah where where because if Alice was the zero address then technically it doesn't break this this example can't happen because we

know that Alice Bob and Charlie are not the same so if Bob's needs to be zero to break the to break the code then then we already required if Bob is your analysis for show not zero and also Charlie and okay so to prevent these counter example specifically this a case that we know this isn't correct we don't need to record no need to record it Ali specifically is not zero but because we know that this case is not interesting for us and we just we we we can see that oh so when it's zero something breaks and we we know already it's not interesting case so we prevent those cases for even turn up because we know it around feasible cases so we just prevent them let's say in advance because we know it's a safe assumption um okay so those are the two examples on

the other token and now let's go to the governance V3 and let's see how we can use CVL to improve the security in governance history and so let's review some of the properties that we want the governance specifically to have and see how to translate them to CVL and run them and see the results okay so [Music] um okay so which properties would we expect the system to have the governance with three to have and we have an invariant and then invert of the system that if a payload doesn't

exist so it's greater than the payload counter as I said before the there are payloads and they live in in some other chain and we we have the payload candle that states how many proposals were created up until now so any payload ID which is further than the counter so it doesn't exist yet should have a null state or a struct of the state of the of them of the proposal and the state should be null because it doesn't exist yet so it doesn't make sense it won't want to be zero what will be now um so let's see how how do we do it well first we need to to understand what our invariants how do we prove them

so modern invariance invert is a property that should always hold um in some tokens it might be that let's say the balance of zero is always zero because they prevent transferring and minting to zero and in this case I want the the environment that some for any proposal ID that doesn't exist yet and we want the state their state to be now to be zero um and how do we do it how do we improve invariant so what we do is we do an induction so we have the the base of the induction that we call the Constructor and then we check whether the invariant holds or not so if the invent whole after the Constructor

then we have the first step and because we have the base of the induction then what we do is we start from any arbitrary state but we require that the invariant the condition was already true and then we call any function with any inputs any possible function any any possible function that the contract has and we give it all possible inputs that might happen ever in any any message sender any block timestamp any let's say they have four parameters two addresses one unit and one pool we we give it all of the input all of the possible inputs and then we check that the we assert that the condition is true again so after the function that is true again

and if it's true again then we know that whenever we start with the invariant being correct we will end up at the end at the environment being correct again so because we know that the base of the induction we know that it was correct after the Constructor and then we do we have proven that whenever it was correct it will remain correct after any function with any inputs that means that it's correct forever because we start from from it being correct after the Constructor and then no matter what we do it's keep keep being correct always so now we can we can assume that it's correct because we're improve proven that is correct always so no matter what we can assume it so what I'm explaining this to you because now we can

understand what is the meaning of this statement so um this is an invariant that represents exactly this property that non-existing payloads have in another state the non-existing part is here because the uh let's start at the invariant keyword and this is the the type of thing first there was a rule now it's an invariant and then this is the name and then you have the un40 the ID the payload ID so if the payload ID is greater than the payload count here the left-hand side of the statement and that implies that the payload the payload state will be none which is pretty simple a way to show to prove that

no matter what there couldn't be let's say any payload that's in the future that will be allocated next or sometimes in the future it can't be already initialized with something it should always start with none which makes sense because none is the enum of zero so in evm usually it will start a zero from the beginning but here we can prove that there is no way to backtrack or something and so this is this invariant is we proved it and now we can use it when I say use it what do I mean I mean that for the next rule we will use the invent will require the invariant and see that it helps us to prove um the the rule so

another property that we want to have in the governance V3 and is that whenever a proposal as Ernesto said there are a pretty complex State machine for the proposals they are the the non-state that we showed before we have the Creator we have the active we have the queued executed and we have also a um canceled and we have expired a lot of states and the state machine is pretty complex but we want to to describe a simple property that it covers many many cases and not just um have a lot of tested checks when I start in this case and then I call some

functions some specific function with some specific input it doesn't break yeah but I want to prove that no matter what if I get to the cancer then expired or executed Estates and I can't go out from that state it's a terminal state so we never go in we cannot go out ever not even to one from the other we can't if I get canceled we can go even to expired or execute it we just stuck there forever same as the for the expired of the executed which makes sense let's say that we have some proposal that says let's let's pay from someone that's the Dow decide to pay for someone and then that proposal is executed we don't want it there to be exist any function with any input that somehow kind of make this

that proposal to be not executed yet which is called queued and then you can just pay them again it's not a good a good thing that happened in the also if you have some proposal that's expired we don't and we know oh that is expired we don't know we know that it won't happen in the future ever because it's expensive let's let's say maybe maybe there is a proposal that is that says let's pay for someone and it's expired so we will just create another proposal that we will actually pay them and then and then we'll pay we execute it so we paid them but then let's say that there is some way to make it unexpired the first one so then we can make it

unexpired then then pay them again so this also doesn't make sense so we want those states to be terminal if something happened we want to be sure that we can't leave those things this is why this this environment is so important and and it came up while discussing with vgd about what they expect the court to hold and and this is one of their values we came up together one of the properties we came up together and let's see how do we write it in CVL so um this is a parametric rule which is a before we saw a specific wall with the delegate and specifically with the transfer and we had one function one specific function that had any inputs we started any possible State we call it

specific function in the with any input and then we saw that the assertion pass then we had an invariant that starts in any possible State and then it's called any function with any input and then check that that specific condition holds still now we have a parametric wall which we start in some state in in any state that that the requires are correct about it then we call any function with any input so again any external function of public function and that the contract had we can call it and then and then we can run a certain and be sure that the assert always holds so here we start with a method there this

this part is the parametric function here okay so the method f is n can be any function the args as they are represent the any parameters and we have the uint40 which is the payload ID and we require and then we require invariant which means that we tell to the to the prover we say okay so we already proven this property we know that if the ID is greater than the count then then it means that the state should be none which help us to prove it because without this invariant this property can be proven because for a specific example that let's say that the next proposal ID the next the next one the one that we

will Define right now and will start somehow without this invariant as expired or as canceled and then we propose a new proposal which go over this proposal so then its state will become created which is not which was canceled before and then it become created so we CA we we we left the canceled State and we entered the created state which doesn't make sense because it shouldn't happen so the way we prevent those cases is by proving that it can't happen and then requiring it so now we know that it doesn't happen next we have the required this requires is exactly as I said before we need to

start in in a state in which the the state is either executed canceled or expired and if we started in that state it's one of them then um we call the assign any function with any parameters any message any image message value any any block timestamp block number message sender anything so there isn't a it's a hidden embed actor a hidden address that has the authority to do whatever he wants or to to somehow roll back transactional proposals it's it checks everything so any message under anything and then we just uh sample the after State and reassert

as I said before equal to the state after this is a pretty a pretty simple rule after we go over any each part of it and see that that they are pretty simple here we just Define the state here we require the invariant that if it's the idea is too greater than the count it's uh it should be none and then that we start in in a state in which it's executed canceled or expired and run the function and I said the assert that it's the same so after we do it we get a violation so and this is a revelation let's go over first the green Parts with the good parts so for all of the functions as you

see here that there's a green check mark it means that we were able to prove it so no many no no matter what initial State we had and what parameters they put in to any of those functions they cancel payload they get payment a capable of State any of those function functions no matter the input the the condition the the cell doesn't break but for the function object executors the the search the assertion broke it went from expired to queued which means that there might be a case in which we have an expired um we have a proposal which is expired then we call this function there are

some inputs to this function that that will change the state from expired to Q which means that um as we would assume at least I think it's reasonable to assume that if a proposal is expired if it is expired it means that we can't run it in the future right that is the meaning of expired let's say you have a milk in the fridge and it's expired you assume that it can be unexpired and then you can drink it again because it's it's expired already um but now here we see that it might be unexpired and it makes it to be cute with Cube means that someone can run it and execute it and which is not not good for for the system

and and not good in general um okay so what we learned today um we learned that what CVL even is so it's a language for for developers that it's already like that we can um write rules in intuitive way and that is will help you secure your code is exhaustiveness and in finding bugs that we can check all of the states the exhaustiveness part and finding bugs we saw from the CI integration that will never whatever you do if you integrate it in your CI the rules run again on

your code on your new code and you just you can know for sure that no matter how small change how many small chances you've made even if you change one one function one line one one if statement something might break so then when after the rules run away over it you know that there are no initial State no inputs to any function that will break those properties and you know that is correct um this is why you should integrate civil into your CI and we also saw how solidity and how CVL and sorry our CVL rules and civil invariants look like and the reason I'm saying solidity so much because they look pretty much like solidity they are pretty similar

[Music] um thank you [Applause] any questions from someone yes does the prover support a reasoning about large multi-contract systems as a single state and okay so as long as the it's on one chain then we you can have a large state of multiple contracts yeah you can have it and the initial state will have any state of all of the contracts so any one

of them can have any state and then when you call functions between them then the contract will interact one another and influence their state of one another if the functions will do it of course and then yeah it works anyone else yeah thank you hi uh how you handle with timeouts and especially timeouts with for example division okay guys how you handle the timeouts when you run rules and got timeouts yes so also we can get timeouts of course

it's something that might happen so if we have a timeouts there are two options and either we try to um have more requires and more environment require more invariance so the state will be more simpler for for the approver so let's say that you want to prove something there are a lot of possible States but if we have many invariants that of course they are correct then it will Narrows out the possible State the realm of possible States but still only the valid States so that helps to narrow out some of the possible inputs and make the approver run faster and prevents times out timeouts and also if if let's say all hope is lost and you try to write all of the environments

that you can add and you can also summarize some functions which means that you can use I didn't touch that feature but you can also take a function and it's relative function and replace it with civil implementation or CVL a civil implementation of that function which will run faster in the proverb and then it will make the the times that time out from from the division or from something else to have less likelihood to happen any other questions okay thank you a lot [Applause]