Solidity Debugging meets Formal Methods

Transcript

[Music] hi uh welcome everybody to the third day of East pra my name is ranik I'm from runtime verification I hope you all got like a good coffee in the morning um so and this Workshop is uh it's an interactive session um so if you bought your laptop you can actually follow along but you don't have to so you can just also follow on screen if you want to um I will introduce my company uh in a minute uh but before I do that I want to start the installation process so because I know that can take one or two minutes um so here's a quick agender of

today uh we will have an installation party of symbolic which is a solidity debugger and it doubles as a symbolic execution engine uh then we have an interactive session of just that that just shows how you can use symbolic as a classical debugger where you can set break points where you can step through the code where you can inspect the storage and the memory it's all integrated into Visual Studio code um then I will do a little bit of an introduction to what symbolic execution is because uh well that's not a well-known concept uh out of Academia and finally I will show you the extended mode of symbolic which is this Advanced symbolic execution mode so

um to participate in the in the demo or in the better you have to get an API key from this website um you can just uh yeah take your time the website is symbolic. runtime verification.com and everything you need to do is you just need to log in and then at the uh after logging in you can do it with uh with GitHub with Google or with metamask you will get an API key at the bottom of the dashboard that you can copy um I will uh I will bring up this slide later on if you didn't have the time to copy the website Ur So it's symbolic. runtime verification.com

so and then there's uh four steps that you need to take so create a free symbolic account that's the first step that I just described um then you need to install the visual studio code extension um and you can just just go to open your Visual Studio code or or codium um if you're using codium and then just go to the extensions and search for symbolic and symbolic is spelled s i m b o l i k so it's with a k at the end and I will get to that later um and then in the extension configuration you need to copy paste or you need to paste the API key that you just got from the website and you need to have Foundry installed on

your system so these are the the basic requirements [Music] um so let me just show you I can do that at the same time so that we match the speed so that was the wrong website so it's symbolic. onetime verification.com uh log in with either Google metamask or GitHub I use GitHub I hope the the network connectivity will be not a problem doing this demo all right so you copy your API key from this field please don't copy mine I will uh

just um regenerate it after our Workshop here and it won't work forever oh there's a question yeah I'm let me see uh okay I haven't seen that one should I try maybe with another one yeah if you have metam mask maybe yeah I think that's the what most users are using um yeah but uh fetch me after the uh fetch me after the talk and I will take a note and take this to our website team

so you copy the API key you open Visual Studio code uh and then you search for symbolic is this extension and you go to the extension settings and you just paste your II key in this field in the first field so I already did that and then uh I will use this demo repository uh for this uh for this Workshop you can also try to use your own uh Foundry project to follow along

but you don't have to do that I recommend really use this uh uh use this example project so you can get clone onetime verification symbolic examples and I will give you some minutes in the meantime while you're doing that I will leave that slide open and I will just introduce uh a bit of my background and a bit of the background of my company so I'm rran uh as I said I'm working as a formal verification engineer for a company that's called runtime verification we are a security company and we do uh well we do all kinds of security stuff we do uh audits or code reviews but we specialize in doing formal verification and we have uh different

open source tooling for doing um formal verification for solidity but also for w based ecosystems so and some examples of projects that we formally verified is we formally verified Unis swap V1 we formally verified the beacon chain deposit contract from the ethereum foundation uh we are currently doing like a long running engagements with Lio and with optimism and so you figure well all these are high-profile customers but we actually want to so it's it's been proven that formal methods um are useful to harden your security but the the problem at the

moment is a little bit that uh well we don't only want that uh like high-profile customers with lots of money can do it we also want that every developer and every independent security research is able to run his own formal verification so and that's why we developed symbolic uh and symbolic is really uh it's my it's my hard project and it's really um like a tool that should lower the entry barrier to formal methods for everyone so you just start with a classical debugger H you can set break points and stuff and as you learn more how this works you can then Advance into this symbolic execution mode and transition into becoming basically a

