Using symbolic execution to increase smart contract security

and it's on so hi everyone we have two guest speakers today Andre will talk about symbolic execution and R about formal verification and uh we'll see how we apply these techniques or processes to increase smart contract security right because that's what we're interested in so uh then they will talk about uh tools that they work on for developers and auditors okay so um Andre when you're ready I actually think that uh rul do you want to start first okay which yeah I going to start um so I'm sharing my screen let me all know when you can see it all right can you see my presentation yes okay so welcome everybody um I'm ra from runtime verification and here with my colleague Andre um I'm working on symbolic this uh new tool which is kind of a hybrid between a symbolic execution engine and a solidity debugger and Andre is working on control which is uh well symbolic testing and formal verification tool but they are both built on the same underlying um engine so it makes sense to present them together and the order in which we go is I start first with a symbolic debugger because it's uh has uh it's more intuitive and then Andre will take over for the second half of this meeting and he will introduce like control and he will go into a bit more detail um than I do um so before I uh well I can tell you all day long how cool symbolic is but you can actually try and go convince yourself it's we have a free online version so you go to tce symbolic runtime verification.com or just follow this QR code and it will load a visual studio code instance in your browser with symbolic installed and you can just start debugging a function by just clicking this small debug button that we show both all um public and external functions um and will have a demo um uh also in in this uh in this session so it can be a bit you need some getting used to it but let's start with a little bit of background Theory and where this is all coming from um so I'm pretty sure you have not used a symbolic execution debugger before because well at this stage um symbolic execution D Burgers have been uh only the domain of academics and research papers but as far as I know there's no um there's no like industrial ready symbolic execution deburger and so symbolic is probably the first one and it's for solidity um on a very basic level it's the marriage between two techniques the first one is debugging um where you can just set break points inspect variables uh see what's on the call stack um and the second one is symbolic execution symbolic execution is a systematic way of exploring your program State um and digging into all the different like really all possible edge cases um and I will make this clearer um in this presentation so I assume that you are somewhat familiar with debugging but I don't assume that you have any prior knowledge to symbolic execution so we will start from first principles um and when you Google symbolic execution well you will find a lot of research papers because that's where it's coming from um and that can be scary and sometimes these papers are super hard to read um but what if you take one thing away from this presentation it is trust your intuition when it comes when it comes to symbolic execution because um you already are a skilled symbolic execution engine like really when you're reading code you're doing it symbolically um and here's one example that I laid out in front of you so we have this small program um that is checking if we have like if our balance is at least something and if not it will revert and if we have enough balance it will make a transfer so this could be this code snippet on the top left corner could be a snippet from a transfer function for example from an esc20 token so and when I ask you to um to read this code uh and tell me what this what you think this piece of code is doing what you do internally like mentally is you start symboling it execut uh sorry you start executing exec it symbolically in your head what that means is for example I tell you hey we have an initial State uh the value the from and the two variables um I'm not going to tell you what these are really what these values actually map to I just say hey this this could be anything and then I have some other variables like this balance off and um the from address like the initial balances of the users and I can say you hey these are concrete numbers so we start off we start with a initial balance of 100 for the sender and with an initial balance of 200 for the receiver so uh the lesson here is symbolic execution does not mean or does not imply that everything in your initial State needs to be symbolic you can have some symbolic variables and you can have some concrete values and mixing them is perfectly fine to do um so then I ask you well step over this uh from this initi State execute over this if statement and the first thing that you will note is well you cannot really know at this point um if this if condition is evaluating to true or to false and that is because well you don't have you do not have sufficient information I didn't never tell you what is the um concrete value of this value variable right so you need to consider both branches like you need to see what's going on in the then branch and your you need to um see what's going on in the El Branch so let's first look at the El Branch um and or let's start with the then branch that that's the logical order right so the left branch on on this slide um and when we enter this then Branch we gained some additional knowledge right because we know that the value must be bigger than 100 um we learned this from the if condition um um if this was not the case we would not be in this Branch so while we are symbolically exploring the branches we actually learn more about our state so and in this state um we have what we call an additional path condition or path constraint recorded that tells us hey value is um bigger than 100 and in this state um well in this then Branch there's only one statement left to execute that is a revert statement so we're going to revert uh and then we are done we are terminated so but now we still have to look at the other Branch right we still have to look at the else branch and again as soon as we enter the else Branch we learned some additional knowledge we now know that um well value is at most 100 again otherwise we would not be in this Branch so and then we can execute over the balance assignments um do the internal accounting um and what I did here like really really slowly um I bet like when you're reading this code on the top left corner you do this within some seconds like you your thought process is so well suited to symbolic execution you do it automatically within seconds um but for the purpose of this presentation I want to show you a little bit background Theory so I want to go to I wanted to do it once very slowly for you um so just trust your ination when it comes to symbolic execution so but um well let's motivate first why this is at all needed and um let me build kind of the motivation for uh symbolic execution and the symbolic debugger so you might have heard uh somebody say that the evm is a state machine and what that means is well we had some initial State uh back in 2015 the first ethereum the Genesis block was mined that is our initial state and then users users started um putting trans uh uh putting transactions on the network the network recorded these transaction and every transaction makes a state change right it takes the evm state from uh from a state before the transaction to a state after the transaction so for example if I'm going to uh send a transaction and transfer 100 usdt to Andre then before my balance would probably be 100 and after I transferred my balance would be zero and Andre's balance would have increased so that's the stat that um changes with every transaction so let's zoom out a little bit from One Singular transaction and laid out on the timeline so we have here two A's and on the xaxis you see uh well you see timelined out and on the y axis you see space let's start with time because that's simpler so in 2015 uh we had this initial State mind um then we C we we C it a bunch of transactions um and somehow we ended up in uh in the presents right and here we are uh we can look at the past and we see well we have recorded uh some million transactions for ethereum they all change the state and here we are with our Cent State and we know that some of these states in the past have been bad States and they have been exploited right and we can be sure that in the future like there will also be bad States and they are also going to be exploited and that's bad right from a security perspective um people are going to lose money and people lose their jobs so we need to kind of find all these bus in our future transactions now the problem is really it's even hard to do that for the past like if you look at some of the exploit transaction sequences these exploits they they are becoming more and more complex now imagine doing that for the future like where you cannot predict the next transaction so there's actually there's an infinite amount of possible uh next transaction that could come in it could be someone doing new P20 transfer it can be someone uh trading on unisub it could be someone um uh staking tokens we can't know and even if we could predict just the next transaction the game would repeat itself right and now we have an infinite possibility of next States and from there there's another infinite uh possibility of next States so that's what we call like the state space explosion problem and that's what we see on the vertical axis like the futur is branching out into uh into zillions of possible Futures and some of these possible Futures contains contain bugs and we need to somehow figure out where these bugs are now before we deploy our smart contracts and that's where symbolic execution comes in so how do we solve this problem um with symbolic uh so first of all what we do is well we try to collapse the possibilities the um the state space uh into abstract States so instead of um for example here on the on the top of the slide you have three concrete transactions um where Ellis transfers first 10 tokens to Bob or she transfers 20 tokens to Bob or Ellis transfers 30 tokens to herself and and all these different transactions they lead to different um post states that you can hear on the right hand side so in in the first state Alis has 19 tokens after the transaction in the second state Ellis has 80 tokens and so far so what we do in symbolic is instead of like considering all these possibilities individually where Alis uh tries to like transfer different amounts of tokens um we collapse them into an abstract transaction and Abstract here means that some of the parameters of your transaction uh can be uh like are not determined they are not fixed to concrete values for example here this abstract transaction the yellow one on the on the bottom of the slide um it has a fully symbolic Chrome address and a fully symbolic two address and even the value that we are going to transfer is not known um so so this is how we collapse space like from an infinite possibility of transactions into a single abstract transaction so that leaves us with a problem of time right um and and the problem with time is a little bit more nuanced um and I it's it's harder to diagram it but the cool thing here is like with these abstract transactions um we actually don't care about when our transaction is applied in the future and in which alternative future it is applied so again on this slide you have one concrete transaction in Gray and then you have one abstract transaction in yellow and you can see um like the in the starting state of the initial trans of the concrete transaction at the top where Ellis has a balance of 80 and Bob has a balance of 20 that this state is subsumed into the abstract State below it the the yellow state right um so if we assign uh dollar from to Alis dollar two to Bob dollar X to 80 and dollar y to Bob um then we arrive at this uh at this concrete state so that is what means what we mean by the abstract state is more General um or um yeah is more General than the concrete state so and now the trick here is that we play well you can also see that the final state of the transaction where Ellis has a balance of 60 and Bob has a balance of 40 that's also sub subsumed in the initial state of the abstract transaction if you follow this Arrow um this dotted Arrow at the uh at the right that goes from the gray box to The Orange Box um and then follow this error again that goes from the final orange state to the initial orange State you can see by transitivity we we call that property transitivity but that's but for forget how it's called but by just following the errors you can see that uh the final state is also subsumed in our initial State and that means that we can uh apply this abstract transaction to any alternative timeline in the future um and if this is to um to abstract I'm uh well I have one more abstract diagram on this and then we are going to uh to to go into the demo so uh ultimately that means what we did is so we started with this problem where you have infinite amount of possibilities alternative timelines some of them are buggy and we must find the bug so what we did is we reduced this problem to what a simple problem that is just we have one abstract transaction that we need to consider and we need to see hey is there any execution path in this abstract transaction that could be buggy um and notice I'm saying well this problem is maybe simpler uh than exploring an infinite amount of possibilities but it's definitely not easy to do um it's it still takes some skill um so but that's where our tool comes in and hopefully it makes debugging these abstract transactions easier for everyone okay I'm going to uh skip this slide because uh think we don't have the time I also wanted to do the demo um this is a sneak peek I think I can also skip this slide because well you will see it live in action so I don't need to talk about in a screen here um time trouble debugging is a nice thing so I talked I talked a lot about like time and space and well when you are dealing with alternative timelines and that is what symbolic execution actually does it considers all Poss all possible futures um then it can well it you can get lost like if you have watched a time traveling movie uh it's it's easy to lose uh the red threat right right and lose orientation the same is true for um debugging symbolic transactions so therefore we have this nice time travel debugging feature where you can actually instead of just stepping over one statement at a time you can also go back like step backwards in time and even better um you can also jump to directly jump to Alternative timelines so that's why on this slide you have this graph on on the right um that basically visualizes all the possible timelines and you can just select one note to jump to this specific point in time in this specific timeline um okay let me uh I think it's it's demo time so let's use this demo that you can also access on your browser um go to T symbolic runtime verification .c so you can play along you can also do that after our call um so this demo is very limited in scope it uh you cannot um upload your own source code there uh you can only debug the wrapped e contract so wrapped e for those who don't know it's a famous contract that ws the native cryptocurrency of ethereum which is called eth into an ESC 20 Tok and esc20 is the standard that is used for um for all the non-native currencies or tokens whatever um of of uh of a blockchain so you have this contract and you have some you have all the classical functions that you would expect from an esc20 you have a pro transfer transfer form um deposit and maybe let's just start with with a simple function that's also kind of interesting so I want to start with the um let's start with a withdraw function so and in order to start debugging it symbolically all I have to do is click this debug button um and then it's automatically stops at the first line so and notice I click this debug button but I never specified um what is the value that I want to transfer uh to to withdraw I left that open and symbolic execution means that we just tweet this parameter as an open variable that could be anything so we assign it to a symbolic value and you can actually see that in the call data of our um of our post state so um if you're familiar with how the uh function dispatching of a smart contract in solidity works so you have this call data where the first four bytes are basically the name of the function that you want to call so uh these four first four bytes you can see them I don't know can you see my mouse by the way I'm pointing here yeah we can see it on the selector right on the selector right so this is the function selector it's a four bytes uh well cryptic hash it's just the internal name of the withdraw function really and then you can see that there's something else in the call data and this something else is the symbolic value that we assigned to this um wad variable to this vet variable so you can see well this is a this is a solidity variable and this here um in the call data that's a symbolic variable and we can see it has an integer type um so let's execute uh let's execute over this requir statements and well let's first try to think what could happen when we execute over this required statement well we don't know what is the balance of the message sender because uh the storage of the contract is also fully symbolic and we don't know um what is the vet value so I'd expect that there are two possible code paths right that we must consider one where the re Clause um evaluates to two and one where it evaluates to false so let's see what happens and I want that you pay your attention on this call stack and what happens in this bottom left corner of the screen so going to execute over the statement and you can see that my control flow branched into two different branches so these are my two alternative timelines my two alternative futures um you can see that that one of these uh the bottom one branch three is an exception so that is the branch that reverts and you can see that it's stuck in line 41 and the other Branch actually jumped to line 42 so the other Branch the branch two is the one that passes the required Clause so I'm going to um when I ex try to execute this uh stuck uh this reverting state it will just disappear from my call stack so I'm going to do that and this this just leaves leaves us with the with the other branch on the C stack so now we are looking at Branch two the other branches uh just disappeared and like I said when we are um executing over if statements we are learning additional information about our execution and the same is true when we execute over over require Clause right now we know that this condition must be satisfied or otherwise we would not be here um in this state so and I can inspect all my path conditions like everything that I have learned about my execution I can inspect it in this um path conditions view here in the left uh in the top left corner so I'm going to expand this and you can see that we all that we already collected a bunch of knowledge um and most of these is just coming from the types so I can for example I can see hey I have this symbolic uh variable which is a message sender and the message sender is of course an address um internally it's but it internally it's encoded as an integer um so but I know that this integer must be at least zero there are no negative addresses right and then there's another um there's another constraint here about the message sender that tells me message sender is at most this cryptic value and I think this is the max value of uh 20 bytes unsigned integer because addresses I think are at most 20 bytes long um so this is just 20 bytes set to all once um and there are other con TRS here that are also coming from the type so let us see what we know about this vet variable um you can see it here in constraint number six they are numbered um I can see well this vet variable is also an unide integer so it must be at least zero and what else do I know uh here's the max value of this V variable it's at most well two to the power of 256 minus one um and if you look at the bottom like the last constraint you can also see this more complex constraint um that is telling me that the vet variable is at MO is less than or equal to the balance of the message sender so this is the information that we just learned by executing over the statement um let me see if I can uh I can make this visible I know it's like the user interface is not optimal at the moment so you can see that these symbolic Expressions that you can see here in the path constraints they can grow really big and then they run out of the screen and you need to scroll um so we are working on like giving them a nicer syntax and making making them more a can looking make them look more like solidity Expressions um but at the moment that's what we have but may I ask a question please yeah of course please okay so about these pet conditions so um like um these are probably generated by the tool right all the pad conditions if I'm right yes these are collected by our symbolic like our backbone here the symbolic execution engine that's running under the hood that's called KVM and and KVM is really executing over each single it's working at the bite code level so it's working it's executing each bite code instruction in a symbolic State and while it does that it collects all these path conditions okay pretty nice so if I'm not using your tool I suppose I should write it by myself like all the pet conditions is the right way absolutely that's how yeah oh my God actually that's how I How We Invented this tool like we had our Auditors um well at one time reification we we do aits and formal verification and we had them like collecting um all these path Conrads manually so I did this personally with pen and paper actually I printed out the source code literally I printed out source code and um I took a pen and at every possible execution path I uh wrote down the possible path conditions that could lead me bring me to this state um and that's what I figured was like a dump part of auditing um but it's a necessary part because you want to dig into all the possible edge cases bus are often not on the happy past bus are often on the edge cases so you wanted to like to just to convince yourself to get a to increase your confidence confidence that your analysis your security assessment of the token that you're are going to evaluate um is doing is well something worth um you need to look into all the path constraints and you need to book keep them somewhere so I did this in pen and paper I found this annoying uml and I think that's how we started inventing this tool is like hey can we automate this to some degree can we not just have a tool record all these path conditions for us and point us like list list out all the possible ranches give us all the path constraints that lead to these states um yeah but I think if you're not if you're not uh wanting to use a formal methods tool if you just want to do manual audits that's still a good practice to do it's better to have these path constraints written down somewhere even on pen and paper uh they're not doing it at all or like believing that you can keep them all in your head so okay so I'm just I'm it's funny for me because I'm thinking that for example for the withraw function if you would like to write unit test actually you are testing like it's an address on new in and things like this that uh when you are looking at the code it's not something like logical to test like it's of course like this but I I assume this is not like on real testing like testing all the pets I assume the pets like I I assume these pets are right on on normal testing yeah on normal testing well there's different techniques how you can make sure um that you increase your test coverage right um so yeah but even with test coverage I don't test things like like the message sender like on the pad conditions here so I don't test the message sender it's an address or you me yeah um well the your tests are only as good as your specification the same is too but the same is true for uh formal verification and for uh well all security assessment techniques basically uh yeah but the thing is well symbolic or symbolic execution in general can point you to all the edge cases really and then when you step through through your code like we do here we might notice a case that we H do not have a test case for right so if I'm executing uh my withdraw function I know my test suite and I'm suddenly ending up in a branch and then I'm like whoa I didn't think of this case before um we don't have a test case for that but we probably should so actually it's a symbolic execution is also like a good guide uh when it comes to um increasing your test coverage and inventing new test cases okay thank you here I think I can also make one additional comment so the idea is that our symbolic execution engine is not limited to the data types that are used in evm sematics so for example wherever you see that uh lower than int or equal equal int that is the integer sort whereas the evm works with uh uh int that goes only as big as 32 bytes so we actually have to constraint these variables to say that okay this has to be an evm word so we have to limit it to be less than 32 bytes so yeah a lot of these constraints are just limiting the uh range of the variables so you've you've created a tool that it's not only for solidity but you like made for solidity so yeah and this can go very well into a rabbit fold so the symbolic execution engine that we have is based on this K framework language in which in a few words you can Define how a programming language works and then this uh K framework uh is able to generate you a lot of tools for um your programming language that you defined and what we did here is that we defined how evm sematics works and um the key framework enabled as the symbolic execution but I'll let U I'll continue from here I think okay thank you for explanation yeah and I have uh yeah you are basically predicting my next slides um so but let me just wrap up the demo real quick um so we can um see the path conditions see there's a lot lot of path conditions that we collected um let me see what happens if I execute over this function um seems that it's not branching on this statement uh which is kind of expected because well there could be an underflow here but we just checked against this condition so this underflow is actually not possible um so we are not we don't we don't need to branch in this situation we can just assume that we are on the happy pass um yeah other features uh what try it on your own I just want to give you some like idea of how this tool works but one really essential feature um especially if you are a security-- minded person or if you are dealing with a lowlevel code um if you are gas Optimizer um then this debugger also has a mode to uh work work on the bite code level so I can actually here open the disassembly view um which loads the bite code and you can see on in the white column here you can see the disassembled bite code you can see the next operation that I'm going to execute is a caller operation so I'm executing over that um and here's a stop operation so we are going to RT now um yeah so this uh this assembly view this is more for the expert users uh but internally we find it like super helpful also to understand what is the solidity compiler doing what is it like how does the code um look like that the solidity compiler generates uh and it's far from given that the solidity compiler has no box in it right so um if you want to secure protocol and you don't trust that the compiler does everything correctly then you also want to look at the bite code at least in in like on the most critical code paths maybe okay but um again go to this try symbolic runtime verification.com demo convince yourself try it out shoot me your feedback feature ideas um so I'm going to go back to the presentation um and yeah you just asked about uh what is this uh like does symbolic only work for uh solidity or does it work for other programming languages and uh uh I didn't expect this question but uh you really predicted my slide here so uh let's talk a little bit about how symbolic and control the tool that Andre will present uh in a minute um and how they fit into our runtime verific tool Suite so at onetime verification we have like lot lots of tools uh that are for other programming languages but at the core they are built around a really really elegant and really tiny mathematical logic that is called matching logic and I I think it only has a handful of proof rules so that's a really tiny mathematical core and everything else that we build at onetime verification is buil around that small mathematical core so that is basically our trust base um so around this matching logic core we have this what we call the K framework K framework is a well is a programming language for Designing and building tools for programming languages uh so you can build tools uh on on top of K for solidity and KVM you can but you can also use it to build a semantics for C uh or for w and kind of develop the same tooling um as as we done here with symbolic and control so symbolic and control are just two specific instances uh of how you could use the K framework um okay I think um yeah I want to give everybody the chance to to ask uh one or two questions maybe we have time for that and then I will hand over to my colleague Andre who's talking a little bit about control and takes this entire concept one step further um yeah I have a question can you hear me yeah yeah your microphone quality is not that good but H just give me a question uh yeah I saw this cool visual graph the presentation uh is it available in the uh demo oh that's a good question and uh the answer is a qualified no um uh we had to like last minute we had to disable it before we released this online demo just because it was not stable enough um but we are stabilizing it now in the background um so it will land there it will land in the online demo soon I cannot say you in exact date um but it is definitely still on a road map and it's one of the highest priority items to get this uh nice visualization graph uh into the demo into the tool in general um so also yeah speaking of updates um you want to like when we push out this graph for example um I will make some noise on Twitter um so yeah go to our website try our tool we also have a um we are currently hosting a closed beta version um that works a little bit differently that is a instead of working on top of control it works on top of Foundry so if you have a Foundry project and want to try a debug on it um you can sign up for a closed better vers at the moment um yeah and then follow us on Twitter uh shoot me your ideas shoot me your feedback uh shoot me your questions and yeah thanks for having me I'm going to stop screen sharing so that Andre can take over I've I've got disconnected I had one more questions if it's possible yeah of course okay so it's just a fast question question you say that on that circles diagram you say that um if I'm correct you are you starting for mathematical assumptions right so I'm curious that it happened for you like to have a mathematical wrong assumption about like your core um your core product that happened to to go wrong to maybe me many layers um so not on this um well not on this mathematical core at least well not that I'm aware of I'm also like this matching logic um has been developed like in in Academia for over 20 years I think and uh there's uh if you're um if you're are into mathematics um we have some strong um theorems that shows um that matching logic is as expressible as um calculus of constructive what's called calculus of constructive constructions for example so what's underlying um Theory improvers such as and actor um so we have all these uh strong mathematical theorems connecting it to other um mathematical logics um but we had um like sometimes for example uh if you have a programming language semantics um you add new assumptions um to your core calculus uh you add new aums basically and we had the cases where these aums were unsound so they should not have been added to the code base um luckily all like these mistakes uh they were just like they did not lead to any missed bucks or so um uh in our analysis and we were able to identify them um yeah but if you are not doing things carefully and if you're adding aums to your mathematical core Theory um uh then yeah you could end up in an inconsistent Theory and prove basically anything about your programs even even if that is not true um but unfortunately it never happened in this uh uh uh the impact was never that big okay thank for can can I ask a question yeah sure yeah in in the demo it is a number comparision it is bigger it is less but if it is something more complex not assume I mean something logarithmic or whatever it is translated to op codes and the op code it is finally also a branch I I don't know if I did yeah yeah you made this clear um yeah so I mean all these path conditions that you see here um they are ultimately they are coming from the evm bite code right they are not coming from the solidity source code level because that's just how our execution engine works it works um uh it works on uh well it works on the bite code level so that's why these these um formulas look so complicated and to be honest they don't even come from just the evm a lowlevel evm but they come from a formal model of the evm which we call KVM so The Logical formulas that you're looking here at um they are K terms or k Expressions uh and K expressions are really just these matching logic um Expressions that I talked about earlier and they can be arbitrarily complex so as I said they can be um well they are at least as expressible as the calculus of constructive constructive constructions I don't know what the name but yeah so these logic just to make it short these logical formulas here um they can become really uh big they can be they can be complex they can have logarithms in them um yeah basically everything that you wish to express uh in in everything that you wish to express in some mathematical uh way could end up in in these path conditions and if in a language there is some random function ER the branch uh was the same uh well we for for evm um we are lucky and we know that uh there is no random function that you can Implement in evm right it's it's a deterministic programming language um but well we also have uh a semantics for example for C and C is not a um deterministic programming languages there's all kinds of undef unspecified Behavior or under specified Behavior you can have random functions um but we have a c semantic that's quite complete and so this approach also works on the sea level um yeah so we don't have um we don't hit a theoretical boundary um yet when it comes to like nondeterministic behaviors as random functions for example okay thanks okay um sorry I'm taking time away here from Andre um but yeah please feel free to shoot me your questions um offline um or maybe we have some like if you want to stay longer um after the 90 minutes of this conversation um I would I will hang around a bit to answer all your questions but I want to give Andre now the chance to uh do his part of the presentation thanks uh yeah thank you so uh yeah I'll share my screen in a second um um okay can anybody can everybody see my screen yes okay cool thank you so yeah before I dive into the presentation i' like to talk a bit and say a few words about formal verification so uh formal verification it's not this Golden Goose of security so it's not like hey I've done formal verification now my contract is unbreakable and has no security vulnerabilities uh that's not the case uh formal verification mainly consists in writing a specification uh of what your contract should do and then proving that your contract behaves according to that specification so of course your formal verification will only be as good as you write your U your specifications and at runtime verification we use the symbolic execution to uh prove that a bite code of a solidity program behaves according to a specification that is defined um starting from the symbol solidity test that I'll be showing later in the presentation um so with that in mind um I'll be talking about uh control which is basically the tool that we've been developing at runtime verification and we've been using it for engagements um for the last year and it basically it's basically made out of two components one is the KVM which rul already introduced and it's this uh formal semantics of the evm uh machine the evm op codes and how they work and this uh KVM implementation um being imp being implemented in K this means that we can use uh the symbolic execution engine now this uh semantics of evm this KVM can also be used as uh node so we could modify it to basically connect it to a node like G for example um it also runs on um all the uh tests that the ethereum foundation provides and um it passes them um and yeah it has been developed from 2016 so uh it has some time now um and um yeah we have this Evan matics and then on the other way around we have the uh Foundry framework which gained a lot of traction in the last year and it's a popular framework for solidity developers that uh um it's a bit similar to how hard hat and before that the ganash and truffle worked one additional up upgrade is that developers can now write their unit tests in uh solidity directly so they don't need to use typescript or JavaScript and one additional step is that these unit tests can now be fuzzed um and so having um I'll talk a bit about the project structure and then show some examples of both Foundry and control um so yeah the project structure is similar because when we developed control we wanted um to have we wanted developers to have a better experience so without to avoid creating multiple projects of basically the same source code and avoid duplication and so the project structure is um I I think it's a bit intuitive so it has this Source folder where developers write their smart contracts and then it has the test folder where the uh tests are written the contracts containing the tests are written and then you have the another important folder is the lib folder which contains additional libraries required and there are two highlighted libraries that I'll talk about shortly and then there's the outfall in which the solidity compiler uh puts all the artifacts of the contracts like the ABI and the abstract syntax tree and all of that uh the idea is that we use the uh these artifacts these Json files to create the specifications for uh the contracts that users write um but yeah the idea is that the uh test a test in so has um looks like this and this is again the wrapped ether contract that rul was uh presenting in the symbolic demo but basically how it works is that we Define a new contract uh that basically is a wrapper over the initial contract so uh we have an address or um reference to the initial contract that we want to test and all of these uh uh test Frameworks have this setup function which is basically the first step before you want to execute a test you run the setup function and then you make some kind of snapshot and then on top of that snapshot you can execute each test that you have in your in your test contract so in this example we would initialize the contract and then we would generate two addresses and then whenever we want to execute a further test these Alis and Bob and the address of the asset Raper contract will be the ones generated in the setup function um and um oh yeah the libraries I almost forgot that so uh I told that there are two additional libraries the forge standard library and the control cheat code Library the idea is that in order to manipulate the evm solidity uh the solidity language uh it's a bit restricted so you can't set the message sender or you can't set how much ether does an account have initially so for these scenarios uh Foundry developed or before that hvm I think they develop these cheat codes which are basically a contract of functions that don't have any implementation these are abstract functions but when you make a call U to a certain add address with a specific call data which is the hash function of this cheat code then the evm the evm implementation of this framework will have a specific Handler for that function so in this test approv Alice to Bob example we see this vm. prank of Alys and what's happening here is that we're um mention in to the uh virtual machine that's running running underneath that we want the uh message sender to be set to this Al specific address that's generated in the setup function um so yeah there are a lot of cheat codes that are defined uh they are public online um control also uh supports I think most of them or at least the most common ones uh that found uses are used as well as control and on top of that control also have some specific cheat codes for symbolic execution um okay so I think I covered this slide um I think I can jump to the uh I can jump to the terminal to see if I can run some tests actually uh okay not this one let's use the visual studio code so we have this secum uh secum control repository that I'll share at the end of the talk let me actually turn on the lights um so I think in the let me increase the font as well so in the WRA ether uh I think I'll focus on this uh test deposit function for now um or actually I think I'll use this test approve Alice to Bob because it was also in the slide so um yeah the idea is that you can basically Forge build everything to compile the source files and uh cool then you can run a specific test which is I'll use this one and uh I can do Forge test Das Dash match a specific test and I can paste the test that I'm trying to execute and um yeah I run it and I can see that the test passes and additionally I can see that it had 256 runs now what does this mean is that the fuzz framework underneath Foundry was able to generate 200 56 different inputs for this amount variable which is uh um which is an argument to the test now if you want to write plain uh if you want to write plane unit test then oops uh then you can just avoid having an argument to the function and now the function is just a plain unit test and you can Define the u56 amount here to have a certain value um yeah regardless of that but um yeah this fuzzing also has um some limitations and um I'll use another example here this is an example that we have in the documentation as well so um I don't know for example this is a very basic contract that has only a u field and it has an error defined and um two functions implemented and the set number function would basically take a number and the Boolean flag for some reason and um we'll assign the number but if that number has a special value which I'll call coffee and it the Boolean argument has a certain condition then I want to revert so this is used to show that basically um how complexity affects fasing uh and the idea is that if now I want to run this Forge test um Match test and I'll jump ahead so um in a similar way I have a test contract defined for this and I have a test set number which basically takes two arguments that have to be fuzzed and then I can pass them to the contract function and then they'll be asserted and so I can just do to match test of test set number and it tells me that the test has passed it again tries to run it for 256 times and then it doesn't find any issue with the function that's happening here now I can increase the fast test so let's see let's put the flag saying that I want to run this for a thousand times and again it tells me that it passes eventually if I increase this around 10,000 times at some point it perhaps will find the issue so okay now it found the bth condition or the random value that's supposed to uh get on this revert Branch but the idea is that the more complex your function or your logic is the harder it is for a fer to identify that scenario um [Music] so yeah that's what I wanted to show on Foundry uh again if there are questions at any point please interrupt me or um put them in the channel um okay so yeah now uh this was Foundry the idea with control is that as R talked about symbolic execution we can take now this Foundry framework that is here and we can take the symbolic execution engine and we can combine them together and what we end up getting is that we can get symbolic exploration and we can get symbolic testing which I'll explain again the difference between the two so what rul demo in the contract I think he debugged the withdraw function which uh basically was a function of a contract so it was not a test in that that case it was the symbolic exploration happening where over the arguments of a function um basically those arguments became symbolic and then we started executing the uh contract code uh now the difference between symbolically executing a function and symbolically executing a test from these Frameworks is that uh a test also has a few additional criterias so at the end we want the uh we want the function execution to to not revert and we don't want any assertions to happen we don't want any assertions to fail and there are these criterias that basically uh Define how a test should pass um and I think the difference here is that if you prepend the test prove or check words before the name of the function then is is going to be considered a test and then if you if your function doesn't have that then it's going to be considered a symbolic exp exploration case um and yeah we have some additional special cases like Constructors and setups but uh I won't go into that um so um in in program verification and informal methods there's this concept of four triples and we try try to adapt that and with this uh way of writing tests uh I think we can apply them in uh solidity testing as well so basically a H Triple it's something that says that um for any kind of um for any variable I have a set of preconditions I have a code and I have a post condition and what this means is that for any possible input I have some preconditions that hold at the beginning of the execution of the code and then I have to execute the code and after that the post conditions should hold and so we can take this concept and apply it into this uh structure of solidity test and basically we can use the uh assume cheat code or the assume function to set a pre conditions for a test and then we can have the code to be executed and then we can assert post condition uh now vm.

