Automated Vulnerability Fixing in (DeFi) Smart Contracts

Transcript

wait a moment mercy all right bonjour i'm paulina i'm a phd student at nanyan technological university and i'm going to talk about how we can fix vulnerabilities and bugs in smart contracts automatically so the end result would look like this we give our tool a condition that should always be true and then if the doesn't hold somewhere in the code then our tool automatically suggests the way to fix it so here we're fixing the bug that allows stealing tokens from a decentralized exchange and therefore it violates this property that you see on the screen making the balance of a protocol decrease why it shouldn't so now let me explain how that works um we've just seen an example of why we should care about smart contract bugs so d5 protocols store a lot of money they

work on smart contracts smart contracts are code code contains bugs in d5 protocols bugs usually mean financial losses so we want to avoid them also that's bugs bunny and he will accompany us in this presentation because of his name um now let's take a look at the actual bug that cost i think eight million dollars to the protocol that had it that is a basic transfer functionality of an era c20 token smart contract so how does it work let's say we want to transfer five tokens um and to do that we record the balance of a sander record the balance of the receiver or recipient we perform the transfer and then we subtract five tokens from the center balance and record that in blockchain we also add five tokens to the recipient balance

and we record that on blockchain two that's it right so at first glance it works correctly and it actually does in most cases um but i'm showing you this for a reason and the reason is what happens when i should when i'm trying to transfer five tokens to myself so in this case again we record the center balance which is 10 that's my balance and we record the recipient balance which is again 10 and again it's my balance now when we hit send we try to transfer five tokens and then we update the standard balance we record the result it is now five but then we also add five tokens to the recipient balance that we have recorded before and it becomes 15. so do you see what's happening well i had 10 tokens and i would have 15.

that means that i just made five tokens out of thin air by trying to transfer them to myself and of course that's the bug that shouldn't happen one thing i want to say about this code is that if you're not familiar with solidity please take note there is a required statement um i think it's the for the search statement there um that's basically a conditional statement so what it does it checks the condition that is there if it is true then the execution of the function continues if it is false the execution of the function reverts the transaction reverts all the effects made on the blockchain state by these transactions are averted all right so what can we do to fight bugs first of course we can ask developers just not to write the buggy code well that's a great idea it doesn't work there are also of course tests and

verification they probably can help us identify the bug but even if they do which is not always the case they still won't fix it so what we are trying to do here is to automate the fixing step to help the developer um we want to take the buggy smart contract that has an issue and then we want to automatically transform that into some better fixed version so that's a very very general task so in order to make it feasible we need to answer three questions first of all how do we decide if a smart contract is buggy and there is something that we should do about it second how do we generate a fix for a smart contract that is buggy how do we actually perform this transformation finally after we generated the fix how do we make sure that it is correct and

correct here means that first of all it fixes the issue we found at the first step and second it doesn't introduce any additional issues which can also happen so let's start with answering the first question which is how do we determine that the smart contract should be considered bugging so apart from mainstream ways to find bugs in your quote which are task team or just looking at it really carefully there are also automated ways to find bugs first of all there are vulnerability detection techniques so they are based on patterns which are defined for some common smart contract vulnerabilities this could be for example integer overflow so what these techniques do they have this pattern and they try to identify if the code contains this pattern in this case it becomes it will be considered buggy

but the main issue with this approaches is that they can't detect anything beyond these hard-coded patterns an alternative to that is to perform property-based analysis which tries to detect if somewhere in the code the property that should always hold can get violated so the property just says what the smart contract should do and what it shouldn't do so the property that is violated by this specific example is the transfer invariant it says that the sum of the sender and recipient balances before the transfer and after the transfer should be the same it shouldn't change um so in this case the property is violated if the center and the recipient address are the same and we can use it as an indication that the smart contract is buggy and should be fixed

but the computer doesn't really understand this natural language properly so we need to encode it in some way that it doesn't understand one way to do that is to just try the simple test cases that perform a transfer and then check the property afterwards we can for example write the task on the left on the right for me that will perform this transfer in the correct way so the center and the recipient will be different people the property will hold that is the example of the correct valid behavior of our smart contract we can also write a second test case that will exploit the bug so it will contain a transfer from the from bugs bunny to himself and the property will be violated so once we generate some fixes for our

smart contracts we can run these test on the fixed version again and then that's how we can actually decide if the fix works because the failing test shouldn't fail now after we have fixed it and the passing test shouldn't fail either um of course in reality we can't really or shouldn't ask the developer to write those tests um so later in the talk we'll see how we can automate that but for now that will be our framework so we'll use a property to help identify bugs in a smart contract and we'll also use test cases we wrote to assess the fixes that our tool will generate so now let's see how our tool is actually going to generate them in general whenever you fix some code manually or automatically the fix is

