Automatically Strengthening Formal DeFi Specifications using Program Mutations with Chandra Nandi

so how do these techniques work so here I have a very very high level overview and I'm just going to take the example of the Satori approver itself but a lot of the other techniques use something similar so you have some code so imagine that being some smart contract that you wrote in solidity and you have something called a specification and these tools like the Searcher approver are going to take the code take the specification and try to check if the code matches the specification so one of two things will happen either the tool will tell you that the code matches a specification or it will find a counter example which is a concrete instance where the specification is violated okay so this is how a lot of these tools work and if you want to know more about the Searcher approver itself I encourage you to go take a look at that the QR code over there there's a really nice workshop being offered where you can learn more about server approver so this is really good news so we have these really cool tools that can you know analyze your code for you and it can prevent a lot of bugs so this is all great but if you are a critical person you might be saying that well uh formal verification is just guaranteeing that your code is just as buggy as the specification right so if you have a bug in your specification then formal verification will not be very helpful for you because it will just say that you know the code is equally buggy and not only that in fact formal verification will tell you that the code has you know the same bugs as the spec and only those bugs it doesn't give you any more or less guarantee so what does this suggest this suggests that perhaps we should take some time and evaluate the specifications themselves right before we actually even verify our code we should make sure that the specification itself is correct so that's what this talk will tell you so we are going to look at one specific technique that you can use to improve and evaluate your formal specifications okay so uh before going any further okay before going any further I want to give you a small example so maybe uh some of you have actually seen something like this so this is a smart contract in solidity and it's doing board accounting so it's a voting mechanism and you can read about it more later but I'll give you enough information in this talk for you to follow along so what's happening here so we have uh the name of the contract which is border and we have this function called vote right so vote is taking three addresses first second and third and we're gonna vote to one to all these addresses so what's actually uh what is this code doing so first we have these required statements and um okay so first we have this require statements the first one says that you know the message sender should not have already voted right and the second one says that the candidates should all be different anyway so the the second line there which you can't see but uh yeah great uh the second line says the candidates should all be different and then in the third line is where the actual voting happens so uh well before that happens you just set the the voted status of the message sender to true and then you just vote right so you give the first uh candidate the vote of three the second one two and one and so on and so that's really simple and uh we also have this other function called voted and voted is just simply returning the voted status of some address so this is a very simple program now what are some interesting properties about this program that we you know we should make sure are true so here are some that I could come up with so one property that is useful is perhaps we should make sure that everybody votes just once another property is that we should make sure that when we count the votes of the candidates we are doing it right right so when a candidate gets a vote that should be increased another important property is that the winner should have the most number of votes right that's pretty obvious um one other property is that maybe the voting order should not matter right like I can be voting in any order but still the winning candidate should always be the same and the final property that I could think of is everybody should get a chance to vote right like no other address should be able to control your ability to vote so these are some properties that you can check using formal verification but now the question is is this enough like did I think think this through like are these all the properties that actually matter or are there some properties that I forgot and more importantly you know this is written in English right so if you want to do formal verification you want to First convert that to some logical representation and that representation can also have bugs in it so we have built this tool called Gambit and Gambit is a mutation testing tool so what is mutation testing it's a way to automatically introduce bugs in your code so that you can check whether the specification catches those bugs so this is actually a pretty well known technique in the software engineering community and we have been using this for formal verification and so what Gambit does is it stress tests your formal specifications to give you more confidence that it will actually in fact catch bugs in real life so how does it actually work so you give it your original solidity program and it's going to generate some mutants for you right so it's going to modify the code in simple ways to generate a bunch of mutants and these mutants have a few properties so the mutants themselves are actually simple they have only one small change in each mutant and the mutants are not generated by combining a bunch of smaller mutations because that actually makes it hard to figure out why the mutant fail verification or pass verification okay so once you've generated these mutants we will verify each of those mutants using the same original specification right so the specification is unchanged but we're just going to use it to verify each of these mutants and so again you know just like we saw before the verification is gonna either tell you that it passed or it failed so what does it mean for a mutant to pass verification so when a mutant passes verification it's actually bad right it means that something is missing in your specification and you should go and evaluate your spec and maybe improve it and if the mutant fails verification what does that mean that means that you did a good job right like you wrote a good spec and it you have some evidence that if there is a real bug that your spec will actually catch it so let's go back to that border example so here is a mutant that Gambit actually produced so what it did is it just set the the voted status of the message center to false instead of true and now you might be wondering that well when I wrote my spec I really thought this through right like I wrote some really good properties this mutant is definitely going to be caught well it turns out that it doesn't right so if you actually verify your pro this program using these specifications it's actually not going to get caught so this mutant is gonna get away so what do you do it turns out that you actually missed a property so one property that you should add to that list of specifications is that once a person has already voted you you're really changing the status of the voted of that address to to true and this is not a property that you know the original list had so you should add this and then your your specification is going to catch this mutant so that brings me to a few different types of uh uh you know ways in which the specification can be wrong so here's one this is one example so sometimes you just don't think about all the properties right so you just missed your you know thinking about some particular thing and your specification is just not complete so you can make it complete by running mutation testing and finding you know introducing bugs that are not being caught and then you can think about the why it's not cut and maybe improve your specification another thing that can happen is that maybe you actually did think about the spec but there was a you know you didn't like convert that properly to a logical expression right so maybe you miss you're missing some assertions or maybe you're missing some Clauses in some existing assertions and then finally you know we're all humans so we make mistakes so you can just simply have a typo in your specification and this will also be caught with something like a Gambit or you know mutation testing so these are some of the you know ways in which we have already seen uh specifications having you know loopholes and running mutation testing on your specification uh really helps find these kinds of problems and so as part of Gambit we also have this really interesting visualization uh so to build this visualization uh we actually collaborated with a company called evil martians so I highly encourage you to take a look at them they're really good at making uh interactive uh tools so uh what is this visualization doing so this is still talking about that border example so a few things are happening here so we have these green circles so the green circles are your specifications so those are the properties that you actually wrote and the gray dots that are inside the green circles those are the mutants so if a Green Dot is inside a sorry if a gray dot is inside a green circle that means that the green circle caught the gray Dot okay and if you want to look at this visualization you can check out the QR code but you should open it on your laptop because it's not meant for um like a like a phone so uh so you can see that you know in this case we have you know whoever wrote the spec did a good job right so we have this additional information here which is coverage so coverage here really means the number of mutants you killed or your specification killed so in this case we actually caught all the mutants right so none of the mutants that we generated uh pass verification so this is actually good so you want your cover is going to be as high as possible um we also have this notion of a solar rule so Rules by the way are the the properties that I showed you earlier so what is a solar rule a solar rule is a rule that catches you know a mutant just by itself so there are no other rules that catch the same mutant so you can see that we have a bunch of solar rules here and so there's no intersection between the greens between green circles so if that is the case that means that there's no overlap in uh the properties that are being encoded in the spec so that's kind of an interesting uh you know metric about your specification you can get from a Gambit uh so on the left panel you also see all the properties that you wrote and here's another interesting piece of information you can get so it's split into two two groups so you have the successful rules that cots are mutant and you have an unsuccessful list they didn't catch any Mutant right so maybe this also tells you uh how you can change your specification and maybe not even have some you know properties because they're just not useful properties and um you can also click on the different patches and you can see the actual diff of the mutants so what was changed in each mutant with respect to the original program and um yeah so that's uh so that's the tool right so we've built this uh really interesting tool called uh mutation using mutation testing called Gambit and it does two things it automatically generates uh bugs are false in your program and for each of those generated buggy versions it uses your formal specification to verify them and if you can verify some of the mutants that's bad you should go and improve your specification and if you can't that's good you can use that as a way to sort of you know give some kind of metric of how good your specification is so uh thank you for for your attention uh so just to summarize you can go check out the tool here we also have a pretty good documentation if you're interested to learn more about it and feel free to talk to me if you have more questions foreign [Music]