formal methods expert without having a college degree are you good yes okay great uh everybody's good with the slide here so I can continue all right so uh it's demo time so if you have checked out this repository uh that I showed you um there's uh two solidity files in here uh this the first one is the font size readable for everybody or maybe not is this better for everybody all right so uh this is a very simple ESC 20 contract it's intentionally simple so that it doesn't attract from

the content of this presentation of this Workshop which is really the debugger itself so it's like any other es20 contract but it has a uh it has a critical back in the transfer function um and uh well we will maybe you can spot it it's a like a a textbook prime example of a of a bug um so it has all the classical functions it has a it has a transfer function it has an appro function and it has a transfer form function and all these uh like the balance the symbol and the decimal they are just public field so it's a very simple implementation um so now how can we start debugging this contract so um and

if you have used a debugger Like Remix before what you need to do is well you first need to what compile this project uh then you need to deploy this contract on chain or on a local test net um then you need to get the address of the freshly deployed contract and you need to do a transaction uh to to invoke your um to to invoke the function that you want to debug um and we could have built a user interface for that but we think that debugging configuration or a debugging session should be reproducible so in our case we don't have a user interface for that but instead you just write solidity code to set up your

debugging session and I can show you how that looks like so here we have this uh under under the test folder we have this debug esc20 file uh that's just inheriting from our uh contract that we want to debug and it has some uh some Constructor that takes no arguments um it's minting some tokens to some addresses so that we can actually use it and then it has basically just some repper functions uh for example debug mint calls the mint function uh and it's specify okay who want who do we want to Mint to and uh how much uh tokens do we want to Mint so and now the critical thing is if you want to start debugging something um

your contract must have uh a parameter list Constructor and the function must be uh the function that you want to debug must be must also have no parameters so I mean the the the the contract under test like the buggy C20 token of course it can have a it can have parameters like a transfer function without parameters wouldn't make any sense but the debugging contract it must be parameterless so and then you see uh right above like every public external function with no parameters you see this debug button and that's just how you start a debugging session so I will do this um for for the debug mint function and what you see is uh on the right hand

side you see that it's automatically um compiling your project and uh then it automatically does all the deployment stuff and the under the background it uh deploys the contract to a local test net uh and it just jumps right into your transaction so and it always stops at the very first line of the contract because usually in solidity um while this debugger works on the evm level and usually there are some op codes generated that get executed before you even jump into the function uh and we will like in a minute I will dive a little bit deeper into uh bite code level debugging but for the moment let's stay at the solidity level so what we can do now is uh we can just what you

would expect we can just step into the function this brings us now really to the first line of the function that we are want to debark if I step into another time uh you can see that I'm now in the mint function of the buggy esc20 contract so that's the actual function that I wanted to debug um let's take a look maybe at this initial State and see uh what what we can see here so first of all you will notice you can insect the evm state so you can you can see what has been the call data what is the current program counter you can see all the values on the stack currently you can see uh what's in the memory and you can see

inspect the storage and the return data um so I assume that most of you would have expected to be able to inspect solidity variables and this is a planned feature it has just not shipped yet so at onetime verification um we like to build our Tools in public and uh do it informed by feedback from the community from the users that are actually using it so we could either have like implemented that and then release the entire tool like one year later or two years later uh but it will never be in a perfect state so at some point you just have to release a Tool Push It Out by the way it's most of symbolic is open source the components that are not open

source yet will be open sourced over the next weeks or months as they become more stable uh but it's completely free to use of course um so and inspecting solidity variables is something that we are call ly working on and we will ship this gradually one data type and one data location at a time so but at the moment you get basically a full view on the lowlevel evm details in this variables view on the top left corner of course you can also um see the call Stacks so you can see that we are actually coming from the debug mint function and we are now in the mint function um you can well just step over step over code uh you can can of course