assume is basically another special cheat code used by Foundry and control uh it it's basically used to to um filter variables or you can you can put that you can put a Boolean in this assumption like I want this address uh field whatever to be different than a specific address and then what happens underneath is that this becomes a path condition uh was the question H the guy got straight picture of the which guy you're not aware bab no I'm in a meeting go ahead Andre uh yeah sure someone unmuted um okay sure so yeah I was saying about these uh precondition and post conditions and how they how uh they can be applied in um symbolic test in solity testing and the I think the idea here is that there's the concept of the the weakest precondition and the strongest post condition so in general preconditions the idea is to have them as general as possible so start from a state where you only know the uh minimum things that you need for the execution to happen and then the post condition needs to be stronger so that uh you can have uh higher uh you can have a higher confidence in your correctness uh and there's also something I'll that's in between the preconditions and the post conditions which is called invariance and I'll uh touch those shortly um so yeah now about control uh s uh I I told earlier that it's similar to Foundry and then it's basically uh this is a list of the initial commands that you can use uh you have the control build which basically uh runs the same as runs the same as Forge build and it compiles the solidity code and then it generates the specifications for each contract and each test um using this evm KVM framework and then you have control proof which can take an argument of the test you want to test um and what proof will happen is that um when you run control proof you will actually execute the specification with uh symbolic execution and I think I can go back to the terminal here so uh yeah in the interest of time I ran some proofs before the meeting just save time so the First Command that I can show you is the control list which basically lists all the available all the proofs that have been executed in your project so um yeah in this example I wanted to run this uh test deposit function and I also wanted to run this test set number that I've been showing earlier with the coffee break and so you can see that I have a proof for the setup function of that contract test test and I also have a setup function for um a setup function sorry a setup function for the uh Raper contract and then I have two other proofs for the test that I wanted to run and uh surprisingly in the interest of the meeting both tests have the proof status of failed but the setup functions uh passed correctly so um just to show how the process would do I I could do Control Pro Das Das uh Match test and you can either put the full name of the function or you can do partial matching and uh here I'll just do partial matching so I think I can do this um test set number and now it will take some time to spin up the internal servers and everything that's needed but should take a few uh perhaps 30 seconds or not or less um and the idea is that while this is running um um I was uh sorry I was saying that what happens here is that underneath control is able to run this uh K CFG or control basically control flow graph of how the execution develops uh with this symbolic execution engine and um it will will generate nodes in this control flow graph and each node it's uh compared with a Target node which we Define of how the post condition should the post State should look like um and uh okay so what happens here is that we see some um not so easy to read uh messages and these are actually the failure reasons or the path constraint that led us to the failure but the idea is that um we can see here the path condition of which our execution failed uh and basically what's saying here is that whenever X is equal to a certain number because here I have a double negation but uh and whenever uh the inlock symbolic variable is different than zero then I'll lead to a Noe that fails and in addition to this I get a model which basically says uh instantiates all the symbolic variables that we have in the test they get initialized instantiated with a concrete value and I suppose this uh this number here is the hex coffee number that I was showing u in the test and so one additional step that that I can do here is that I can do control show on the test set number and one second it will display this control flow graph in the terminal and uh I'll try to go through it and uh yeah the idea is that as I said we have these nodes of the kfg which which represent various snapshots that were taken during the um execution of the test so this number of steps is representing that okay before the two nodes happened there were 1,256 operations that happened and uh I won't go you can ignore this code for now I know it's not readable but what's interesting is that at some point I see that there is a split on a jump eye up code and then I see a branch happening and I see this constraint saying that okay whenever X is not equal to this number the execution continues and this is added to the path constraints that R was showing earlier and so if I go down this path I see that at some point I end up with an evmc success status code and I see that um the terminal node is basically subsumed into the Target that we were trying to achieve and then we have the second Branch when uh X is equal to the number and then it will do some processing and again it will reach another branching point because what happens here is that I have an end in the if condition and so at the biteco level somehow this gets split into two if conditions one after the other uh so then I here again I have the second Branch constraint based on the Boolean argument that I had and so on One path again I see the uh ICD vmc success and that it gets into the target node and then again on the last Branch I see that I have the evmc revert status code meaning that the execution failed here and now if this doesn't have um if this is not if you still want more information about this then you can you could use the control view kfg option um which again would take the test and uh this would display um uh CLI implementation of um kfg viewer so here now you can actually explore or the control flow graph and I know I can maybe put this down uh so basically now you can browse the control flow graph and then at each node you can basically inspect the state of the evm at that point and here on the right hand side um I would have the options that I have available I have the uh some basic information like the test name uh the status of the proof and the time it took so for this it took a bit over uh two minutes and uh then I have three more um cells so I have the one on the bottom right which this is the source code and basically using Source Maps it theoretically could Point um wherever you are in the node to the specific function that you're in but this uh is not always working correctly because uh the solity compiler does a lot of optimizations so usually the source maps are not very accurate uh so for now I'll just uh disable it and then I have two more items one is the one sh showing the path constraints that I have available at this point and then the other one is for the configuration and this is basically a snapshot of how the evm machine the evm state is at this point in time I see that I have for examp example I have the program bite code here that's loaded into the evm I have all the jump destinations that are available I have the address that's currently loaded and I have the call Value and uh the local memory and so everything is defined here to uh be available now again this is not I know it's not very easy to read so um yeah um okay now I'll also run the second uh the that's deposit proof and uh while this is running I think I can uh no I think I'll continue a bit with the test sorry so yeah again it takes some time to basically read the proof information and use the if it identifies a failure and then it basically calls to a um smt solver like Z3 to basically generate input for those uh failing constraints and it basically takes time to generate that model at the end with the concrete um values um or perhaps I I forgot to run this proof entirely and it runs for the first time now which is also very uh possible output and seems to be the case no okay so yeah in this test I think I can put it side to side uh o I'm not good with these okay so in the r ether contract here I think I can look I can close this we have this test deposit function which basically takes an address as an argument and then uh we have an auxiliary function called not built-in address and this is something that we use to trim branches that we don't necessarily we are not necessarily interested in because um when you have a symbolic address at some point is going to assume that um it's going to compare that address with all the addresses that you have available in the State uh So to avoid uh re-executing or executing multiple times the same code paths but with a different address uh constraint uh we just assume that um the symbolic variable is different than the subset of addresses and then we set the message sender to be equal to this symbolic address and then we want to deposit a value that's the message value um and uh yeah running this function you can see on the right hand side that the proof is failing at at some point we have this path condition saying that the proof is failing when the call Value is uh greater than zero and um I can go oh not in this one so yeah we can see that at some point he's doing a check balance so underflow on the from address and then there's a branching on the call value of the function on the of the payload that we're making and so if at any note I look into the let me close again these ones if at any point I go in the account State uh uh this is the account State and this is how accounts are represented we have the address the balance the code and so on so at some point we're going to see this account that's here with the symbolic from address and we can see that the balance is zero and why the test is failing is that whenever we're making this um whenever we're making this uh deposit function if the call if the message value is higher than zero then the test would fail because we don't have the balance to do it so um what we can do here is that we can do vm. deal um to the from address uh we could deal let's say 10 ether but uh I'll ask this is like an open question what do you think it will happen in this case say that I recompile the proof and then I run again um any suggestions or any idea um okay then I guess we can do control build and we can also do control build Dash Dash recompile and then we can do Match test there the POS it D Dash rain it and what basically here is that I've changed the solidity code please recompile everything and then I'm proving with the Das D rein it meaning that I want to start a new proof instead of continuing the initial one but while this is running I think I'll go back to the slides um as I said I'll be all over the place so uh yeah the idea is with symbolic execution is that uh it gets a bit complicated when um Loops are involved uh because the idea is that Loops are kind of like treated like black boxes you don't know at which point in Loop you are you don't know if you're at the start of the loop and you don't really know if you are like at the end of the loop uh and so it's a bit complicated when you want to do symbolic execution on Loops now there are I think there are two main ways to handle this um and also as a side note uh I can tell you that here this function has more than one Loop so um I don't know if you can see the second one but we're also discussing about that one um yeah so the idea is that um there are two ways in which symbolic execution can handle Loops the first of it is that you can do um bounding so most simp symbolic execution engines would like identify a loop and then do it for number of iterations like three or four or 10 times and then it will automatically jump out of the execution and this is possible because in the bite code you can identify where a loop head is both by how the loop head looks like and both of like um the program counter that gets repeated over time and so you can basically bound the loop by executing it a finite amount of times but then if you run a loop for 10 times you still you're still not certain that the problem won't be at the 11th time of execution the of executing the loop so the other approach is with something that's called an invariant and basically invariants are these properties that have to be valid at any point in the execution of time um and so this function uh I haven't tried to execute it uh and I'll show some overly simplified uh invariants um just to develop your intuition and show and show you how these invariants uh are supposed to look like but uh in reality whenever we have to work with invariant they are very brutal and uh whatever change we make to the source code we have to uh modify the invariant and update them again so uh this is a Sol function that I wrote that basically takes an array and uh it Returns the minimum uh the minimal value of the array and so uh if you would want to write invariance for these functions basically when you have invariance you need to show that the code you want to execute has a termination and you also want to show the partial correctness of the code basically again you have to specify what what the function should do and then you have to prove it so to show the termination of the code I basically drafted an invariant here that says that um at any point of the execution of the loop of the for Loop the I iterator has to be between zero and the length of the array that we have so this will be valid before the loop during the loop and even after the loop and so um the second invariant that we need to show the partial correctness of the code we have the second one here that basically says uh we take a j another iterator and uh which is of type int and for all values of J that are between zero and the iterator I well I need to know that the the mean variable that we're having defined here is less than equal to a of J so this means that again at any point in the loop the mean variable will have the uh lowest element that we can find in an array from the start to the point where currently at um so yeah this is basically how um you can Define or what the intuition behind invariance um and yeah using this and using the hard triples basically you can do program verification in mostly any kind of language not even not really not only evm um and yeah I I said earlier that there are two Loops here one is visible but one is kind of hidden and the other one that used to make us trouble is the use of the dynamic types as arguments so uh a dynamic type doesn't have a fixed number of elements you could basically uh it's not known at compile time so when you're compiling a function like this the Sol compiler will actually generate a loop that copies values from the call data to the local memory and the other way around so we also needed to figure out a way of how we can handle these because there are other symbolic execution tools out there we're not the only one but most of them will or at least some of them will fail when um you want to run it on a function that has Dynamic types and so uh one way we um we handle this is that we use the same Concepts but uh we choose to bound the dynamic types that we're having so um saying that we have have a function that has a u into 56 and then has a dynamic type of uh an array a dynamic type of array uh and the array holds bytes Elements which again are another Dynamic type so it's basically an array of arrays um in situations like this we want to bound the length of an array and the light the length of an element inside the array so uh we use this using a concept called npec commments um and basically the compiler allows you to use uh special tags in the comments and then uh you can see in the compile Json you can see that um you can read those values and that's how we extract this from the Sol source code and the idea is that we can basically use a certain tag like control array length equals and says that okay I want the data to have three elements comms and I can also say control byte length equals to data which means that um each bite uh each bytes element inside the data byte array I want it to be have 200 bytes and so uh we can restrict the length of the elements and the L of the array but the value can be anything in that boundary basically um and uh yeah I think this is what I had prepare for today um I also think that maybe it was a bit too much um I can go again into the execution of the code and I can see that the path condition the proof that we wanted to modify failed again and basically because the C value now the branching is not over zero but it's a about uh that 10 ether that I used as the initial balance so the gold value is now whatever what happens if the call Value that I want to send is 10 ether plus one the initial unit that we have um so going back to the code and I'll I promise I'll finish with this how you would uh work around this you can say that okay I want to deal to from um whatever the message dot value is that we're trying to send and so at this point um whenever it goes to that comparison between the call value and the um balance of the from address um is going to be the same value so it won't be a branching so yeah um any questions yeah so uh Andre about the invariance you didn't show in the example uh the emance that you showed in the slide so so do do you have some assume statements or how do you um uh okay so this is not code that actually runs uh I wish and I think everyone wish that we can write in variance this like as easy at as and as read at as these ones but in reality evm invariants are way harder to write because you basically have to reason about the entire configuration that I showed in that terminal so you have to reason about uh gas you have to reason about how local memory works and all the program counters that are used and so uh you can get to a point where you have an invariant that does the job but then you want to modify something like even the tiniest bit of change you do in the Sol code it will generate a different bite code and then the invariant won't hold anymore because the program counters have changed for example uh so yeah I don't think I have an example of an invariant um I think we have um two block posts in the making that will be pushed out pretty soon that contains a full walkth through of how you would specify an invariant like how would you come even even come up with an invariant like at the solidity level at the natural language level then at the solidity level translate it to the evm level and then actually how to apply it um in your proof uh that's a bit of a tedious process uh but it's the only way we have if we don't want to fall back to um to cutting off reachable states by using Loop uh by using Loop unrolling and bounding um yeah just just uh stay tuned for this for these blog posts they they contain a full walkthrough of this thanks uh yeah also all the materials that I've shown previously um I think I can also share this the slides uh here um we have the security control repository where we have these proof examples then you can you can try with then we have uh an entry blog on control we have the control documentation and the open source implementation of our tools that we're using and also the link to the symbolic and then we also have a an pretty active community on Discord with this QR code so you can join our Discord then you can always post any kind of questions that you have on either symbolic execution or developing or how we um how to use control basically great if uh if uh you the slides are sharable and they public so you can just drop the link in into the com into the chat I'll take it and put it on the metup page H sure let me see how to sh so uh any other questions I do have a question like um so at this point after this presentation maybe I will jump to use I mean for me as you say as you said that as you explained that uh formal verification is actually a better uh it's better than fast testing like I would replace every fast testing but I think it's not actually um the greatest definitely not better in the sense that you should give up all your fuss tests yeah um you should do you should definitely do both like use fuzzing first because it's also way it's way faster um and you can write like 1,000 tests easily for like for f and then once you have these fast fast tests passing you can take the same test and throw them into control I mean they use the same format um so yeah but but ultimately I think you should be should be doing both like use a fuzzing first um and when the when the fuzzer does not return anymore can example use control on top of it I'm really to get the confidence that you explored every single edge case so I I also would like to know that um where do you feel like it's more important to do formal verification like on like I'm imagining on protocols or things that have huge complexity maybe so I'm assuming not all the development should use foral verification I mean I understand this is the the the pure way to go but I don't think for like small projects and things like this there is make any sense to use so I think the main resource here that you have to take in consideration is is time basically how much time you have to devote to um do the symbolic execution because we're trying to make it as easy to use as possible by um as I was showing showing here uh basically reusing the same test that you use for fuzzing you can use symbolic execution over them but at some point even if you run those test with symbolic execution you can go into these uh States or these branches that um you have to spend time to basically understand what's happening there and if it's a to understand if it's a valid Branch or if it's just some um again some branch that you're really not interested in and so you have to spend a bit more time to do this and it's also the fact that um as I was going towards the invariance uh topics it takes uh it takes some time to execute something symbolically so the examples that we have here take around two to five minutes but uh if you run some uh more complex code you can get towards a few hours and I remember a few like last year or so uh we worked a lot on performance and we were able to achieve these uh times that are you seeing now but we used to have proofs that would take three three or four hours in like the best scenario so um yeah you don't this is not a present this was not a presentation in which we're trying to convince you to drop unit and fast testing so those are great ways to test your uh project and um you shouldn't drop them this was just something that okay you have uh you have a test suit with which with which you're happy uh but you still want a higher level of of confidence then you can use something like control on perhaps on your CI to run before the release for example um and yeah also I I was talking about invariant uh so because of the fact they are so brittle you can't even it doesn't really make sense to write an invariant early on in development because it will change a lot through times um so yeah I don't know R do you have something to add on this yeah so obviously it makes sense to start formal verification with the most critical um code paths in your code base like the one that are um transferring assets obviously a good Target um and then work from there I mean if you're a security minded protocol you go uh through different security audits maybe and that's also a good chance to talk to the to the uh weevie team and ask them what they think are the most critical code pathes because they may come up with like new scenarios that you didn't know about and so um they can inform this process hey what should be formally verified next in our process um yeah always good like start with the functions transfer assets and then um ask ask your development team ask the auditing teams that are looking into the code base what else should be covered um what is like what is a whiskey function um and and start from there yeah okay thank you for explanation oh great so um if there are no other questions we are 1 hour and 45 minutes into the presentation so um last call okay then so uh thanks a lot guys so uh great presentation and uh personally waiting for the tools I'm I'm really looking forward to try uh the symbolic debugger and uh let's keep in touch and we when you have some news just drop drop in some um uh messages let let's talk talk again and um hope you have a a nice release of the tool and um thank you and thanks for having us uh it was a pleasure looking forward to the recording sure yes sure thank you so thanks everyone see you around thank you yeah thank you everyone