How To Get Security Under Kontrol by Palina Tolmach

Transcript

so it looks like we can start uh hi everyone my name is Paulina uh I am a verification engineer at rtime verification where I work on developing the tool control uh that I'm going to introduce today uh runtime verification is a technology startup providing Security Services to blockchain as well as some other Industries uh and in blockchain not only we do traditional security re reviews or audits but we are also experts in veloping and using formal verification tools and in this talk I would also try to explain why that matters for security um by definition security is the state of being free from danger or threat and as you probably know at least in blockchain that's pretty much impossible um even though we should try to get as close to that as we can um if

we look at the defi protocol and the the process of executing its transactions we would see that there are actually a lot of components in this technological stack and unfortunately the issue might sneak into any of them um so in the case of a defi protocol there might be issues in the solidity code of the protocol itself there can be compiler bugs front end vulnerabilities um as well as some other potential issues uh in the lower level um layers in this Tack and also unfortunately insecurity so there is no security in isolation right um even if solidity code is correct it can still be exposed by a bugs in compiler or in CPU a cosmic ray um flipping some bits in some computers R

and so on and so forth uh but the good news is is that there are some tools that actually help us make sure that all parts of this stch are secure and control the tool I'm going to talk about today uh is working on the solidity um and evm smart contract level so on the slide um I have put some of the existing techniques that can be used for a security and correctness Assurance of smart contracts um based on the level of confidence that they provide us um in terms of the security of the implementation we are looking at and um I do know that uh saying that manual review provides us with this low lowest confidence in the results um is debatable but what I want to say is that generally uh we have no guarantees in

terms of how much the particular auditor um how much time he's going to invest how much uh how much effort this person is going to invest in this review how confident he is in this particular with this particular implementation um so it is very dependent the quality is very dependent on the particular individual at the same time uh static analysis provides us with um a bit more consistent results in that matter um this usually operate on the high level source code or some intermediate representation and they typically perform pattern matching to identify some vulnerabilities uh some common types of vulnerabilities that exist in smart contracts uh sler is a prominent example of that and that is it they are actually very useful uh with

searching for this common vulnerabilities in smart contracts um however unit testing fuzzing and ultimately formal verification provide us with more and more confidence uh in the correctness and security of the implementation we are analyzing and now I'm going to explain why exactly so that is let's let's consider this example that I have prepared for this talk um let's assume uh that your project uh uses this library to perform some arithmetics and generally in solidity development uh there are several libraries implementing fixed Point arithmetics so that is just one of them and assume that your project um so your project uses this library and this Library releases a new version and this

version among others contains this change so even if you looking at diffs in your dependencies which I think you should do um you might still I guess there is a chance to not notice this particular change so what this function does is multiplication so we just multiplies X and Y and uh normally it only reverts if there is an overflow that occurs in this multiplication uh but I have also added another condition uh why it would revert so unfortun it to revert if x is also equal to this very specific very particular hardcoded value and I just tried to disguise it very lightly so it looks like a bit mask and it looks less suspicious but uh generally for the purposes of this talk I I didn't try to

to hide it very well um so so that implementation is actually based on solid uh that is a library and there is a link to it on the slide we actually proved it correct so this particular function is safe to use if you're not using this modified version uh so let's talk about why analyzing that is challenging and this function uh that is a gas optimized implementation that is why it's implemented right in assembly and together with gas optimizations it also provides some challenges for um for reasoning about it security and one of the problems is that um because it's an assembly static analysis tools provide limited support for it because they usually operate on this high level um

high level of the uh B the source code itself and some high level intermediate representations um in addition to that uh for some of the vulnerabilities we actually do have compiler checks that are just inserted automatically and starting from version 0.8 solidity for example inserts uh this automated checks for overflows however in this case um if the smart contract is written in assembly you won't really get any of these built-in compiler checks at the same time uh in this particular case we have just added this this custom condition for this function to revert so it's not standard problem there is no pattern that would detect it so none of these techniques would really help in this case and you actually have a better chance of fighting this just by doing

the manual review um but asly is less readable than source code so this bad readability also provides additional challenges um when it comes to this to the security of this particular function um so what we can do uh in order to uh try to reason about this functions correctness we can write some unit tests and here on the slide I have examples of some of these simple unit tests what they do they call this small what function that multiplies two values uh with some with some concrete values so here we have this test small what and what it checks is that multiplying 5 by 0.5 returns 2.5 and that works so that provides us little bit of confidence um in the fact that this function actually

works correctly because well at least it can correctly multiply these two values um unit testing generally is very useful very usable it should 100% be part of any um development process however the problem is that it provides us with this very limited information about all these possible behaviors that this function can have we don't really know how it would work on some other values other than the concrete ones that we have tested before you can increase coverage by just adding more tests um but it would still be hard it would take a very long time to enumerate all possible values and U you can also it it is recommended to increase coverage by adding more tests that explore different execution path so if you have a revert condition you can or