set break points and then directly execute until the breakpoint is hit if it's hit um yeah that's uh that's the the basic the most basic functionality so and one word about the storage so you can see that storage slot number six has uh this cryptic value I think that's the owner address um of the of this contract so if I'm going to execute now over the next statement of the balance off uh so when I increase the balance of the of the receiver of this mint you you can actually see now that the that there's another storage slot that is assigned

2,000 so why it's 2,000 um let's look at the debug esc20 contract we called mint LS 1,000 tokens so it should be 1,000 but in our Constructor we uh we minted 1,000 token to Alice before so now in total it's 2 2,000 tokens so this storage slot belongs to uh belongs to Alis balance um and then we are updating the total supply of our smart contract and you can see that in the storage slot so total Supply is now 11,100 so all what you would expect uh the storage here if you noticed um at the moment it only shows

you the warm storage and that's again a feature that we are uh like there's a difference in the in the evm that tells you what is warm storage and what is Cold Storage warm storage is all the storage slots that have been um accessed during the execution and cold storage is everything else everything that was all the storage that was not attached um and at the moment it only lets you inspect the warm storage so only the slots that have been accessed but uh well we have a basically we have a pending pull request it just needs to pass uh code riew until it's merged uh before it's merged and then we will also have cold storage so you can actually inspect the entire state of the evm you can inspect the uh

full storage you can inspect the full memory the full stack the program counter um yeah but uh well we just released this beta basically last week so it's a it's a pretty new tool to the market so please be patient if it's uh if it's not perfect yet and actually we appreciate if something is something in this debugger is not as you would expect it um like if you were hoping to get a solidity debugger uh and finally use it in in Visual Studio code and that's not what it is then just let us know so so we can make it happen the good thing is we just like started developing it so we are very flexible in terms of what

features to prioritize next all right so uh if I step over this function it brings me back to the debug Min function nothing interesting happening now um and the debugger always drops at the last state of your smart contract so uh because the the final state of your smart contract just before the transaction is finished is usually very interesting uh there you could see hey did it revert for some reason uh did it uh what's the return data and stuff like that so we always by default we always stop at the at the um at the initial state of the transaction and at the final state of the

transaction okay so let's uh look at maybe at a more interesting example so let's look at this transfer function maybe again it stops at the initial state of the smart contract I'm going to step into the transfer function or the debug transfer function first so uh uh I'm now the debug oh I'm I'm hiding all this with my big head so maybe I can just do it this way uh so I'm going to step into oh I can just scroll up man I'm

dump so now you can see where we are so I'm going to step into the transfer function um so there's a required Callos here where we check that our balance is sufficient by the way I'm going to hide this one here uh so it's checking that we actually have enough balance to transfer uh this check should pass so now we are just memorizing hey what has been um our balance before the transfer then what has been the balance of the receiver before the transfer and now we are basically just uh debiting our account and crediting the receiving account du mid event and we turn two because that's

what the standard of um ESC 20 demands has anybody spotted the buck yet okay that's great uh because then I will show you in the next text test actually this debugging session did not trigger the bug so it it's uh yeah I'm not surprised you didn't spot it so let's look at the so I'm going just to step over this one again it stops automatically at the final State and I'm just going to dismiss this debugging session so now let's look at a more at an even more interesting example even more interesting so this debug transfer

self so now we are transferring tokens to ourselves um so you see I'm calling the transfer function and I'm saying hey want to be the receiver of the of this transfer and I'm also being the sender of this transfer so I'm just uh well transferring to myself and what should be happening is uh nothing my balance shouldn't change at all right so because I'm like just sending money to myself so at the end it should be as before so there's also this assertion statement at the end that uh validates this so I'm going to debug this

one and I'm going to set a breako this time because we haven't seen break points in action yet breakpoint and the let me set it in line 32 that's where all things are still good um so up until here everything has been fine so and now we are updating the balances of the receiver and of the sender of this transfer right so I'm going to update the balance of the message sender first and let's look at the