usually just some patch that introduces the changes to the code so there are several ways to fix our example one of them is to just add a restriction on the sender and recipient address which will just not allow them to be the same so if i wrote this fix manually that would be it but we're generating it automatically so the decision we need to make is whether we want to perform that on the bytecode level or the source code level bytecode level has several significant advantages so first of all it is always available in constant in contrast sorry to solidity code that may not be public most importantly bytecode is what exactly being executed it is the program that is run by the evm and also in contrast to solidity which has to be processed by the compiler

first which might contain bugs which also happened or it might introduce some optimizations we are not aware of so generally using source code is less safer in that regard but bytecode also has a very significant disadvantage it is extremely hard to read so that is the same statement you can we have also seen in the source code and it's extremely difficult to parse it if you're a human being not the evm and it is also very important that we understand the fix we are going to apply to our smart contract it's very important that we understand what is actually happening therefore our choice is to perform the repair on the source code because it's very easy to inspect visually and the availability question is also less important because we target our tool for the developers so

we assume they have the access to the source code they wrote all right so we decided that we'll work on the source code and source code is basically text and if you're a computer it's very difficult to work with stacks because it's not very structured so as everybody who works on source code instead of using the actual source code we'll use the abstract syntax tree or ast so that is the tree-like structure you see on the screen it can be produced by the solidity compiler automatically so notes there represent code elements and there you can see the ast for the first line which is an assignment and the request statement um which is a third line so we have an s team um we know that the program contains the bug we want to fix the bug fixing the bug means changing the code

so how do we actually change the code well answering this question relies on a very important observation that even in buggy programs most of the executions will be correct so another another way to say that is the developer gets most of the things right therefore if you look at the actual buggy smart contracts and if you compare the original version with the fixed version you will see that the div between them is actually quite small it would be one line or maybe a few lines max so a straightforward approach to search for a fix in this case is to just brute force our way through all the small changes we can find for this program so we can change or mutate the code in one of the following ways first of all we can insert a statement that is actually the fix we are looking for we

can do that in the ast and then respectively in the source code we can also replace statement or parts of statements so let's say we want to change the sign in the required statement we can do that in the ast and in the source code as well you know maybe that could have fixed the bug one other thing we can do is rearranging the order of statements we call that moving all right but as good as computers are at brute forcing checking all possible changes in this code can still be too much so we need some way to optimize our search for the patches and one way to do that that we use is to just use some heuristics so we looked at a lot of smart contract source code from vulnerable smart contract data sets or just actual postmortems and we noticed

that some issues are just way more common than others so these include for example missing required statements um slightly inaccurate required statements missing variable updates and so on so what we do is we first prioritize those patches that would fix these issues we look we try to synthesize them first and we check them first before we try to generate some other statements so that would actually generate us some pretty good one-line fixes that are very small but in some cases there are more complicated issues that require a several lines fixed so in this case we need to generate a fix with a single line first and then we need to mutate that further as you can probably guess again that generates us a very big search space for the patches that might be hard to

analyze so we need another optimization to handle that and in fact program repair techniques borrow some ideas from biology and evolution to do that so they use something that is called genetic algorithm so what's that um well first we need to generate using the strategy we have just discussed we need to generate some initial set of patches for example we generate five random patches then what we want to do we want to select the best patches out of what we call in evolution terms generation one and then we'll mutate those best patches further and we'll just drop the rest of them as you can probably guess we also need a criteria to select the best patches and we already do that um remember the test cases that we wrote

before we can use that to assess the quality of the patches so as we have discussed a good patch fixes the previously failing tasks meaning that the property will now be satisfied and they also don't break the tasks that worked previously um so using that uh we can actually select the best candidates uh we can move them to the second generation and then we will mutate them further and we'll just repeat that process until we find the best patch that you know satisfies all the conditions that we wanted fixes all the tasks um so that is actually the patchy generation technique that completes the first version of our tool so that's good but if you were

concerned by the fact that we are only using two tasks to assess the quality of patches you were right and i'll see why i'll show you sorry all right so in the current state our tool will try to take a shortcut it will generate a required statement with an invisible condition you can see on the screen so a variable it checks that a variable is not equivalent to itself which of course can never be true it can never be satisfied the call to this function will always revert from the point of our tool and our tests that actually looks like a correct fix because if the property hold holds before the transfer and then nothing happens then the property still falls right that makes sense but of course that's not something that we can use we want people to be able to transfer their tokens so

as you can see we need a better way to automatically ensure that good behavior is preserved now let's see what options do we have for that okay so first of all we can just add more tests that is a widely used approach and it actually would make our approach overall work better but as all the techniques using tests are the patches will be subject to test overfitting so that's very similar to how model machine learning models um they just learn the test case they are trained on instead of generalizing the behavior that they observe our tool will do exactly the same thing we will just try to find a patch that is very specifically tailored to exactly the data set that we have and it will work for these test cases that we have

