# Solidity Debugging meets Formal Methods - Raoul Schaffranek | Runtime Verification, Inc.

- Speakers: Raoul Schaffranek
- Channel: [ETH Belgrade Community](https://streameth.org/eth-belgrade-community)
- Date: 2024-10-07
- Duration: 28:47
- Topics: People & Blogs
- Watch: https://streameth.org/watch/yt-6Kl4UvWjO8Y
- YouTube: https://www.youtube.com/watch?v=6Kl4UvWjO8Y

## Transcript

thank you so my name is RA shaan I work for runtime verification and I'm a former verification engineer there um and today I want to talk a little bit about what formal verification actually is and how we are working on making it more accessible to uh to individual or to developer teams and to individual independent security researchers so at one time verification we used uh our tooling to formally verify the uh East deposit contract when ethereum went through uh from the proof of work to the proof of stake consens mechanism we formerly verified Unis swap um Lio optimism parts of igen layer so but you know all these are Big players but uh and formal methods formal verification has been proven to be useful to harden your security but we need to make it more developer friendly so that everybody can use it and this is kind of uh the topic of my of my uh talk really so if you have not heard of formal verification today I'm going to talk about a specific flavor of formal verification that's called symbolic testing and uh I want to think you about symbolic testing just as a way of increasing the confidence that you have in your test Suite so in a similar way that fuzzing or property testing improves the confidence over unit testing symbolic testing is just a logical next step to make your test s to make your confid to increase your confidence in your um in your test Suite even more and it's actually at the upper hand it can give you very strong correctness guarantees that in I will talk about in a minute so if you are familiar with fing then you are in a very good position to understand symbolic execution so when we're talking about fuzzing we basically mean we have a test s that's usually written in solidity um and then you leave some of the parameters uh you leave some parameters in your tests and what the fuzzer does it's um it throws random inputs at your test function and then it tries to find counter examples so and at the end the fer tells you hey I found a counter example which is really nice because then you know you have a bug and you need to go back to your smart contract fix this bug you can just run your fing Suite again and eventually the F will at some point say okay your test passed and well this test pass is a kind of where we from a formal verification perspective get really paranoid because what it's actually telling you is I'm not sure I just couldn't find a counter example but I have no guarantee for you that there is no counter example maybe you just need to fast longer so maybe you just need to fast for 24 hours or for a month month and I actually recommend do this like it's it's a no-brainer if you're interested in security just set up a fuzzer that is running on a server that uh that FS your codebase 24/7 it's why not it's it's really cheap but even if you do that for like 1 billion years uh it has still no guarantee that there is no potential bug so what is symbolic testing now symbolic testing um also just takes a solidity test uh and it EXE executes the test not on random inputs but it executed on abstract States so and now the cool thing here is uh instead of a fuzzer you have a prover and the prover can either say hey I found a counter example so great you need to go fix your smart contract or it says I have a proof that no such counter example can exist and that's really a rigerous meth mathematical proof that this is literally impossible or the Prov says you know what I'm not sure um I don't know and then you need to guide the prover you need to provide some custom Lamers and tell it how to make progress so and the ultimate goal is of course Reach This Green State like have prove have proves that your smart contract actually satisfies your test Suite or your specification and a problem with formal verification at the moment is that well the developer experience is not that good mostly common line tools that give you cryptic error messages and we are building a new tool which is a symbolic solidity debugger so and this tool is actually the first like visual symbolic execution engine uh and it you can learn like gradually like I know this space leads a needs a solidity debugger so bad right uh and this one is integrated into Visual Studio code and you can just use it as a classical debugger so you can set the break points you can step through the code um all of that stuff you can even go down to the bite code level uh and uh step over one bite code instruction at a time but the killer feature is really that it also has this symbolic execution mode and this symbolic execution mode visualizes symbolic execution for you so it becomes a gradual learning curve like if you you if you know how to use a debugger then you can gradually make your initial state or your test cases um more symbolic and then by that increase the coverage of your um of your debugging session so and you can uh we have a public online demo that you can go to tr symbolic. runtime verification.com um it you don't need to install anything locally for that it just runs in your browser you can see how it unfolds uh in front of your eyes um okay so let me take one step back and like what is debugging what is symbolic execution debugging is you know other ecosystems have it class like tfy has it Java has it uh you set break points you step through the code you inspect the states of the variables um it's really just I like to think of a debugger just as a guide when you're reading code because well I was I was doing audits a lot and I was executing programs on pen and paper actually so making sure that I cover all the branches and stuff so I figured well a debugger would be so nice it it can help me so much time it can save me so much time so and now symbolic execution is a way of exploring the state space of your smart contract systematically um so that means you have some uh during the execution you will have some abstruct states so instead of for example you have a balance of Ellens that's 100 you say the balance of Andro of Ellis is just X and you don't know anything about X so and when you do this that means there's sometimes your code can take different paths because it does not know enough about the balance of Lis so it can it can Branch so in instead of having like a linear stack Trace you now get an execution Twee or a control flow graph when you're done symbolically executing you either get a counter example or you get a proof of correctness or it gets stuck somewhere and this stuck is really where things are getting messy and where you need to dig deeper symbolic also has a uh we we just launched a offline version of symbolic uh an online version of symbolic that you can just install from your Visual Studio code and this version on Visual Studio code on the marketplace has not these symbolic execution features built in yet we are working on that but this is just a classical debugger and I assume this is a useful tool in its own even if it cannot perform the symbolic execution yet um so we are currently trying to merge like the symbolic execution mode and the concrete execution mode if you still don't get what symbolic execution is just trust your intuition really because symbolic execution don't try to read an academic paper about it like these are very condensed and very deep and super hard to read but actually you are a very good symbolic executor like already so whenever you're reading code basically really every time you're reading code you are symbolically processing it in your mind so let's take this uh let's take this example snippet um so this snippet could be part of a transfer function so it first checks hey is the uh balance that we want to transfer does it um exceed the balance that I have and then it's reverting or in the other case is transferring tokens from one address to another address so now if I tell you um to execute this code mentally from this initial state where we don't know what will be the receiving address we don't know what will be the sending address and we don't know what is the value that we are going to transfer but we know that whatever this address the from address is has a concrete balance of 100 and a concrete and the receiving address has a concrete balance of 200 so now I ask you okay from this initial State execute the if statement and what you notice is that in the if statement we don't have sufficient knowledge to decide if we need to take the then Branch or the el else branch and so what you do is okay you first consider the case where you go to the thenen branch and then you make a like a you like make a little mental note in your head that you still need to look at the El Branch later on but let's first look at the Zen Branch so and we've learned something about the value now because now we know that the value must be greater than 100 otherwise we wouldn't be in this Branch so this is what we call a path condition and then the next statement that you would execute is this revert statement uh so the transaction reverts nothing interesting happens afterwards so we are done with the Zen branch and now we memorized we had a little mental note on the El Branch so we still need to check the El sprin what we do is okay we now know that the uh value must be uh less than or equal than 100 we are executing the storage updat uh one step after another and then we are done so and I did like I did this very slowly um but I bet if you're reading this code you can just do it within like some seconds and that's really you that I'm just saying this because you are an excellent execution engine mentally let's talk a little bit about um the evm you you may have heard that evm is like a state machine and the if I'm not mistaken the initial State like the Genesis blog was mined in 2015 and um well this basically at this stage there were no smart contracts uh everybody had a balance of zero basically and then we did like lots of transactions people deployed smart contracts um and here we are currently at this time and we know so we have recorded like a lot of transactions they all changed the state they changed the balances of the users new smart contracts were deployed and estate is really just all the um all the account balances all the storages of the smart contracts that's what our state is and the every transaction changes the state in some way if it does not revert so now here we and we know that some of these transactions um have been exploiting bugs well and that sucks so but well it it happens and there's most of the time there's not much that we can do about it but we can do something about the future we can try to make our smart contracts more Seeker and find these bugs in the future so the problem is now well we cannot predict really what will be the what will be the next transaction uh and what will be so there's basically an infinite amount of choices for the next transaction and even if we could predict just the next transaction well the game would repeat afterwards so you have this huge ever expanding State space and you know that well some of these states might be buggy they might be exploitable so what's a systematic way of finding these buggy States um in your smart contracts before you deploy them and what we do um I'm going to skip this slide uh what we do is basically with symbolic execution we make it possible to explore the entire State space so and this entire State space it will include the buggy transaction ction and so you can actually see that includes a back how are we doing this let's look at a simple example so um we're doing a uh let's say we are doing a simple transfer from transfer from Alis to Bob we are transferring 10 tokens or from Alis to Bob 20 tokens transfer 30 tokens from Lis to Lis and every like every transaction would lead to a different successor State what we're doing so if you just may maybe one of these transaction has a bug in it right so and if you're lucky you have a test case or you have a fuzzing test or you R A debugger and you found this bug but there's no guarantee the the space that you need to explore is just too big so what we do instead is we execute a transaction from an abstract state so instead of saying we are transferring from Alice to Bob we just saying we are transferring from somebody to to somebody and the somebody's are just variables it's dollar from and dollar two and we don't make any assumptions about their balances we say it's X and Y and then we make an abstract transaction transfer form we are transferring like some value from sum address to sum address and then now we only get two possible successor States uh the first successor state is well um the addresses were different so we credit the One account and we debit the other account the other case is the addresses were the same so the balances should actually not change and executing transactions on an abstract state with abstract inputs that's symbolic execution so you can actually collapse like an infinite possibility of transactions into a single abstract transaction now if you think about fuzzing there's also so one of the problems is you usually fuzz only one transaction there are some fuzzers that can do multiple transaction fuzzing so they execute they randomly generate uh one transaction and then they generally they generate another transaction that follows after um so but well it's a sometimes it can find bus but still your state space is so it's so huge so what we do we do in symbolic EX execution we do something uh that mathematics like to call um structural induction so and this structural induction basically uh allows us to execute a transaction from an arbitrary State and it will end up in an arbitrary State um so we don't need to generate another transaction at the end because we know that whatever follows this state could be subsumed in the initial state of the of the proof of the first transaction that we executed I'm sorry if that is uh if if that is not very understandable um but the thing here is uh the thing that you need to take away from this slide is if you're doing symbolic execution you actually don't need to do multi multi transaction symbolic execution it's sufficient if you just do one transaction and it will be will be generally enough to cover all the possible states that they want to cover so in essence we reduce this problem of an ever increasing State space that you need to explore to just one single abstract transaction that you need to explore and that you need to to test or to debug so that's a huge achievement uh it makes like it gives you so much greater confidence in in your smart contracts because now you know okay now you have the peace of mind that uh your father didn't say green just because it was not uh it was not uh fuzzing long enough um so you you actually get a proof that this cannot exist um temporal granularity I'm going to skip over this slide because I'm running out of time let's let's look a little bit at the user interface of our debuggers so um as I said the states are basically uh all the storage and the account balances and stuff but that is only at the transaction level so if you look at the the state before transaction and the state after transaction okay this will be your state but during a transaction there will be additional States like your evm state there will be a program counter there will be a stack there will be Memory um so and our debugger basically allows you to look into all these lowlevel uh State components of the uh ethereum virtual machine and it's uh gives you basically a full view of what's what's going inside in your virtual machine um from a classical debugger you would also expect that you are able just not to look at the lowlevel data not just the memory not just the storage but you also want to look at solidity variables right and we are working on that uh the problem at the moment is a bit that the solidity compiler does not generate sufficient information for us to uh to decode variables reliably um but the ethereum foundation is actually working on what they call the East debug format and we are kind of waiting for this format to land uh in the compiler so that we can actually do reliable variable decoding and then it will be even easier to use what's our road map for symbolic uh we just released an open beta version so I told you about this website tr. symbolic. verification.com and there's this is the symbolic execution version that runs in a browser it's it's not it's very limited demo to be honest um but we also have this like just the classical solidity debugger and it's available from the visual studio code Marketplace you have steps through debagging you can do it on the bite code level um and we are really working on a on a good Foundry integration so that you can just use debug your Foundry tests uh I put this under the one column here it's it's not ready yet implementing Foundry cheat codes is something that takes some more time uh our next step is well part of symbolic is open source so the visual studio code extension is fully open source but there's some components that currently run on our servic uh and we eventually want to make these other components also open source um as they become more stable then uh we want to uh make it even more convenient for users to use and uh really to look at the state exploration tree um so there will be a nice graph visualization feature and then just as I just said we working on the East debug format and then eventually we want to make this debugger also able to debug onchain transactions so one last thing is formal verification is mostly used in the context to prove program correctness but it also allows us to uh build an entire level of new applications so you might have heard that formal verification proofs are like compute intensive and that's true finding this proof finding these proofs is very difficult and it takes time it can take hours but once you have the proof you can actually verify it really quickly it's a it's a different like different complexity class it's really simple to do that uh and we have a proof checker for our proof objects that just not even 200 lines of code and that enables us basically to put formal verification proofs proofs of program correctness on now these proof are still very big so you want you don't want to put them on chain as they are but what you want to do first is you want to uh you want to zkn you want to snar them so that they become constant size and yeah I'm I'm very happy um Ilia from pi squared who will be speaking after me is doing exactly that so that's a great company and they are building really a new kind of infrastructure uh for Block chain that enables entirely new applications um and they are using formal verification to do this all right that's all I've got for today I hope it was not too confusing for all for you all please try out this debugger uh install it if it's not what you expect it to be then we are very early in development we literally just released it two weeks a one week ago so if it's not what you expected talk to us like and tell us what do you want from a debuger so we are very flexible and prioritizing features um and if you have an idea for a cool feature uh yeah please let please let us know so and all this uh well open source development depends a lot on uh benefits a lot from Community contributions so I would be H very happy to talk to you all thank you we we have time we have time for Q&A session if you're open towards it that's great so if there's yes Mike mic is on the way thank you can I ask two questions yeah I have a quick one uh when you said uh you have open source on the road map are you open sourcing the prover as well uh the prover is actually open source so that's one of the components that's open source it's called Uh uh the the Kover so we are building on top of What's called the K framework which is a very general like theor improver specializing on proving stuff about uh programming languages and virtual machines so you can yeah it's it's completely open source okay I'm surprised because I know Sora is not open source and so I was very yeah exactly amazing that you have so you can actually uh and we have another tool that's called control and that is uh basically just symbolic testing so you it's a combination of a Foundry and symbolic execution so you actually can use control is completely open source if you have a Foundry test Suite uh you can just run control on top of it to get like really to hammer out all the edge cases um it's a it's a very nice user interface it's not perfect like uh but it's completely open source and you can actually run it on your own CI pipeline if you want to so that's a great thing of making sure that your code base stays intact awesome thanks and my second question is about the well I didn't try it yet we have a quick question maybe I will have get the answer but um you mentioned that uh on uh testing transaction um debugging online onchain transaction is something you are working on and I'm curious what are what's the difficulty how how is it different any different from testing a local setup um it's actually well one of the problems is that when you're debugging locally we can just uh compile it with our own uh parameters so we can actually in some cases we want to turn off compiler optimizations because either it's compiling to slow or also compiler optimizations sometimes mess up the source maps and um for onchain contracts you always have optimized code and optimized code is in it's it's it's more difficult to debug than unoptimized code but uh it's not really like it's just taking time to develop it it's it's not too difficult to do it just taking time does that answer your questions we have one more question in the front please go ahead great yeah uh the question is uh can you show uh like highlight the boundaries when you should do formal verification because it's quite complex things and how long approximately it takes for example for average code like 100 lines of code how long does it takes to build the WM model for that um yeah so for example how control works is you don't actually need to write a new specification if you have a Foundry test Su already so this uh huge step that makes formal verification often very hard is you need to write a formal specification in some weird formal verification language but now you can all only you can use it in you can do it in solidity but yeah compute is a different like how long actually does it need to take to find these proofs um that can range from minutes to hours to even days um depending on the complexity of your smart contract um so I really recommend uh well you can you can do it for simple task on your own customer Hardware um but it's definitely something that you want to enable on your CI pipeline because then it does not block your computer so be every time basically you merge something into your master Branch you want to trigger control onto your CI Pipeline and then um if you have time to wait another 24 hours before you deploy your smart contracts then take this time it's just another day uh and it maybe it will find a counter example and it it can save you from from losing lots of money does that answer your question do we have we have time for one quick question in case there's more someone in the audience yes thanks hey no oh okay thanks for the presentation and question is what differ your debugger from Foundry debugger for example because uh what I saw is the same we can trace memory stack storage Etc and Foundry has a very uh beautiful visualization of state which different uh so The Foundry debugger first of all it's a common line tool it's a terminal user interface and it's not hooked up to visual studio code um also I think our debugger well it's it's very early yet but uh one of the Prime features that that we are working on now is like the symbolic execution path and I think that's nothing that is planned for Foundry yet um what are other differences um well we allow you to inspect the evm state at a deeper level so uh we're actually working on making like the full entire evm state inspectable every single component every single bit while The Foundry debuggers like taking a more practical approach and they are mostly uh visualizing ing the memory and the stack I'm not even sure if they visualize or if you can inspect the storage I'm not sure I I don't want to say anything else but our goal is really make everything inspectable and it's a w r please give it up one more time for [Applause]