storage uh so my current balance is 10,000 tokens after updating the balance from the message [Music] sender it becomes 9,000 as expected so now uh yeah there you have a you have a question oh yeah greaten uh if the value I don't know we do this uh uh we have this um balance off check we check that the balance does

not exceed the value so yeah yeah you can you can so yeah and you're right so the problem is now let's see what happens to my balance if I execute over the next statement so you would expect it to go back to 10,000 right [Laughter] so you would expect it to go to 10,000 but it goes to 11,000 so I just like created money out of thin air or I just created tokens out

of thin air by just transferring tokens to myself I can just basically increase my my balance to to infinite um the problem is here that uh you see the message sender and the two address are actually the same and the bug is here where we use used we use the cash balance of the receiving end um from before doing the before debiting the message sender account so that's the problem here and um that was a so this bug it may look superficial right so you have to like be careless to introduce it into your

contract or you have to do it on purpose uh but actually I have seen this in a in a contest basically the first audit contest that I ever did H contained the exactly this Buck like exactly in this configuration uh and this was my first contest as I said and uh it was confirmed as a as a critical sity issue and I I I thought yeah I made it now I'm going to be rich uh I called my mom told her hey you can retire now we are going to be rich don't worry I buy you a nice house uh which year it was year 2021 yeah and uh like I got

7017 out of this High surity finding $17 yeah so I I'm I'm still not rich so that's why I'm here today um yeah the I mean the finding is super critical and it has been acknowledged but it was filed by I don't know 20 contestants uh who were doing this audit so and uh the way that the code platforms work is the more users report the same issue uh the less the payout do you know approach that you milk it first and then you return 90% second again do you know that there is a novad approach that you milk it first and then

you return the 90% to the project so sorry I this is this monitor is way too loud so it's too loud so uh what do you know that now is the approach of the hackers that they milk it first project and then they return the 90% and keep the 10% as the white heck uh yeah uh for the for the other and for the record that's the joke but it's happening yeah it's it's not really whad hacking if you are like just like expecting to get a to get a profit out of of it right so it's just I I think if you're right teching then you should disclose vulnerabilities

confidentially like take a proper route and not just exploit it and then because even if you're exploiting and then intend to return it like uh returning from a hack returning money from a hack can also go uh can also go badly uh for example we have seen like people try to return money and then it got exploited by a me b or something like that so yeah uh so if you're really white attacker then always always choose the the honest rout and disclose it uh confidentially I I remember that there has been the discussion recently that actually the white hackers do not you know get that uh I would say like satisfactory both recognition and and

the Bounty because some projects they just squeeze down the bounties or refuse you know whatever is being found out they do not concern those as a high file or high risks uh and consider those as a low risks so um there's like a gr area where some people turning at to into the you know white hacking of the hack first and return later yeah I see that yeah I think it's a yeah it's a matter of uh security politics basically okay so but has everybody El now now understood where this bug is coming from okay I see you all nodding that's great um so nothing interesting is happening

after this bug was triggered now I just minted tokens to myself critical bug not very nice uh and I see really um that I have an exception an assertion failure at the end of my debugging session so because I put this like this is like a test case basically this is like a unit test that asserts at the end that the balance before should match the balance after if I'm just transferring money to myself and the cool thing here is uh well you need to you don't need to set a break point anywhere to trigger it so I'm going just to clean all break points cool thing is really you can just restart this debugging session uh and directly execute it and because this debugger automatically

stops at the final state it stops here at this assertion as well so that's a nice way of also just doing unit tests it's a poor man poorman's way of doing unit tests basically um that brings me to the next feature that we are planning to do so um well you probably already have a Founder test suite for your smart contracts uh so what we are currently doing is we are implementing foundaries cheat codes uh into the this debugger so that you can actually just uh if you have a found a test you can just execute it right out the wi out of the way and pranking and um assuming things about your initial State they will all just