in our dataset but it will not generalize beyond that it may not ever work on anything beyond these tests um one example of that in our case would be the following so we can add a test that looks like this where we actually performed the valid correct transfer so the sender here is the basebox bunny and he transfers six tokens to daffy duck so we can check um that if bugs bunny does that his balance decreases by six if he transfers six tokens well a patch that could have been generated in this case would look something like this we already know that the left side of this expression is always invalid so it's not helpful at all but still because of the second

clause it will allow the execution if the value is equal to six so even though it would work for all the tasks that we have it's not really usable it doesn't generalize so you might guess that instead of tests we need some approach that would consider all possible behaviors not just some specific behaviors that are caused by concrete values we used in the tests and that's what we have formal analysis techniques for um and especially symbolic execution because analyzing all possible executions of a program is exactly what symbolic execution does now let's see how symbolic execution works it might be a bit too much to wrap your hand around symbolic execution in one slide but that's a general idea so let's

consider this simple program that is given on the slide there is one conditional statement checking that x is less than or equal to y therefore this program has two branches this condition can either be true in this case that would be equal to x or it can be false and that can be equal to y so symbolic execution assumes that the variables used in this condition are symbolic and symbolic here means arbitrary or any that means that x and y can take any possible values that an unsight integer which they are can take therefore both of the branches in this case should be explored they can both be true symbolic execution for the analyzed code memorizes or records two types of

information first of all let's explore the true branch first so the first type of information it collects is the path condition it's called pc on the slide so the past condition is just a condition or we also call it a constraint that represents the condition that should hold in order for this path to be analyzed um then the other type of information is the variable updates so whenever we execute this path we also want to record that that would be equal to x if this condition is true so we record this the path condition first that access lesser equal to y and the variable update then we also repeat this process for the

false branch and that pretty much gives us the comprehensive view of how the program actually can work with so these are the only ways it can be actually executed so what happens if we symbolically execute our example so for simplicity let's assume that bunny is always the sadder it will limit the number of paths that we have in this presentation and the recipient can either be bugs bunny or it can be daffy duck val corresponds to the amount being transferred and it can be any unsight integer so since it can be any unsight integer when we symbolically execute the program we record some variable updates but then once we reach the required statement we know that both of this both of the cases are feasible so either the required statement is true and the

execution of the function continues or it is false and the transaction reverts so then if the if it didn't revert then we continue updating some variables we record that information uh in the symbolic execution tool state as well and then we also need to check the assert so we already know from our previous discussion that the property can either hold in this case if this header and the recipient are different or it can also fail so the property may not halt if the sender and the recipient are the same address then sorry then from the previous discussion and our manual analysis we also know that if the transaction reverts um then

the property will just always hold so we do know uh for sure from our manual again analysis um that this condition is not possible so it's not feasible in our example for the transaction to revert and the property to be violated but we know that and the computer doesn't know that so since we're trying to automate this whole approach what we want to do is to inform computer about that as well so what we can do for for that is to use an smt solver so without going into the details smd solver can be viewed as a tool um into which we can feed these conditions the path conditions so these constraints that we have that balance should be less than val and that the property is not holding and then we can use the smt solver to ask it can these

conditions be satisfiable in other words that means can this ever be true in this case smd solver tells us that no is not possible that is unreachable no point in analyzing this further we just drop that but we still have this three other execution path with their path conditions that we can analyze so we also invoke the smt solver to check their satisfiability and they are satisfiable so all of this can actually happen so and a very exciting feature of an smt solver is that it can generate concrete values for these satisfiable path conditions that symbolic variables should take in order to drive the execution towards a specific execution path so we can use that to generate test cases automatically

however we already have seen that using test cases might be insufficient so we need a more formal way to actually prove that the original behavior that was valid and the behavior of a punch smart contract they're actually equivalent and that is one more thing that we can use an smt solver for so in a very similar manner as we use the smg solver to check if these conditions are satisfiable we can also ask the smg solver is program one equivalent to program two um so that's what we are going to do for our original and fixed smart contracts so in order to use an smt solver to do that we need to actually try to check the opposite so we write a condition saying that the original smart contract is not

equivalent to the patch smart contract then we can ask the smg solver is that satisfiable and if that is satisfiable it means that the smt solver managed to find some concrete values for which the programs behave differently meaning that they are not equivalent in contrast to that if it couldn't find any solutions it means that they behave exactly in the same way they are equivalent we found our fix that's it but the issue is smg solver doesn't understand solidity so we can't just fit that into the smd solver what we can do instead is to translate it into something that smt smt solver doesn't understand and that is logical formulas so we just need to take that and translate it into a logical formula um the logical formula should just