an if statement you would like to write some tests that expose both of these branches um however the problem is that some branches may not be obvious so in addition to this branches that we see in the source code of these conditional statements um compiler automatically inserts some of the checks itself so for example because these functions all the functions here are not marked as payable which means they can't accept eer so if this contract received eer if any of these functions do uh then it's going to revert and that is the compiler introduced check so there is more there are more branches than you think most of the time and the summary here is that unit tests are very useful can expose some logical flaws but they only explore a single execution path uh in a smart contract

so what we can do to increase coverage further uh we can do fuzzing so we can write a more informative test and we can fuzz it um so here on the slide um that is a Foundry test so Foundry is the development framework very popular one it's written in Rust um so what it lets us do is to write this uh more interesting parametric test uh as you can see different from this unit test we were looking at it now accepts two parameters X and Y and what we do in this in the body of this test we're just checking that if x multiplied by y doesn't overflow then the result we are getting from malw for multiplying these two values is the same as we would get if we just multiplied them in solidity

so that is the readable implementation that we can actually inspect ourselves and make sure that it's correct alternatively if it does overflow then it should revert so that's what we are trying to see here this test is going to fail because there is also this specific revert condition that we introduced ourselves and this test can be fuzzed so so the general idea behind fuzzing is I think very well explained by this tweet you can see on the slide uh with a joke saying that the QA engineer walks into a bar and orders one beer zero beers a lot of beers minus one beer uh so that is what fuzzing does automatically it just keeps executing this function with random values uh hoping to find certain edge cases and generally fuzzing also is very useful it can help identify un cover some edge cases and some problems

um however that it doesn't find the issue in this particular case and so it cannot find this revert that occurs if act this has this super specific value um because it just is too specific for it to get randomly generated in this limited number of fronts and that is the summary of the fuzzing part so fuzzing examines a lot of different execution path it can uncover a lot of branches and explore the the corresponding execution path however there is no guarantee that it will examine all of them and and um here is how control can help so different from these other tools that we have considered um that perform concrete

execution control uses formal verification which means that instead of running this code concretely we're actually going to mathematically prove um that the implementation in solidity and the one the gas optimized one U are behaving exactly the same way um we have this Foundry integration in control so we are going to actually anal ize the same test so this test mwood function and the one in the previous slide are exactly the same and we'll just run control on top of this test and we will see that even though the test is the same the results are actually different so control is going to tell us that the proof had failed and it had failed if it fails if x has this specific long value which actually

corresponds to this zerx FF um that I have used in the original implementation that's just the decimal value for it um so to summarize um because control is different from this concrete uh from the tools that perform concrete execution since it is powered by this mathematical the act of mathematical proving control can explore all execution path and uncover all these possible H cases and uh due to its integration with Foundry if your project has Foundry tests you can just give control a try and uh try to run it on the existing test which means that there is little to no uh need for some additional specification uh control is open source and it's a

common line tool so um we actually do recommend trying it on CI uh we have this GitHub action uh that you can find the link to on the slide so you can actually um add it in introduce it to our CI so the test can be run uh either periodically or they can be retriggered by any code change and that would help ensure that no C changes or no changes in the dependencies um introduce any issues that could have been CAU by formal verification um and in addition to that the example I have used in this talk um is actually quite quite simple uh because I wanted it to fit into 15 minutes uh but control can cover a larger set of properties uh including security properties correctness um

conformance to this standard we use it ourselves internally we use it in the engagements with our clients so you can actually try to run it you can run it on a larger code base and verify some more interesting properties in addition to this equivalence checkin that we have done today between the solidity implementation for a uh a specific function and a highly gas optimized one so that it can also provide you with some guarantees in terms of how exactly um your gas optimized and not readable code behaves uh in addition to that uh we also plan to generate ZK proof objects for this this proofs that we generate using control which means that um this proof objects would certify that uh the code code that has been verified and the

code you're analyzing sorry and the code you are running and the code that has been analyzed uh is the same and um this Pro objects could also include some verification artifacts that we can that we produce during this um mathematical proving um we actually are raising at the moment so if that is something you're interested in investing please let us know and finally one other thing I would like to mention is that in addition to control we actually have more tools uh that we developed at runtime verification so um please feel free to explore them and one of these tools is symbolic uh symbolic is a debugger for solidity uh and similar to control um the actual verification happens at the bite code

level so uh even though uh the input is this solidity contracts and solidity tests uh we actually as you have seen we have no problem um analyzing inline assembly and also the quote that you the code that is being verified is also the same code that would be deployed on chain um and you're going to execute there so symbolic is the as I've said it's a solidity level debugger uh but since it is powered by control and formal verification you can explore all possible execution path and you also have access to this very detailed um evm level information about the execution stack uh and generally just the state of the program uh the state of the contract

that you are looking at so it has this vs code interface so it's very it's very usable um and you it hasn't been released yet but uh there is a demo that we have published you can find it uh via this link that you see on the slide and in addition to that we are currently looking for beta testers so if that is something you would be interested in uh please let us know and please sign up um that is all that I had for today uh these are some of the socials using which you can stay in touch with us and follow our updates uh please feel free to join our Discord and uh share your feedback or report any issues you might have encountered when using our tools and these are also the link to control

documentation and GitHub as I've said it is open source and it works with um similarly works with Foundry projects so that is something you would be interested in please give it a try or um let us know and yeah I guess that is all for me today thank you very much