work as as just as in Foundry um so you don't need to write like a debugging reper contract like we did in this case uh for for many cases you can just reuse your existing Foundry tests basically also as a configuration for your debugger and the nice thing is here well also in Foundry tests are just code they are committed to the code base they are reproducible so um it's a very good way of doing proof of concepts for example if you have a um if you're doing if you're doing audits if you're doing a code contest or bug bounties and you need to come up with a proof of concept I think the debugger is a very nice way to visualize them so because writing a code of proof of concept is uh one thing

but then you also need to explain it to somebody uh maybe to the developer team that you're auditing so and that's really nice because they you can just send them to the debugger and they can like step by step reproduce your proof of concept and literally see where things are going sideways um okay we are at uh halime um I wanted to show you a bit about yeah let let's do this real quick um okay I'm going to I wanted to talk a little bit about bite code level debugging but I'm doing to do this very quick now um so and I'm just taking taking the the debug function here is a uh the the Min function here is an

example so it automatically stops at the first line and what I'm going to do now is um I'm going to the call stack and right click open disassembly View and this opens this nice disassembly view let me just put it side to side with a source code all right uh it's maybe I need to doesn't fit on the oh so now it fits on the screen uh it's not not perfect not ideal um so but now on the right hand side of on the right hand side of this column you can basically see the dis bite code of the smart contract and

you can see that there the first instruction is a push operation the second instruction is also a push operation then there's an M store um and you can just step over the bite code level as well so uh and I I if you like reading bite code at first is a little bit intimidating uh I have to admit this um but it's a very like like this debug is a very good way of learning how debugging how the bite code actually works so a push operation just pushes an item on the stack so I would expect this that this uh number hexadecimal 80 is on top of the stack after I executed over this first um bite code instruction so let's see what's our stack yeah it's it says 128 which I assume is just the

decimal representation of hexadecimal 80 so now I'm going to push another um constant onto the stack and I can see here live how my stack changes now I'm going to do an M store an M store operation will basically pop the top apperance of the stack it will pop these two items and then um WR something to the memory so if we look at the memory now it should be all zeroed out it's user interface is not perfect yet but you can see the uh memory is all zeros so if I execute now over this m store operation um the items for my stack are

gone because the uh um mstore operation consumes them both and my memory has changed so this constant uh hexadecimal 80 has now been written to this uh memory offset um what's Happening Here is well the solidity compiler basically so the memory of the evm is just a linear memory it's ever expanding to the right um and the solidity compiler when it allocates new variable or uh a new value on the memory it always do does that by pending this value to the right hand side of the of the memory um and

this this special memory location here just tells the tell solidity where is the next free slot free offset in our memory so that's just how solidity Works solidity reserves some scatch space it calls it scatch space at the beginning that's memory that's uh just used internally by some internal generated code but all the variables that are allocated in memory are then um well are are appended basically to the to the memory okay that's very nice of course you can also set uh bre points on the on the bite code level um that's really

nice uh yeah the way that it looks weird here on the on the on the right hand side is because basically how you can read this is well this is the address of our smart contract that we executing and this uh suff this uh suffix here is the program counter yeah there's another question yeah thanks uh since we're running out of time uh this is awesome that that the debugger is inside the vs Cod what would what is the any other like um exception or added value contrary to where the founder debar uh so oh Foundry debugger yeah Foundry has this build-in uh build-in

debugger it's called a forge debug uh it's a common line tool first of all uh so it's not uh connected to visual studio code at all um and it does not give you uh so it's just a matter of taste like if you are a commment line person uh then you would prefer the forge debugger if you are a visual person like me you just prefer working in Visual Studio code um but I think we have like uh more feature plans like I will show you like uh in the second demo I will show you like the symbolic execution features and that's something that is only uh it's only possible in our debugger now that's not possible at