encode all the behavior the whole behavior of this function um so in other words it should summarize that we would call it summary since we already have analyzed the three possible execution path of the contract we already know exactly what's going to happen in each path so we just need to combine this information about individual path into one big formula that will fit to the smg solver so the formula should convey the following idea there are three ways in which this function can be executed either the required statement is satisfied and the property is satisfied as well or the required statement is satisfied the property is violated or we just revert that's it so that's exactly what we're going to build in a formula so i don't want to show actual formulas they are unreadable so just

assume imagine there are formulas in these rectangles um so first of all we of course want to collect some information about how the variables are updated then when we see a required statement we know that there are two possible ways in which the program is going to be executed so we split that into two clauses it's either true or it is false if it is true then there are some more variable updates that we also record in summary and then we check the assert which again splits the first class into two possible ways as we have seen before that is a summary then we can repeat the same process for the patch smart contract it is a bit different it now has a new line of code so the summary will look in a slightly different way but if out of those out of those

summaries we only choose the path of sorry the parts um which correspond to this valid behaviors from the original program we want to preserve and then ask the smg solver if are they equivalent then it will tell us that yes they're equivalent in fact that is the one of the fixes for this program all right so that's the final state of our framework for today which now has symbolic execution automated test case generation and equivalence check-in so you might be wondering why we're still using test cases if we have equivalence check-in and the answer is because equivalence check-in is very confidentially computationally expensive so we can use test cases to just quickly you know remove the patches that obviously don't work these are just some examples of what we

can do with that so first of all we have already seen that we can automatically change the constant to the correct one in the required statement we can generate some required statements like access control which before we added that this code violated the property that the owner can only be changed to a code that was provided by the previous owner and we can also fix something a bit more complicated such as for example the following property for the pull smart contract where you could send your tokens to state them so there was one type of token that had an address which you could take there and it should have never been changed in this pool um but you could reset this value in the initialize function which was supposed to be only called once

but someone forgot to set the flag that it has been initialized to true so you could have reset this value but you can't anymore if you have fixed that um all right so that basically concludes my presentation um the short summary is that we can fix bugs in smart contracts automatically we can do that in practice we can do that using formal techniques that can be used for other to solve other problems beyond verification as they usually um yeah on a side note we're setting up a spin-off startup company to commercialize the research in this direction and we're focusing on the builder first approach to security um we are currently raising funds so if you're interested please drop me a line to this email address and there is also my twitter account

in case you need anything else too all right thank you very much [Applause] [Music] any questions thanks um have you explored the techniques to prune the results like for example using fuzzing to compare different implementation and do for example differential fuzzing to check if the implementation analysis oh yeah i think you can use exactly what you saw differential fuzzing should help the only thing is that if you're using these formal techniques if you're using formal verification oh sorry smg solvers to do that you have somewhat better security guarantees because you're

potentially you're covering like the complete behavior it's very exhaustive on the other hand it of course comes with scalability issues so if you have loops or if your program is just very complicated or if you want to for example build a summary for several functions in a row that won't really work that well how do you deal with the initial state for the symbolic execution engine because in this example you have you have like one function but how do you deal like if the function with a state variable or stuff like that um well you mean if we have several functions in the in the execution trees yeah like like you have a function with a bug and within this function you are going to read a stat variable and

the value of the state variable might depend of previous call or like you know something else um how do you deal with that well if if the so this particular function did change some state variables um so we actually we just record that into the summary and we assume that the value for correct path the value should just not change for the state variables um but yeah so the issue here is that what do we do if our execution trace that let's say the vulnerability has several functions and they all have state variables that we update they call each other yeah so that's um in all the examples that we had we had just some a few a few functions so it wasn't that long and there were not that many variables so we could just

mutate that using this technique and it actually did work in it worked pretty fast it was i think some minute time or something like that but then of course i mean theoretically that is a bottleneck that's true thanks really interesting thank you very much hello uh thank you for uh the presentation so uh i was wondering how do you carry new version uh of uh of language uh with your solver so imagine there is a new version where uh um it's not the same semantic so how do you carry that

oh we do the same thing as so here i had an example of how we built this summary for this for the original version right and then we just repeat the same process the same process for the patched version so we symbolically execute it once again we again build a summary for that and that's it so and then we just ask the solver if these are equivalent and the solver can infer if if they are even if they look slightly different um and it's the same for um like in solidity eight and before there is overflow that is uh that is not carried with the compiler so so it's like the same um yeah so honestly we do this on solidity 0.5 so we have our own symbolic execution engine that is solidity level

and it currently works with 0.5 but i think we are porting it to other versions as well there are slight differences in semantics so we'll just encode that information in the summary if there is some okay thank you thank you thanks all right well thanks a lot [Applause]