Formal Methods for the Working DeFi Dev by Rikard Hjort | Devcon Bogotá

foreign [Music] why am I doing this talk the candid motivation is I want you as developers to do more of the work that you assign to Auditors yourselves um we get a lot of questions you know someone signs up for an audit the audit is going to start in two months the code will be Frozen and then we are invariably get the question can we help you prepare for the audit somehow can we help you get like make sure that the audit runs smoothly um there's a few obvious ones let's see do you have a pointer I do uh these things I'm not going to talk about because I hope dearly that if you hire an auditing company you have good tests they run they pass you have integration tests you got documentation and you make sure that your devs are available for the couple of weeks that you're going to spend on an audit if in case a question comes up those are the basics but I know a lot of teams are really really highly skilled and they're very motivated and they want to do more if they can so uh well what can you do what's what's the secret sauce to getting a good audit actually what's the secret sauce of the Auditors Auditors like us different noted companies do different things but we have our own little method of working which I'm going to share with you um invariance we like something called invariance sometimes you call them Properties or property-based tests or whatever your favorite equations over State I usually just use the word invariance for everything they help you find more bugs right better docs trust your code more they help Auditors because you know as Auditors especially we we're going to be looking at invariants and trying to find more of our like invariants of our own basically so if you come with a little set of these that you've already gone over you've done some of our work for us and we can focus on like either deeper work or we can work more efficiently and get you done faster um so we want you to come up with invariants if you're on chain code they're also good fuss targets we're going to get to that uh they also one thing we found especially developers they can tell you exactly like oh you have to go to this function and this function you will see exactly uh where this variable get updated and everything and once you start talking about invariants and we say things like well just a sum of all balances always match the total balance and so on then we find that a lot of Auditors or sorry developers start looking at their code from a new angle because this is sort of a top-down angle it's almost like you're coming back to the design phase uh moving out of like the optimized imperative code and thinking in a more declarative fashion um don't have to read all this I just like to have a thing I know this is being recorded I I myself like to pause slightly talks and like read slides uh so I put more on here than uh I'm gonna read so don't read all of it I'm just going to say really quickly here's what we can structure this talk uh we're gonna go over like how to make invariants I call that state is just equations uh then how to prove invariance at least uh in a pen and paper fashion which is what we often do uh talk about how to approach things when you can't really get your proof to work and also how to use your invariance to do fuss testing and even monitoring if that's your that's something you want to do um and if you have code working right now if you have a laptop up like you can bring up your own code uh go over your own code link because I'll be explaining how to come up with invariance if something comes to mind and you want to write that down please do that I'll be working over an example from an audit we did a while ago so if you don't have any code you're working on right now or you just want to follow follow through now and then go out and start working on variants on your own after this session that's fine too uh I'll also it's a lot to cover an hour isn't really enough uh anyone here interested we can just just grab a table I'm happy to take anyone from this crowd anywhere and just keep going with the workshop if you want to keep working on invariants afterwards so just just grab me we'll find a table somewhere and as many of you who want to keep going we'll just keep going I like this a bit too much it feels almost pathological but I love when developers come up with invariants um so testing versus invariance testing is I guess I didn't see the the previous talk but I think he was talking about how to do better tests Tesla sort of like the camping knife it's like if you know what you're doing you can use it for almost everything and you'll get out of most things by just doing a bunch of testing it's our first and most robust line of defense um there's a myriad of resources to help you test better there are talks here probably how to test better um so again I assume you already know how to do tests I assume you do unit test that you do integration tests you try deploying on test Nets and so on um and my analogy for tests is sort of like an experiment right you're trying a single thing you're going to see what happens if I do exactly this call or I do this little sequence of calls um it's great and we often like especially test driven developers like to talk about testing as you know some sort of silver bullet or even if they say it's not then you can kind of feel like oh the test is testing is what you need and that's going to solve your problems um but I don't know any developer that actually trusts their code enough oh my test Suite passed uh bring on the billion dollars TDL like that that doesn't happen right you're like you sit down and you like really think through it and you talk to your colleagues like well are we sure like have we thought about everything um and it's sort of like that sort of like Theory um reasoning about code is like developing a theory it's like what if if the experiment is or if testing is just an experiment like in in the physics or like a science context they help you verify that your theory is correct and if you do enough experience you might be pretty convinced but you also probably want to make sure go over your theory and see if like are there any holes in it does my theory leads to inconsistencies even if you tried 200 prime numbers where maybe prime number 201 is going to be the one that breaks your little mathematical theorem so you need to be reasoning about uh what your theory is saying um the thing is there's very few resources about this I had one five minute talk by my professor when I started college saying like here's how I run over code in my head and I think that's that's the end of it and it feels like reasoning about code is something you learned from experience uh it's something we're always doing when we're debugging doing code review doing design discussions we're kind of like simulating things in our head um but there's not much resources about it no one's really teaching you how to do it it's just sort of like well you're a good developer with time you learn it so I want to change some of that by giving giving you some structure if you don't know where to start reasoning about your code to make it more secure here's going to be a few steps to get you going um this is meant to either intimidate you or titillate you depending on what your uh what kind of person you are um but we're doing something that's sort of analogous to math proofs so in math you were taught both like Computing answers like figuring something specific out but also how to do proofs how to make sure that the algorithm that I'm doing is always going to work again it's sort of like the analogy testing versus uh reasoning experiment versus Theory uh reasoning about code is analogous but proofs before anyone say Curry Howard like I'm not talking about something like that if you're a theoretical computer scientist I'm talking about something very straightforward that I think anyone who has taken a basic code boot camp should be able to do um and just like proving uh there's a method there's a bit of artistry it's not always straightforward I can't guarantee you that your proofs will work even if your theory is correct but there's a structure to it you don't have to just be flailing around trying to prove random stuff um and with that we get to the actual invariance what is an invariant what are we looking for and what are we trying to do um so this is very small um so one way to think of a good invariant it's something that it's obvious that the code is doing or should be doing um but like if it works correctly it should be doing this specific thing but it's sort of incidental from the code nowhere in the code is just like directly enforced it's just something that sort of should be obvious from your business logic um ideally it's really something really high level like aliveness uh like a liveness claim that you know this contract can never get stuck and so on but to be completely honest starting with really simple invariants will get you quite far most of the time and we'll do a very simple invariant here today uh and I can tell you from experience that even those really simple invariants that aren't like super high level claim that the entire protocol is perfectly secure they still help you find bugs in your code and we find bugs all the time using them um invariants defined as it's not varying its constant in mathematics is unaffected by a dissocinated operation uh and or an invariant quantity function configuration of a system it's something that's always true uh you can think of what's the code behind the code because the code is very exact it's imperative it tells the computer or like the evm exactly how to do every little step uh so it's not it's it's imperative not declarative is one way to say it and here's your chance to be declarative you say something like you know here's the equation that should always hold I think any ERC erc20 contract should have this property right you keep track of the total balance you're minting you're burning uh you're transferring and we just kind of assume or like we hope or we might be very very confident that the total balance is going to be the same as the balances in each individual account that has interacted with the mapping of balances so this is just a way to say take all the balances in the mapping and sum them up if someone knows way too much about the evm like I do then just think of us every every time you wrote directly into a mapping technically the mapping contains a bunch of other stuff but don't worry about that uh and again a gradient variant is something that's obvious from the intended business logic like this like of course you know the total balance should be just all the actual balances that are out there but it's not necessarily obvious from the code nowhere in the code is the stat there's no one summing over the balance anywhere in the code um here's a working example if you want to if you don't have any code of your own you want to pull up and follow along on your uh laptop you can go to uh GitHub alchemics Finance V2 Foundry repo it should be pinned at the top uh we're working at the contract Alchemist so we're going to be like Ctrl fing through a little bit of it if you want to follow along properly or you can just watch the slides uh really quickly this is sort of a slightly more involved version of the the sum of all balances total balance invariant they have something called shares that they're used to uh that they use to make sure that you get your you know your your yield in proportion to how much you have staked uh essentially and then for every specific yield token there exists a total shares valuable so slightly more involved than this the sum of all balance this is total total balance invariant here's how you frame it as the mathematical equation uh if you go into the uh mapping of all yield tokens where that contains the token address as a key and a set of params that's this you'll took in params if you go into param's total shares that should be equal to the sum over all the accounts uh this value of each account uh that's just one invariant we come up with we proved uh it turned out helpful I'm not sure if we actually find any found any bug on that one but you know we do find bugs on those kinds of things quite often um but the question is like so if you're sitting here with your own code for example or you're watching this later are you thinking about your own code how do you come up with good invariants uh how do you come up with like looking for something like this and there's a few tricks um first is to come up with many like try to think of anything you can say that's an invariant uh state that is invariant and then focus on the ones that seem to be important um second one is go over storage variables do you have uh do they have like obvious relationships this was a good example you have the balances you have the total balances of course that should just stick out as a sore thumb like that's these these two things should have a very tight relationship between them um ghost variables is a nice trick that's sort of just like introducing variables that don't exist directly in the code but that you can use when you're reasoning over pen and paper I'm going to give you an example de-optimizing is always fun like you're doing a lot of optimizations even if you're not doing even if you're not a big Optimizer you're not iterating over all the accounts of all your users for example that's the sort of optimizations as solidity developers we need to optimize but what if you just think I don't have to optimize at all you write the code as you would in a dumb Java program and then you just State the invariant say like well this this naive implementation and this optimize implementation are identical modulo gas usage um go to your design spec I hope you have one you all right design docs right read it over see if there's anything you're mentioning there that's obvious like that's something that there's a good chance something says something in the design dock like well these these two variables should have a relationship to each other that might not have been carried over to your code comments uh those things you should go to invariants and you can also work from unit tests like replace some unit test values and start thinking about what if we start fussing it what if we use symbolic values what properties would they have to satisfy and then just try to State them as you know equations or something similar it doesn't have to be a mathematical equation it can also just be a very exact description that's what happens if you open a math paper it's it's not all just a set of equations it's a formal formal line of reasoning written in English and that's fine too so ghost variables are just a way to introduce variables into your invariants or your system descriptions that don't exist on the chain or that you don't have on the chain um so impossible to compute functions we've seen already some some overall balances you could think of that as sort of a ghost variable you can't really do it on chain for several reasons uh but you're absolutely free to use it in your uh in your invariance and just make sure that you know whenever you're adding or subtracting from a balance somewhere in that mapping then you know that sum gets updated um another one is like well total deposited ever for example how much ether has this contract ever received maybe you're not actually tracking that you can't probably actually track that in your in your contract but if you're just reasoning about the um about your contract then you can say like well how much ether has ever been in this contract make that a variable and you studying your questions um and hopefully you may decide that some of these ghost variables actually deserve to become State variables it might make sense to actually keep track of these on chain the way we do with totals um even if it's just for monitoring even if it's just a little view function even if it costs a little bit of gas it's going to help you reason about your code monitor your code and like make sure you can run your tests on um on chain State forever here's an example of de-optimizing just to give you a quick look of what that can look like here's a really simple optimized you know normally optimized piece of code when you give rewards then you increment the total reward ever variable that should be a semicolon there uh and where did all semicolons go must have done a search replace oh well um because what happens when you keep copying over from different resources um and then when you withdraw rewards you just calculate you know whatever a user has a specific stake and you can say the last time they're reserved they received a reward you calculate how much reward they've earned since then then you update some variables and you send them some tokens the really dumb way to do this is when you say give rewards uh you just iterate over all the users and you give them a bit of reward and then when they withdraw you just set their rewards to zero and you send the tokens you can't do that right that's not really possible and if you do that I will slap your fingers but if you can definitely make a statement like hey these things will give the exact same uh results for a single user right if we call to give rewards with a certain number of amounts and then I call withdrawal rewards I should receive the same things from both of these implementations that's a nice little variant um oh no this this would be just like you know in an adult like we're going to get to like part of the reasoning yeah I want to also emphasize and I will emphasize a few times you need to show your work again like I feel like a math professor here but like show your work because there's a lot a lot of work involved in coming up with the invariants and improving them and if you do this to yourself and your notebook and then you throw your notebook away then you know well the next person is going to have to redo it or the auditor is going to have to redo it and that's can be expensive for you so make sure that you you know have it I don't know how you like to document things if you like to do it in your codes you have to be new code comments or if you want to have a Google doc somewhere whichever this but but this like you could have a few pages in a Google document that say like hey what if we implemented like this here's our actual implementation these should be equivalent here's you know uh pen and paper proof showing that it should be yeah so yeah this this doesn't work in in a real contract because sorry oh yeah yeah don't go deleting all your semicolons like all the experience examples here are illustrative it's not uh they're not this one isn't pulled from an actual deployed code uh it's just you know a quick example of what de-optimization looks like um or I could say oh it's it's pseudocode like because some of you might be riding Viper and this the process still works so um okay now we get to actually proving them so you come up with something that you say like well this should always hold over my contract forever uh proving I had a math teacher who said like well proving sounds scary like oh it's you you just need to convince someone how good does your proof need to be well you're gonna have to show it to someone if that's you if that's your friend if that's nature magazine then you know whoever you're talking to you need to convince them that yes I know like my argument is sound and it's complete and you know my my uh my theorem holds right uh the good thing about code is that it's usually boring and straightforward it's uh pretty mechanical um because hopefully the code is pretty straightforward and all you need to do is check a bunch of places which can be boring but uh straightforward usually so how do you prevent a variant well straightforward you uh figure out where are all the variables or ghost variables that are ever written to where are they modified if you find all the locations in the code you lists every function that modify any of these invariants you make a list it's a Google doc if it's you know if you have some cool emacs tool to do that go ahead just make sure you have a list of them um so this is like manual verification like of course there's still we work with tools we mechanize things we love building tools to do these things but it's actually really very useful especially for smaller contracts to just do it as pen and paper a lot of times so don't get intimidated when I say like just write it down like write it down into document and follow through it's it doesn't actually take that long most of the time um then you check what's called a base case you check that the invariant will hold from the start in the Constructor uh the initializer wherever just make sure that like your invariant isn't invalidated immediately as the contract is deployed uh that's usually the easy part and then the hardest part is the inductive case you find all the locations that you noted here and you go over all of them uh you can assume as you go into the the contract that that's the transaction start that the invariant holds and then you just look at all the locations that modify the variables you do some symbolic updates uh just say like I'll show you what that means in a second and then you check that your invariant still holds if you do all these and you find that the invariant holds from the beginning and it holds at the end of each function if it held in the beginning then you're done like the American holds forever and this contract um on the working example so if you pulled up the code then you can control F for our variables which are total shares and balances um if we look over the contract I usually use a silver Searcher and some other tools just look get an initial search for where are all the places where these variables can be modified there are more structured ways to do this but just use the fastest um make sure you look for assembly code because you know it can modify your storage variables um and make sure you find all the relevant locations uh I'll also look in the contracts you inherit from because you know modifications can happen there as well and use a dependency graph tool if you need to in this case we find uh these three functions modify our total shares and balances add yield token issue shares for amount and burn shares these two are internal this one's external uh I can just tell you the ad the first one add yield token uh it's fine it just sets the values to zero uh Constructor and initializer doesn't really touch any of this so everything's zero so we get initially zero equals zero because the total shares for every yield token starts at zero and all the balances start at zero so this is a sum of zeros and we get zero equals zero that's true so the invariant holds initially and then we go and find um the issue shares for amounts we find that in these two locations are variables to balances and total shares get modified um technically it also makes sense to reason about like is there could there be re-entrancing here actually in this case that wouldn't matter um are there many different paths through this function no it's a very straightforward function technically there's a path here but it doesn't matter for us because we always only um the only relevant changes are in this basic block there's failures but if this function fails then you know State doesn't get committed and still fine so we find that we add a number of shares to total shares read very carefully accounts recipient balances yield token shares yes heal token steel talking total shares yes yes okay we just add shares to both sides note that we don't really care how the shares were computed like we this might be an external call like anything can happen here it doesn't matter what we know is that if we come to this location of the code and we go through this line and this line our invariant will hold once we're out of it uh this one has left us an exercise to the reader it's slightly more not challenging it's just the exact same thing um but I mean like now we've proven this invariant and it may Sun sound slightly meaningless but it's sort of like that was one of those questions that come up as you're developing hey am I sure that well total shares and like the uh and the balances they should always match uh I should check that at some point uh maybe I haven't but like now you have checked it and you've wrote down your proof hopefully and now you know and you don't have to worry about it that's one good thing um you can convince everyone that the invariance holds uh the case may seem trivial but as things get hairier the bugs get scarier and this class of bugs are definitely out there people do forget to like do the second variable update I mean it wouldn't be crazy to find this code without uh the second line here it happens you know someone slips through a code review and then it happens and now you're in deep because this is actually used to calculate rewards and if this line was missing you'd be in deep trouble and your Auditors would find it and report it a critical order ability uh and again make sure you save yourself some somewhere useful somewhere you can find it somewhere you can show your colleagues so you don't have to redo your work um Chris is anyone did anyone pull up some of their own code and it's looking for invariants in that oh someone okay cool okay so I know that you're all hardcore super developers and your code is not always this straightforward um so what you do then uh failed proofs and I don't mean like if you find that the proof doesn't hold then you know you're very it's invalidated and you need to like make sure that you know figure out why why it doesn't work and fix that what I talk about here is fail proofs is when you actually fail to prove it you didn't really conclude that your invarian doesn't hold uh you're not sure it holds what can you do especially as code gets guitarrier uh well so these when that happens it's actually a good guide to refactoring and refining your code um so here's some basic tools that we can use and we usually recommend like if we can't prove if we can't prove an invariant and we really try to uh then we usually ask you like hey can you make this a bit more clear because we haven't been able to convince ourselves we haven't been able to convince you uh you should want to be convinced of this invariant and until that happens we should make sure that we can either help each other reason through the code or we can make the code more easy to reason about so if the function's logic is too complex if you really don't want to refactor one thing you can do is you can instead of giving a name to each function you give a name to each basic block as does everyone know what I mean when I said basic block okay going back um so a basic block of code is a code that will always be executed together so for example if you enter this if you enter this function um This Can't Fail there's no branching here this can't fail there's no well this can't fail actually so um but if we okay if we ignore reverting failures for this case which we can because you know reverts will just mean that nothing happened these three lines will always be executed together uh and so will this condition but this line may or may not be executed so you can think of this as a basic block and this is a basic block if you have a while loop then the body is a good example of a basic block if there's no more branching in it basically anything that's like you can treat a solid chunk of code that will always be executed together with each other if you had thrown this line into here or like another if case then it would not be in the same basic block and then it would be harder to reason that your invariant holds um so yeah I mean that's what a basic block is a single piece of code that would always be executed together um and if you have really complex logic and your functions are really big you might want us instead of giving labels to just a function so you give labels to each basic block and the reasoning works the same way if you can prove that after each basic block as you go into it and as you come out of it the invariant holds then you know your inductive proof is fine and your Marion holds um what we find sometimes is that you will only like the variables that need to be updated together are updated in slightly different places uh and then we get an argument like well you know but they will always because of like some sort of reasoning about the possible execution conditions they will still always be executed together well why don't just co-locate them put them right after one another to make it easy to reason about them if you have complex arithmetic expressions with rounding ignore that for now uh treat numbers as real numbers don't worry about rounding at all you can do rounding error analysis separately write your stuff as functions imagine it's all real numbers make sure you're invariant holds and then you do rounding error analysis we did a talk on that yesterday I'm sure you can find the link in the Devcon videos about how to do rounding error analysis to make sure you're contracts are safe if you have a bunch of different invariants a nice thing is to do what's called framing conditions you just write over each function which storage it modifies so you can look at a function and say like well this function modifies all these storage variables if it doesn't modify any one of the ones you care about then you're fine if it modifies one of the ones in your invariant but not one of the others then you know look out but it's just a good way to build up your code with comments that will make it easier to reason about in a structured way if you see doing this more and more um again did you check everything Imports inheritance both up and down uh inline assembly there's a bunch of places where you can have storage modifications that you weren't thinking about uh control effing does is not enough uh and if the code keeps changing if you're doing this as you're prototyping you're doing it wrong this is like once you've done a proof and you checked everything and your code changes you will need to recheck your proof so this is very much something you will do towards the end ideally when the code is frozen or almost Frozen um so again like if you're asking a an audit firm to audit your code you should ideally freeze it before and that will like whenever you freeze it you can start doing this or slightly before question for the live stream so pretty much when I have the client that really likes to change the assumptions of the whole projects basically then uh I should I guess I should write those invariants but recheck them every time the changes happens yes yeah and I mean that can be a statement of work hey we did all these things and then oh we just wanted to add a new functionality and like okay I'm going to recheck these things that's going to take me four days and like but you already checked I'm like well you changed the code it's like that's sort of the negotiation with um with the client and it also kind of emphasizes that you do need to freeze your code as much as possible like so again if you if you doc if you document your proofs really well and they don't refactor everything and change the entire design then change like looking over the proof should be pretty straightforward if you're used to it you can kind of work from the diff uh just oh they made this code diff and you can make sure that all these changes would still respect the invariant um just look at all those locations and make sure that the environment is still respected do you have the microphone thanks y'all yeah I just wanted to add that maybe the thing he's talking about with frame conditions helps with that because you write down you know what storage slots these functions modifying tell your client like hey you make the modification write down the updated storage slots and then that minimizes how many functions you have to recheck your invariant for because if they didn't change which storage slots it was asking you don't have to recheck it yeah I mean there's a feedback loop here as well right I mean if you if you write down your framing conditions put them in the function and then you can make sure that the client knows to respect them or like you know up again update their framing conditions and so one beautiful thing about this way of working that we found is a lot of our clients get trained to do this more and more themselves they start producing better code it's more readable it's uh it's not always less complex but like the important things are more co-located and so on so uh I would say if you personally if clients keep changing the code like make sure that they understand that there's a cost to that uh if they still want to do it of course they can do it um but also help them to train them to be better at when they do that they also make sure that the proofs that you produced or that they produce that they have are also kept up to date right um yeah I like that it's a co-location sort of like imagine like if you I don't know if anyone writes Java or C or JavaScript imagine if you use one of the basic data structures like hash tables or something and you manually had to manage the number of items you imagine how to manage all the internal variables this is sort of the kind of encapsulation uh I know people don't always love using libraries for different reasons uh you know gas optimizes and so on but try to make sure that you're uh your your code behaves more like it like you know the all the things that are relevant to this little data structure updated in the same place how do you recommend testing uh basic blocks if they're like within a function like unit testing them like for invariance if you wanted a certain variance for a baseball I mean it's just the same thing right like in like if you let's say that this was a really complex function and there's a bunch of code here and a bunch of code here uh with and there's a bunch of different paths through this function right I would name this basic block whatever basic block these contain I would name that something and then instead of checking every function instead of going over over every function and prove this I would just prove it over the basic block like here so I know I can assume aspie as we go into this look when we are here assume the invariant holds after the basic block which I know will be executed together I can show that it holds and then for every basic block you just go well in this basic block it's not modified so if hold four then it holds after this the basic blocks appear if it gets modified before if it's it doesn't get modified so it still holds right so it's sort of like you instead of showing that the invariance hold over each function you do it over the basic block and you give them a name or something and if for some reason this was down here one of the updates we're down here then that's a good reason to move it up so that they're in the same place because that will make you reason it's a lot harder to reason about it if they're in the different basic blocks so you have to think about everything that happens between there but if you co-locate them then it's a lot easier okay I do wanna you you need I mean technically you could say like you needed to hold from if it holds in the beginning of the transaction holds at the end of the transaction but I mean maybe the invite sorry maybe the environment uh breaks uh between two blocks but your environment holds for the whole function yeah how how do you recommend dealing with that it's just much Harrier proof to make like it's just like if you really need to do like consider if you really need to do that if you really need to do it that way then you do need to treat the entire thing as one block and reason about all the possible paths between uh I'm a little short on time uh if I want to get through this so we do have a minute 10 minutes of questions at the end right uh so if there's something that just one quick question if you if you have like a [Music] that you generate and you increase one by one um this ID will eventually overflow and you can you cannot prove that it will never overflow but it will require millions of transactions so in practice the you you should not you you can prove it but it will be never reachable uh so what is what is your view on this you state your assumptions you make the assumption that there will never be two to the power 256 uh transactions on the ethereum blockchain and you move on with your day that's it all right it's like the the counter in open sampling contracts can be unchecked on its increment because it will never update it will never overflow if you know what I'm talking about if you don't then doesn't matter um so I I just need to move on uh so if it's if you're having a lot of trouble look at the environment that's giving you trouble pick one function uh look at all the relevant variables and try to group them uh you may have to create a few different paths uh use helper functions like you know this one's really good the they had the burn shares and issue shares I think that might have been in our recommendations like well these things will have to be up there together let's make sure they're updated in a single place uh where all the relevant things to burning shares happen together right don't do it all in you know all over the code if you can avoid it um remember this is what you need to show the invariant holds at construction time and it's not initialization and if the invariant holds at the beginning of a basic block it holds at the end of the basic block through that for all the blocks then the variant holds anyone who's likes discrete math this is an induction proof um we're security Auditors we have slightly different priorities sometimes from developers so like we kind of security is the most important thing simplicity is the second most important thing it can depend but like the thing is Simplicity is so tied into security that we really care about Simplicity and we'd rather have you skip a neat bit of functionality if it just makes things too complex and then you know save that for version two or something or an extension and optimizations are the least important thing I know that doesn't resonate with everyone but uh if these things are so much more important to you than uh keeping things simple and having make it being easy to reason about security what you can do again it's just it's a lot of work but then again uh you should probably spend you know 10 times more time on securing your smart contract code than you spend on writing it uh so it might be worth it you can start with simple functions and prove that they're sort of like the de-optimization thing start for something simple prove that it's correct then start doing incremental optimizations and prove at every step that your proof still holds right and you end up with slightly more complex proof but you'll end up with a proof nonetheless saying that your invariant still holds over you're more optimized um optimize code um do you want to talk about invariances test targets uh we like to use Foundry uh you can take your invariance and just create a bunch of tests to just test those as properties like you uh you take the variant we had here and you just there you go uh and you run a test uh that just does a bunch of different operations and it interacts with your protocol in a bunch of different ways and at the end it checks your property that's pretty straightforward a really cool thing you can do uh if you could instrument your testing to just you know at the end of every test you're running check your invariant like make sure your advantages always holds everywhere uh it can be hairier there's things I'm going to show you one trick to do it it's not it's not the most elegant way but it's the most simplest that will get you going quickly um here's a dead simple idea if we take the contract we just had uh and we just wrap it so we take all the functions that affect user accounts so we make sure we keep track of all the users we have so we can do the sum overall to balance this thing uh and then we just whenever there's an interaction we make sure we add that user to the set then we do the regular uh update and then at the end of every function we check our invariance um and we do this for all the Contra or all the relevant functions in the contract and checking the invariance is just checking well you know so once we have this one's called A2 uh so checking A2 is just doing this thing we're summing over all the balances and then we make sure that matches the total shares so now you're checking your invariant at the like in each and every uh interaction you're doing with your contract uh again I mean I'm sure a bunch of You Are cool hackers and you could do this with uh if you get the name of The Foundry op code but you know if you can update the the evm code of the contract in place to do this in a cooler way and in a more robust way but this will get you going pretty quickly [Music] um so yeah basically your job is to update ghost variables the variables that you have in storage you can always check your ghost variables you need to keep track of with a wrapper uh this might also convince you that some of your ghost variables should be actual variables maybe it's maybe it makes sense to keep track of a set of all your users in your code I don't know um it's a trade-off you have to make and finally I just want to mention you can also use this for monitoring I think someone mentioned it um there's two approaches to monitoring um roughly one of them is just doing it on chain like make sure check your if you find some important variants that you can check on chain you can put them in requires in a search clause and then if something if for some reason at the end of a transaction they are violated you bail you stop the protocol um that's good because you can halt the contract before bad things happen you can't no one's going to be able to mess with your uh toll shares and like steal a bunch of yield that way uh it is pretty scary though because it can can cause liveness bugs you don't want your contract to end up in a state where it can never proceed and now all the funds are stuck uh so you know talk to your auditor it's like talking to your doctor like you know we're we're here have them on speed dial ask like I'm not sure about this but I have this little thing in my code and like they might say that's fine or they might say come right in drop everything you're doing and let's talk about this uh and you know obviously gas costs you have to put the gas cost on all the users or you can do off-shade monitoring a poor man's monitor uh we'll get to that but uh you can you know deploy it later even if you already have a protocol up and running you can still deploy um some off chain monitoring uh he can't call us live in his bugs obviously uh what do you do if you detect a failure maybe it's all regulates your variant got violated someone stole all your money um and it may not prevent tax that you know happen in a single block someone uses flashbots it violates some invariants and now you know the damage is already done before your Sentinels can come in and halt your protocol uh apartment's monitor is actually just using your Foundry fuzzing test and running them constantly against on-chain state and you know pinging a Dev if for some reason they get violated um after that well well first I should mention what can you do next well you can keep finding invariants uh you can add more uh document them share them with your Auditors share them with your uh with your users you probably have a bunch of white hat users hopefully that can if you make bold statements they will take that as a challenge to go out and try to find violations of them um and the good thing is you can kind of keep doing this long after deployment finding uh finding good invariance making that will improve your documentation uh and they will improve your monitoring so you know security doesn't end when you deploy uh another thing I want to mention is we like symbolic execution with like formal verification uh so we're working pretty hard on making sure that if you write your invariance in Foundry and you fuss over them you can try as many million inputs as you want we also have a tool that will let you uh run it symbolically so try it on all inputs uh there's a bunch of trade-offs you should do fussing first because it's fast uh you can write your test using solidity same thing because you know we used to found your chest anyway um you're limited to what you can express in solidity whereas with our KVM Foundry implementation you can kind of use all of matching logic and not all a matching line but a lot of matching logic uh it's a it's a nice logic uh fussing is extremely fast uh this symbolic execution is pretty slow it's getting faster my CTO is looking at me uh I might have called it as orange but it's turning more and more yellow um doesn't require any human intervention uh this often requires human intervention uh because a symbolic execution or engine or a prover might not be able to complete it might not be able to say yes I proved it or no I found a counter example it might say ah C3 can't handle this query so you're gonna have to help me out here and that can require some expert human intervention symbolic inputs are 100 and 100 input coverage you're testing every possible value uh so if you prove your invariance with KVM and Foundry then you've they're proven uh this was contentions yesterday the idea of false passes and false negatives I think it's unfair to say that you have false negatives with fussing because well it's not like Foundry comes in or a echidna comes and says like oh actually we didn't find anything so therefore it's safe but the problem is sometimes that's what developers or users think so uh that's why you can think of that as a false positive you can't really have uh or a false negative you can't really have a false negative or false posture with symbolic execution either we prove that this doesn't hold or we prove that it holds either your invariance is correct or it's not or you get stuck and you need a human and then you need to do some things that are easy to try hard to master easy to try means that you can get in on our Alpha release and do it uh hard to master means you might have to call us and we'll help you and we're happy to help you along um here's what it can look like you know Forge tests will run the standard 256 tests for you you can make turn this up to as many million as you want uh with KVM Foundry uh this is a example from rolls talk yesterday uh KVM was able to prove that a specific invariant just held that was written initially as a Foundry test again go and look at his video if you want to check that out uh I would be remiss if I didn't mention that we are starting a research branch and runtime verification so if anyone's research minded or just curious please go to research.rontimereification.com we have a bunch of research challenges there if any one of them look interesting just reach out to us we'll see how we can help you along or if we're happy to hear your ideas on any of the research challenges I think that's what I got we do have 10 minutes for questions I was promised so I've seen a few hints uh again if someone wants to like try this right now like pull up some of your code try to find some few a few invariants I'll just do a little train out of here and we'll find a table somewhere and sit down and work for as long as we have to uh if you go home and you do this later write me at Twitter or at runtime verification.com you can always reach out to us at Discord we're happy to help uh this is a past talk the video should come soon so check that out as well it's important to what what you'll be doing because eventually your environment will contain a division and then all bets are off and you need to know what you're doing cool um yeah so the idea that you can do pen and paper proofs as a really you know robust method is new to me I guess my question is it might be a bit vague but like how do you think of the risk of let's say I take that seriously and I write my proof I convince my team member how do you think about the risk that we've still missed something is it common in your experience if like a client takes it seriously that they they kind of mess that process up um the good thing is that if they do then I mean we'll if if you write invarians and like hey we have a proof we will also check the proof like I mean we're part of the audit yeah we're the ACM Journal you're submitting to or like you know we'll make sure that you're reasoning is out uh because like oh that's a good invariant we trust you guys but let's double check right um ask for pen and paper versus so this is still formal verification someone says like someone said like oh it's not formal verification because it's a pen and paper now it is formal verification it's not mechanized for my verification you wouldn't take a math paper and say oh it's not a formal proof because it's in English like it's still formal proof it's about how you reason and how good you are at formal reasoning um it's about how many nines you need right I mean it's a Swiss Cheese model um you can't you may not ever catch everything that you want to catch the world is chaotic but if you start with your pen and paper proofs that will get you a very long way and in the end like a few of these things might be like like the environment I showed you I wouldn't even necessarily want to mechanize that because like ah there's more interesting things to mechanize but here's the pen and paper proof that's fairly convincing and we'll make a little note somewhere that if anything happens that updates any of these variables we need to double check it right it's sort of like a an index for you to work with um I I sort of grabbed the mic whoever whoever has the mic just go okay so um obviously like part of the limitations of of defining invariance would be like if it's a house and the invariant there's no Thief can go through the front door or come out if you somehow got in right let's say that's the invariant right so obviously the limitation would be that um you know we sort of like didn't define that oh there's also a window you know or they're you know there were roof tiles or there was something to that effect um now obviously you didn't make the statement that that it's like an absolute thing but how do we work towards like um that kind of like uh comprehensive or exhaustive type of um invariant definition well I so I mean to to work with your analogy what you do is something like instead of saying the thief can't go through the front door it's like what do you care about the thief can't get in the house and then you have to say what are all the ways to get in that like you know is there a whole like what can happen is there a hole in the walls and where is there a window can you get in from the roof uh it's sort of the same thing here it's like one thing we do a lot is like a really good starting nodded with is where are all the places where any token transfers happen those are a great place to work backwards from because you know and then there's always inline assembly but let's let's forget that for now um but just look at all the places where tokens or ether change his hands and then look then you can start looking like well if we cover all the paths that can reach those locations and those are all safe then we're safe and then you know of course like you know what what if the token can do weird things if it like can block use or something something you need to keep in mind but um yeah that that's sort of the approach right like find like well take the floor of the house that's the thing that this thief can never reach and then like exhaustively enumerate all the way someone can reach the floor of your house I guess yeah yeah I think so so I mean like a lot of these things like well you know the dev the devs can upgrade the contract and take all your money like that's that's an assumption sorry like but barring that we're doing reasoning who has Mike I have Mike um so in the example you showed where you talked about basic blocks my reaction was like and and reasoning about invariance before and after they're not as it's written they're not necessarily accessible to us to to like it's not maybe we instrument it but yeah I can't really get in there easily with the tools I have in my hand I by hand like Forge and say okay this is an invariant that holds over this if statement or like the Block in there um so so I'm curious like you know how if there is a way I'm missing and then this this also maybe part two is like does verifiable code look different than uh like readable code and testable code because if I'm to I imagine pulling this out into a lot of helper functions that's not my preference in this case so I I'd like to hear your thoughts on that um well so first of all I mean like The Foundry comes with some limitations that you don't have like you know and then very very mature language like Java there's all kinds of Reflections and like python like there's just nothing you can't do whereas you know you this function is internal so we can't can't do a really unit test with boundary um so which is also a good reason to do this kind of reasoning because like instead of having to go through all your code uh with a tool you can just go and say like well I know solidity well enough to say that well the only way this storage lot can be modified is either in inline assembly or somewhere where this is exactly named in this way uh in this specific contract I don't think anyone's made a solidity no there's no yeah there's no other way to round it right now so um so I mean that that's why this reasoning is pretty good like you can actually especially right now with the state of solidity you can track tackle these things on pen and paper quite easily that you can't really do with Foundry um ask for the readable or I'd say that I say they all come together pretty well uh in the sense that you don't have to have small helper functions all over but like like I I again the data structure example right like if you think of your Java hash map as a single entity make sure that like it might be a good idea to have like you know the updates or deletions from from that just be co-located and might as well probably be a function right uh so and it's not about going crazy I wouldn't say like break these out too in in a helper function like we have Burns and we have the issues like that's fine it's only two places um verifiable code and testable well testable code especially now if you're using Foundry uh testable code kind of requires you to put everything public which you know is a bunch of costs that you might not want to pay um but verifiable code I'd say now it just really relies on this that you have all the relevant changes to things that have a clear relationship are co-located uh whether that's in functions or anywhere else and you know right right a bunch of inline comments that say like you know how yours back in this environment and so on uh I'd say that the the enemy of this is maintainable code that's why it's like the good thing here is like well things we don't maintain that much code here like we deployed and then it's deployed um so you don't have to worry that much about like well what if we change the code and then we forget to update the code comments because like we're kind of relying on the idea that things get Frozen here that's one reason that formal methods doesn't haven't really had a breakthrough in you know web 2 or standard back-end development because like you well everything has to be maintainable if you keep if you have to redo your proofs all the time then you know it might not be worth it so the fact the code is Frozen is actually pretty important here does that answer it okay I actually have a follow-on question to that uh right here in the back hi yeah um you you said that you should be doing these proofs only during the uh or when the code is frozen because you can you don't have to be redoing your changes over and over right which is right you're like you don't have to be redoing this work but it's you have something to mechanize the invariant checking you can do it you know not only with changes but you can also get valuable feedback during the development cycle right so and that has other benefits too that you sort of alluded to in your symbolic execution is that you don't have to rely on the fact that you have to manually look at all the places where uh storage is updated you don't have to worry about the fact that you made a delegate call into a library and oops actually that Library had an inline assembly blocked as a secretly uh changing that all gets sort of uh handled for you automatically during mechanized uh proving so um I I just I I guess I quibble with what you've said there that you should only be doing your invariant proofs you should probably be doing it much more frequently yeah I mean I'm I'm more talking from experience like it's it's like I would say like start writing in variants like as soon as you hit your docs like you know you're doing your design start writing your variants keep them up to date in the code realistically that doesn't happen as much as I'd like if you want to be a unicorn and do that I love you but like I know most people here won't do it um that that's sort of what I was I was getting at and especially like yeah if you do your instrumented tests then you know go right ahead it's also like from experience sometimes the signs change enough during the process that maybe teams don't want to invest all that time in because these instrumental tests can take a while to do as well if you want to have some examples go to that alchemics uh V2 Foundry repo it's called that because we're working on uh setting up founder tests sort of like this but like even even more powerful and extensive so you can see some of the work that goes into doing like full Foundry uh checking of a bunch of different invariants but the all the variants came from an audit where we found them and uh wrote like formal English proofs of Lucas over there actually did than that so it's uh yes this paper and a bunch of other things in our Publications are actually really good resources if you just want more examples of this uh this entire section where we just go over like 10 different invariants and give formal fairly formal proofs or hand waves uh about why each of them holds so it's a great place to go and see more examples uh there's also links if you go again to the beginning in the the lecture notes or slightly more extensive there should be links in there uh a kind of a follow-up on that it strikes me that some of this could be related to behavior driven development uh I don't know if I haven't really seen this in the solidity web 3 world but you know think of like a tdd loop but then zoom out so instead of writing a failing unit test red green refactor Loop you're doing a red green refactor loop at like uh app or protocol functionality level so instead of like the standard arrange act assert way that we might set up a unit test in Behavior driven development they call it given when then so given some background when some action gets taken then I expect these assertions at the end and I think it could fit well with like trust threat modeling like actors assets actions I was just curious if you've seen that because when we're doing bdd and I'm trying it out on a solidity project you got to keep those green and so I wonder if there's a way to kind of Drive some of your development within variants that you use in the bdd world you use cucumber which is like um runnable English language so I I thought that might be a pattern I don't know if you've seen that no I haven't but I want to talk to you that sounds great I want to check that out cool hello I just wanted to make one clarification that the inductive proof at the function level is what you need to perform to get the invariant to hold but the basic block level is easier that's why it's presented as an alternative so if you can show it at the basic block level then it holds at the function level not necessarily the other way around so if you can't show it at the basic block level try it at the function level still might hold so does it does it work with Viper they gave him I guess it's language agnostic okay so KVM doesn't actually work over Viper uh so the thing is like well the the thing we're developed now works over Foundry and Foundry works over solidity uh but I mean there's nothing stopping you from setting up your own little pipeline where you build your contracts in Viper test them in solidity with Foundry or just you know hack on Foundry to make it include a Viper compiler and then do the same things because you know it it's all evm at the bottom anyway so uh yeah I'm sure I'm sure someone's going to hack together a Viper extension of Foundry eventually bruh just curious if you had any examples of mechanized invariant tests that you like to look to or that I could look over just I still haven't wrapped my mental like my head around the mental framework for parsing out like what invariants should look like yeah maybe like a mix of English uh like pen and paper invariants and code might be might be helpful yeah actually check out the the alchemix paper for a good like run through of um so there's a section at the beginning that lists some variants in the section at the end that proves the variants uh and in between are just all like the you know um findings reports um with mechanized proofs I don't we I mean we have a bunch of like tested come talk to us like depends on like your background on where you want to start we have just a bunch of different resources depending on what you're interested in your starting level just to make make or die multi-collateral dye proofs if you want like well here's a full uh formal treatment which have some English language stuff but it's also like you know fully formally uh specified at the function level all of it and that's all verified um that's a good example but you know hang around we'll clear up oh yeah yeah anyone in a oh uh anyone in a runtime verification t-shirt is there no Workshop after this Okay Okay cool so yeah we can't hang around here no okay fair enough okay thanks everyone [Applause]