the forge debugger at all and also sorry I I I saw your question one minute um and also uh I think the for spec debugger or the forge debugger uh does not attempt to decode variables at all um and we don't do it at the moment but we have it planned so uh that's the the key differences but it's a very nice tool actually I used Forge debug a lot okay there's another question yeah so this is kind of technical but um is this implemented using debugger adapter protocol so that you can connected with neovim and Helix and uh other editors as well yeah thank you for bringing out this question I was was hoping somebody asked me yeah this is all implemented on the debug adapter protocol so you can uh

this is just this it's like a networking protocol for debuggers and the nice thing is you can develop a debugger separately from the user interface so and then just connect it to different idees so in this case we have connected it to visual studio code but in the future uh we might also connected to I don't know to emac uh even to remix um if they are open for that or basically any IDE that supports the debug adapter protocol on their side so we do it on our side yeah go ahead just remarks thank you for pointing it out because that would be awesome to to connect it towards the 7702 you know the new transaction type which is going in

pectra uh I'm not an expert on this new transaction type so yeah it's just it it it will allow to execute the uh the bite code within the within the context of the EOS musically uh the E object format or no no no no no different one there another one okay yeah uh let's talk about this uh like fetch me after the talk so that sounds interesting but I'm not an expert on this topic okay so uh uh we have 20 minutes or 23 minutes 17 minutes left okay it's less time than I expected uh let's do a little bit of theory for before we come to symbolic execution uh so you might have heard

that uh the etherum is basically a state machine uh the network is in a current state and you do in transaction and it modifies the state and the state is basically all the storage of all the smart contracts all the balances of all the accounts that's that's your entire State and then you do a transaction and the state changes now uh so I think the ethereum the the initial state of ethereum was created in 200 15 if I'm not mistaken uh and then we recorded a bunch of transactions uh the state kept changing changing changing we know that uh some states in the past have been exploited due to backs and now we are

the present so and now here we are and we try to avoid situations like this um but that's very hard to do given that we cannot predict the future we cannot see what will be the next Transaction what will be the parameters of the next trans transaction so even if we could predict just the next transaction well the game would repeat right we we would have we have an infinite amount of options just for the next transaction and then there's another infinite amount for every possible successor State uh after the after the next transaction so this is a huge expanding State space and how can we actually make sure that our smart contracts are safe from situations like

this how can we make sure like you can think of if you're doing a debugging session you're basically following one of these paths so and there's an infinite amount of paths so how can you actually make sure that you well find the path that leads to this bug and this is where symbolic execution comes into play um so here's a simplified example basically zoomed in into this uh uh into the formal picture so we have a transfer form function we are calling it from an initial state where Alis has 100 tokens Bop has zero tokens We call we could call this function with different parameters transfer from Alis to Bob transfer from Alis to Alis this amount

10 amount of tokens 30 amount of tokens and every single transaction will give us a different uh successor state so in in one of the successor State Ellis has a balance stand of 90 and Bob has a balance then of 10 so in another one Ellis has 100 Bob has zero tokens um now symbolic execution is the way of exe sorry is a way of executing transactions um but leaving the concrete parameters of your transaction leaving them symbolic so first of all you start in a and by symbolic I basically just mean variables so if you look at this initial State this is now a symbolic

State that's why it's yellow uh I always imagine like symbolic states must be yellow so we have just a generic balance of a from address that equals anything that's called X and we have a balance of the two address that equals y we do a transfer from the from address to the two address with an unknown amount of value so we cannot see that actually right so ah let me see if I can H this this is not perfect okay just just trust me so we

have in this yellow box we have a variable here we have a variable here we have a variable here and then we have the two abstract or symbolic successor States uh one where the balance of the from has decreased and the balance of the two address uh increased and then we have the case where the from address and the two address are the same address so that's the buggy case that we just explored in our debugging session and then the balances should not change so the interesting part on this slide is like here you have an infinite amount of concrete uh transactions that you could follow and that you could try to debug and maybe one of these basically only

this transaction only this debugging session will trigger the bug um and in this case in the symbolic case you just have one um you just have one abstract uh debugging State basically one debugging session and it will eventually definitely trigger the bug because symbolic execution is a way of systematically exploring all the reachable states of your smart contract and I'm going to give you a demo right now um and and even if you have not installed uh the visual studio code extension you can just try out this demo at symbolic. rtime ver try. symbolic.

runtime verification.com there network is not the fastest but all right so here we have another smart contract we have the famous W EA contract uh it's completely unmodified but one change um I just mentioned that for com completeness that is we change the solidity compiler version because our deburger is not is not well tested on older compiler versions and newer compiler version is giving is giving us uh additional extra information um so it does not match the bite code of the deployed rep East uh contract one to one

but this is just to demonstrate the concept so now I have this w e contract and I want to to say debug the transfer form function so one thing that you see here now is that uh the symbolic execution mode does not have the same limitation oh I should increase the font size okay so one thing that you can see here is that this symbolic execution mode does not have the same limitation as the concrete execution mode in the sense that um you can start debugging functions even if they have parameters so that was not possible with a debug

with a concrete debug execution because when you doing concrete execution you always need to know what are all the concrete values that you want to debug uh with symbolic execution mode you can just then just leave them open so I can just start debugging this uh transfer from function and now let's let's first look at what is the call data here um going to make this all clean this user interface a little bit up you so if you look at the call data you see that there's a this uh hexadecimal constant which is just the selector of the transfer form function

and then you see that there's this plus bytes operation and that is a well that is a that is a function like uh that's that's a symbolic term basically um and basically it says well the call data is our function selector uh plus some variable that is encoding The Source address uh plus some variable that is uh encoding the destination address so if you look closely you can see here that there's uh it's saying Source if you can look here it's saying destination and then uh not visible on the screen right now there's another parameter appended at the end of the correlator that is for the amount that we are going to transfer now let's look at what is the our storage of the smart

contract and that's very interesting because it just has this cryptic value in it and this just says well our storage is fully symbolic that means our storage could really be anything we don't make any assumptions about what is the shape of our storage and what are the contents of our storage could be anything really and now we execute um now we execute over this code and we just track and modify the variables and what you see here now I just stepped over the first statement and you can see now well the debugger oh I have to scroll

up well the debugger stopped at two different positions uh it first stopped at the require Clause because there is a branch that is reachable that violates this requir clause and symbolic execution really explores all the different branches so it has to stop here and say and tell us well uh we found a branch that is throwing an exception here but there's also another branch that just passes this require clause and then just goes to Line 6 64 so and if you look at the call stack now you can actually see that uh we have different branches and one of the branches paused on an exception and the other one paused on a step

so um this exception Branch I'm going to select it here it's not doing any interesting be Beyond this point um it just reverts your transaction and you're done with the execution so if I'm just going to execute over it it will just disappear so that leaves me now only with the with a branch that uh passes line 62 so now I have statement um and I don't have sufficient knowledge about whether this if statement is true or false like in concrete execution when I know all the concrete values of the variables um I can always say okay this if is true this if is false um in the

symbolic case I cannot do this so what we need to do is um or what the debuger does is if I execute over it you would see it branching again and one of the branches um would stop at line 65 and the other Branch will stop at line 69 so I'm going to do that there see and actually it's not just two branches like I predicted it even for me like I'm as I'm a formal verification expert for years now but even for me it's sometimes really hard to predict how many branches are there uh so in this case there are actually three branches and uh why is that there's only a single if

state M but if we look this if statement is actually a compound operation so there's actually uh it's a it's a conjunction here and that means when the left hand side evaluates to false uh then we can just directly or when the left hand side yeah when this part evales to false then we know the rest then we don't need to look at the rest of the condition we just know it's going to be fult so we just step to line 69 but could also be the case that this part is true and uh this part of the of the conjunction is false so that's another Branch because it has a like um well it has different

side conditions so that's why we see three branches here and two of them actually stopped at line 69 so you can see that here and one of the branches stop that line uh so only one of the branches enters the then branch um and so you might wonder okay now what are the constraints that must be satisfied for example in this if condition like in this branch that is like that is stopped at line 65 and you can actually go and inspect what we call Path conditions so a path condition basically tells us hey for every possible execution

that passes to line 65 all these like logical formulas must be satisfied and you can see there's quite a lot of them um and they are not super readable at the moment uh we are working on that we are like always trying to improve our user interface uh just why are they looking so weird um so you have have to have a formal um uh you have to have a logical language to express these constraints about your variables so and in our case uh we are using something that's called

The Cave framework and these are basically cave framework is based on matching logic um and these are just matching logic formulas uh given in a very weird syntax so the goal is here ultimately we want to look make these uh constraints uh look more like solidity Expressions so that they become more natural to read for a solidity developer um they look scary at first but that's I promise you that's just you get used to reading them um so for example here uh let's pick out this side condition that says the message

sender equals the source address and then that's negated so it says basically the message sender does not equal The Source address and I think that's one this one is coming from uh this part of the conjunction of our statement so Source address does not equal the message sender and you can see that in the in the constraints here so [Music] um yeah I can I can like now step over every single uh line of code if I want to and see how my uh like how my control floor graph unfolds um but I will do

something else instead I would just restart my debugging session and what I will do now is I will just execute without setting any break point and remember that the debugger automatically stops at every final state so in concrete execution that was only just a single final state but if I do that now in the symbolic case I can see really all the possible branches all the possible control flows that my program can take so I've just done that and let's see on our call stack there are actually how many branches are

there 1 2 3 4 5 6 6 7 8 9 10 so there are 10 different branches um just for a simple transfer form function so and if you would look at the code you wouldn't see those like I I cannot predict those but that's ultimately what you have to do as an auditor really if if you're or if you're a security researcher and you're reviewing code you really you must consider all possible cases because bugs are always or all like critical bugs are often hidden like in some edge cases so and what symbolic lets you do is it really forces you to look at all the possible edge cases and

you can see the side conditions that are attached to uh to each branch and you can see which of these branches maybe there's one of these branches that's doing something weird so there's certainly there's a five branches that are reverting should they be reverting um and there's a like then four branches that are uh that are successfully terminating and do they do that in the correct State like we can just pick one of those uh branches and then actually um see if the if the storage is actually what uh we intended

it to be and is the stack yeah stake is not that interesting but basically is the storage uh in a correct shape now um is it expected or is it unexpected is it returning the correct data um we can all see that okay one last comment here now is uh let me go back to my slides yeah so uh yeah we are doing this we Dev Ving this debugger we it's it's pretty new it's uh most of it is open source right now some components are still closed Source but will be open sourced over the next

weeks as they become more stable we have some other um uh open source tooling for example we have control which is very nice control is basically uh it's Foundry but instead of doing fuzzing it's doing symbolic execution so and that means like if you if you have Foundry it calls your tests with random inputs and then it just tries to find if there's some input combination uh that violates your assertions and in control we use formal verification or we use symbolic execution and that means we don't just try it on random valus we do it on on symbolic variables and that means that we really cover your entire input space

so if you have a u in 256 integer value that's 2 to the^ of 256 and if you want to fuss over all the values well that will take you more time that we have in the universe uh so but if you do it symbolically you can cover all these possibilities really every single possibility without any exceptions in a reasonable amount of time it will be slower than Foundry of course uh it sometimes can take you uh minutes or hours to run control on a proof um but then at the end you get a really uh on on a test sorry and then at the end you get a really strong correctness guarant uh because control will either find the counter example that breaks a code or it

will give you a proof that no such counter example can exist and that's really a machine checkable super precise rigerous mathematical proof um and or it will give you a stuck state which means hey I I'm not sure how to solve this and then uh H you need to write some lammer we call it so you need to guide the improver in the back end um to make more progress okay that's uh all I have for today thank you very much for attending this Workshop uh please follow me on Twitter uh follow my company and thank you