Building Secure Contracts: Use Echidna Like a Pro | Devcon Bogotá

foreign [Music] secure contract using fuzzing before we start just to get like a sense how many of you have used the kidney in the past echidna it's a what we're going to present okay okay so who are we so Gustavo Greco and myself Rosner Feist we are both security researcher at trail of Beats if you don't know us we are a company where we specialize in high hand security technology we have expertive in blockchain but also another topic for example we do a lot of cloud native application or we do a lot of cryptography with like weaker stuff and so something that I think differs from other company is that we spend a lot of time trying to apply research and program analysis into like our daily job as a result we have built a lot of Open Source tool you might know slitter which is a static analyzer for solidity a kidnap we are going to talk about it today but we have a lot of other tools for example tiller which is a static analyzer for algorand armana which is static analyzer for KO and so on four techniques the first one is using unit test the second one is using manual review and the two last technique are using fully automated or semi-automated technique I'm assuming everyone here is familiar with unit tests you should use any test and they are good usually to cover that the system is working as expected in the happy path something that we have learned over our audit and I know those analysis that we have done is that there is no correlation between the quality and the quantity of the unit test and the likelihood of having high severity vulnerability and this is we actually have an academic paper on this where we have looked over like all the audits we have done and this is a correlation that we have not found and the reason why our intuition tell us that when you are going to write unit test you are going to try to cover happy path things that are supposed to do in the correct execution while vulnerability usually lies in the edge CAD in the things that you haven't considered an example of a unit test the second technique that you can use is manual webview so you can go line by line and try to understand what the code is supposed to do what is actually doing and if there is like a difference between both doing manual review requires specific set of skills it's time consuming it's it's it's kind of difficult to do usually you are going to go through a security company to do a security assessment um to have people that have this specific set of skills the next technique that you can use is using a fully automated tool these are like the two that are going to find some of the common bugs you're just going to click on the button and the tool is going to tell you there is this type of work or not for example you might know Theta which is our static analyzer for solidity this type of techniques might give you forth running um but they're also really powerful because I might cut you know like a critical bugs you oh yeah okay okay so first Rita like the best technique is spend one hour like the first time you try it uh there is a triage mode so once you have triage like the ways you as I won't show up like in the next execution and if it takes you like one hour and at the end of the day you might be able to catch critical vulnerability I would say it's worth going for the first result and look we are we have like a list of trophy for uh Twitter that demonstrates that we have found a lot of like actual bug using it so yeah there is like a false positive pass for for false alarm but it's not going to take you so much time and it's going to provide you value for example we have a git abduction with Filter when you can connect it to GitHub on every pull request commitment depending on how you are going to configure it it's going to run if to see if you are introducing new new vulnerability yeah perhaps sorry perfect perhaps next uh Year we will do a slitter workshop on you and this is open source and it's free okay the last technique that you can use is using semi-automated analysis so these are going to be tools for which you are going to provide some information for which you are going to have a human intervention to explain to the tool what you are looking for and this is a bit more difficult to use because it requires like this interaction from you know from the user it's a Technique we are going to see today with property by testing with action now so what is property-based texting to understand how it works I have to introduce fuzzing so first thing is a standard program analysis technique that is used a lot in traditional security the idea is basically you provide a one-time input to the program and you try to see what's what's going to happen you try to stress this with random input the most trivial uh further that you convert you just go on your keyboard and you know you patch random bottom and you see what's going to happen on your program um again it's well established in traditional security we have a lot of tool if further go further and so on however most of the traditional feather are going to look for memory corruption for crash in the program we don't have a lot of memory corruption on solidity there are some but they are not that common what we are going to try to look for is a property of the system that can be broken and this is why we call it property based testing basically the way it works is that the user is going to define invariants the further is going to explore one Dome is a program and it's going to try to save the invariant odd or not you can think of you of feeling really as like unit tests on steroid well with unit test you try one specific value with the program while first thing is just going to try randomly a lot of different value I've been talking a lot about invariance or what an invariant an invariant is something within your system that should always be true it's something that should never be false or that should never be not possible to check if it's actually holding so I'll talk also about ekina so echina is our further for smart contract interpensers we have been using it for like four or five years even now uh in all our audits you can see a list of uh match your code base actually using and I've integrated Echidna in their process for Aquino we are focusing on the you know ease of fuse so the invariant are going to be describing solidity we have a GitHub action similar to slitter and we support all the compilation of framework if you use Foundry are that Bernie travel whatever we're going to support it because we are using it in every of our audit and every now and then someone comes with a new compilation framework okay I was talking about invariant so let's say you have a token you have a Neo C20 token it has you know a balance you can transfer token what would be an invariance an environment could be that if you have a total Supply no user in the system should have not talking to the total Supply right if you have 10 million of token if a user of 20 million yeah something is wrong the way it works is that you're going to take the contract in solidity you're going to Define invariants which are going to describe what you are trying to check one way to do that is to create functions that are called echina underscore some name this function should work on a Boolean is a Boolean is true the property or if the Boolean is false or the property is broken you give both to Akin now Akinator is going to explore one Dominator program and it's going to try to see if it hurts foreign for you so we have we're going to have a couple of theory of exercise where you're going to try to apply again now and to Define some invariant on the system you can go on this repo or you can scan the QR code to object repo check out the Defcon branch and open the first exercise if you have any problem to install Akin now if you have any question let us know we also welcome everyone who is not into the exercises just to see even even if you're already uh know how to do how to do testing or even if you if you use fasting every day uh it's it's totally fine we will happy to take uh any questions simple or more advanced about how Echidna work so please feel free to to do it and we will take 15 minutes for this uh for the first one okay so the question was what are the benefits of using Echidna other Foundry um so first I think echina has more features than friendly at the moment they were developing Foundry for like six months we have been using a canine like four years we support any compilation framework so let's say you are using r dot because you want to do integration test and you need some complex setup using like typescript or whatever if you move to Foundry you're going to have issue because it's more difficult to you know create this type of test so you end up in a situation where you need to have a setup with two different compilation framework if you use some Advanced options then you have to need to have like both Advanced option in both compilation framework if they support it and it's a lot of you know like maintenance um here we are like you know agnostic to the compilation framework in that sense we have we're going to talk about that later we also have like a couple of advanced features that the others I don't have for example something that you can do with echina is that instead of trying to find in there that are broken you can look for functions that consume most of the gas so you can list the further one and give you a summary of okay I can learn this function with this parameter and it's going to Output this amount of gas and if you are looking you know for on this type of things uh it's very nice hey there uh Brock from Foundry here um I'm curious uh how do you go about benchmarking uh a fuzzer right so how do you um because it's something like for us it's just a black box yeah and yeah okay that's a really good question and even in like traditional Feathering you know like if you go like in the literature of whole feather or benchmark I would say that most of the benchmarks are poor or one of the issues that when someone does a benchmark to you know benchmark their own tool there's a bias all right so we we have Benchmark we have our own Benchmark to try to see you know like in our past audit and everything how it works and everything but obviously we have a bias like it works well for us because we are you know building the tool on our example um so I would say like the best place to have like a good Benchmark for fuzzing should not come from to level yeah yeah it's it's also an open question what is your benchmarking like if you if you are if you're saying well this is faster than this sort of thing but it could be executing just always the same thing like you know calling a constant function over and over again is going to be faster than calling some deep deep part in the in the call uh on top of that you have like bugs what about like finding bars how much bugs you found and there is there are a couple of academic papers saying that some people uh like to compare this but you have a like um like a plot saying how many Bucks you found and let's say that one faster is better than the other but you don't know if the next hour you will have a a peak saying well these found a lot of things so there are all the things that you can do so you can use coverage but also coverage is not going to give you like uh uh it's not going to be the the ultimate answer so it's it's still a debate how long you should run faster for a benchmark or even for you know testing something it's also a debate what you what we should use for benchmarking uh should we use like complex defy applications like but how many of them we have like 10 or 20 we don't have thousands of different device so it's it's uh we we definitely are interested in a deeper discussion on how to have a good band merch set for for touring and we have the same problem for example with Rita well how do we Benchmark it our static analyzer provide good weather and it's tough um we usually tend to have a practical approach in the sense that if the truth provide value during our audit if it helps us you know to find bugs and we make us faster that's good enough for us yeah and at the end of the day also depends on the invariance if the if the if the developers don't know how to write good invariants then no tool is going to provide some magic um value so it's it's it's tough okay okay and I'm happy to discuss with with The Foundry team or any other team doing doing fasting we will will be here uh today so please let us know okay my other question is regarding like the tool is only for passing for its support like symbolic execution or something like that so yeah you want to yeah it's it's only for first thing we have another tool for symbolic execution which is called Mantika however and something actually we're going to discuss later I think in practice any formal base method approach is going to have a lower return on investment at further if you have two weeks three weeks to work on a project you know and you want to invest some resource to increase your confidence in the project first thing is the best solution yes and uh and also we found that so Echidna is a tool that works with our static analysis leader that gets value so you have in some cases like let's say that you have a test that says if x equal to some some value some uh traditional fossil techniques have hard time to deal with this but what we what we do is constant mining so we scan all your code look for these magic values and we will play these magic values and some mutation of that from time to time so or fossil should be able to get inside the inside this if you if you if you have a test case that is not that is not working please let us know and we can try to to see it but in practice it seems like some of the typical use cases for symbolic execution in which you have constant uh Magic values to to look for they can be replaced by uh constant mining extraction how many of you have issued to install Akin now to one like the exercise how many of you have issue like installing akina or opening like the different exercise okay uh no you you you you you have to open your terminal and a kidnap will deploy the sort of unit is still installed the tool and when you put like equipment you cannot test some contract it will compile it running inside the simulated blockchain and give you the answer so you don't need to connect into something uh so yeah going to them into the repository and it says like yeah yeah so yeah this is like your traditional one but if you go into the Devcon branch that is sorry yeah so it's it's it has more specific yeah so so over there you said like if you're using Mac you can do that that or you can download okay yeah okay yeah so I wanted to highlight one one little feature that we are testing on Echidna that is that is also used in fasting but instead of testing a property where we are doing minimization or maximization of some value so this is an a new thing that we are that we are testing it is not property based testing but it's it's something it's something that we are trying that we are trying to push so if you want to know if a user is it's capable of uh extracting tokens from your system without you to realize you can use that feature just saying uh Hey Echidna can you maximize this balance of this account so it will try to generate you the maximum sequence so it's it's it's a little bit outside this but uh it's something that we wanted to mention okay so our Target here is a token um it has a transfer function like a classic Crosshair function you enable it from a possible contract which is like a basic possible system and what we want to try to do here is to create the invariants such as no user should have a balance above the total Supply test the tokens where we are going to do it is that we are going to inherit the token or Target we are going to create the contract test token we are going to initialize the balance of the colors of the first user to 10 000 and this is an initialization so you are creating a token there is 10 000 in one address and no the invariant is simply that um no user so the user should not have more than 10 000 okay again you deploy a token 10 000 token to one user this user should never have like 20 000 token all right and if you want this with a kidnap a Kina is going to tell you that this invariant is property on total Supply was broken it failed and it's going to tell you how and the answer is that you just call the function transfer with the destination address 0 and 1093 token so what happened here this was compiled with solidity 0.7 so there is no overflow and underflow protection so there was an underflow problem here where if you try to send more more tokens that you have a new balance the balance is going to render flow and you know you have a really large balance something which is interesting here is that we Define the invariance you know without looking at the code without looking at the function we were not looking is there any issue in the transfer function we just Define an invariance and by doing so we can realize that there is a bug in the transfer function um so this is a kind of a nice a way of trying to find bugs because you don't look at the individual function necessarily you can just Define invariant and the further is going to try to break the environment for you does that make sense any question yeah okay so okay so the question is does it execute a specific function or how does it know which function to curve the answer that is going to call everything so in this token if you look at like the word source code you have a transfer function possible function and like some additional function so the federal is just going to call everything and everything external or public like everything that a user can call okay the question is if you have a very large token or very large contract you have a lot of function so here you can take different approach either um you want a keynote to call everything and you just do nothing and you let it now when uh which might work no it depends on what it is if you know that some functions are more important and you want to Target you can change in the configuration configuration file of echina and tell him call only this function or don't call this function so it depends what you are trying to look if you want to increase your confidence you should call everything if you think there might have an issue in a specific function and you want to focus on that you can you can Blacklist on white list depending order okay so the question is can you define the order of call you can Define the order of the initialization but not after that I think it was another question no okay okay okay so the question is um can you have like a better log because obviously this is like a simple example uh and when you do want them you know exploration you might call a lot of functions that are not necessary for what you are trying to to call right and the answer is yes um so Echidna does what we call shrinking where once it found a way to break the invariant it's going to try to reduce the choice so it's going to continue to First more or less on the seminal iteration uh and trying to reduce like the size of the of the trace foreign [Music] Target so you're going to try to have an invariant um on the same token the first invariant was that no user should have a balance above total Supply here as we kind of hinted before now this is a possible system so it's a system where the owner can pause or unpause the system and what we want to verify the environment we want to have is that if there is nowhere now and the system is pause can someone unpose a system and this is what we're going to try and yeah let's take 10 minutes for this one I'm going to show the solution for the second one so it's the same Target that for the first exercise but here we are going to focus on the contracts that were inherited by the token you have two token now you have two contracts right ownership and possible and here you have a system where your owner and you can pause or resumes as a contract and what we want to check is that if we drop the ownership and we pause the system is it possible to unpause it so here we have a bit of initialization to do what because we want to drop the ownership and we want to put the system we are doing this in the Constructor so we are calling pause and oh no from now on the system as a contract is deployed it's pause there is no no the invariant is then just if the variable that you know tracks the possible state of the system is true and this should hard work you pause no ownership it should be always post and I cannot tells us that it actually failed and the reason for that so this is kind of like an old bug that were really frequent and common in old version of solidity there was no constrictor keywords and where you were doing the Constructor that you needed to have the function name which was a match with the contract name and here you have the contract ownership and a function owner and because of that the functional is a public function and anyone can call it and become the owner this does not work anymore with more you know modern version of solidity but the type of bug that we are finding a bit more a bit too much in the past something which is interesting again is that you know we did not look at the ownership contract we did not look like at the implementation itself we just Define an invariant and without the one of the further one and you found the environment for us so now bring the question on how to define it okay foreign okay so the question is is defining invariant part of the auditor you know work uh yes like we are using a Kinder in our audit and during our audit we are going to Define invariant and something we are going to do that we are going to discuss with the developer because the developers know you know better than us what the system is supposed to do so we are going to have this collaboration with them to understand what the system is supposed to do and to Define this variants foreign how to define invariance because you know like if you have bad invariance it doesn't matter what you are doing you know if you are using further if you are using like formal method if your invariant are not good you're just going to check for some things that you know doesn't matter the best approach to writing variants is not to start with a tool it's not to start with you know writing down solidity invariant is to start with English open a file and markdown file or whatever I know a format you like and write in English what the system is supposed to do start simple start with invariants that you know you know are true start with things that are not working once you have 5 or 10 simple invariants buy them in solidity and when the further on top of them if the invariant are all holding then you can go back to thinking about the event of the system and you know go more deeper into into the environment themselves if something is broken then look if the invariant is incorrect or if there is an actual bug and iterates go over um yeah in in our experience when we work with uh with um with clients when we ask them to do step one undefined invariants they are actually uh they they realize about bugs so it is already a good a very good thing to start thinking into that even if you don't if you're not testing yeah okay okay so if I understand correctly the question is that can we connect this to mainnet okay okay how to use it with other contract so you can just in the Constructor deploy the contract uh something that we are not going to cover here but we have a tool which is called itino which is basically going to take your unit test take like your suite and we play them in Echidna so for example if you have like a complex integration with like you know you are deploying in your unit test 10 different contracts you are deploying like a knockoff unit swap or whatever you know you need and you can replay this in the keynote so that everything is going to be set up yes yes I I uh I think there's some a little bit something else there that you want to what if you want to Define an invariant on a uni swap contract right that you that you are using that your contract is is is using so you will need to know how Unison uh Works in order to put it in your environment like if I'm swapping something then I'm getting something else right and in that case you need to realize that it's difficult to write invariants with other people called right despite despite this is working and everyone is is using it but every time that you use a third-party contract then you have you are importance on risk and you need to completely understand the other contract in order to know what is going to the effect in your own country I so there is case was we have a special uh I'm from gearbox protocol and we work on composable Leverage and we have adapters because we just provide leverage for some other contracts so when you combine gearbox with uni swap you get immediately um margin trading and in this case it has adapters and these adapters incorrectly Parts path to make check after uni swap however they integrated and may call to existing uni Swap and guy who were on immuneify problem he write a small test and this test show us that if you really add some additional part of call data it could be interpreted incorrectly so we have two different ones our system could be fooled check not Z balance which should be checked and in this case it was a fault of the system and the funds could be drained and in this case I think we could find some fuzzing testing to really provide any information but this test should work with uni swap because we behave in different way and we shouldn't cover that because we run with mocks and MOX of course was created with the same bug so MOX was okay but real implementation total different and I definitely believe that fuzzing should found this mistakes yeah yeah definitely definitely when you are creating a mock you are assuming how everything works and if your assumption is not precise enough it will it will you won't be able to detect something and we as an Auditors it's it's common that we have to audit contracts that will interact with other other contract let's say compound so when we go into compound we have all the documentation and says well compound word like this or like that when we look at the code and see some things are not documented and we go back into the developers and look look if you're if your contract is doing this so that it will revert and you're not testing for that so it's when you when you are using a third party uh contract you are importing the risk so either either you have really good tests or you even uh make sure that you understand everything otherwise it will be difficult to catch the uh but yeah I think this type of work can be found with fuzzing like the most like the difficulty is going to find initialization that makes sense and then that makes sense um that's why that's why you know we are kind of in putting like the infances onto defining environment because this is like the key component of this technique yeah uh in terms in terms of speed is it okay to put all deployment script into Constructor because of course if you deploy such a huge system and you deploy some contracts from external repositories like uni Swap and so on it requires time and of course when you want to test million operation if you redeploy each time holds the system it could require hours or days I know yeah so so so when you use Echidna you deploys only once and then the when your test finish it will go back to the states after the contract is deployed there's no need to redeploy it and that is why we have we we ask the developer to have fixed amount of parameters in the deployment right on the on the on the Constructor otherwise we will know what what we should deploy yeah I think there is a question over there also um I'm just wondering as you uh once you've kind of defined your invariance um and I imagine you guys in your audits you you run through these and um basically I'm not trying to understand when you guys have confidence that yes the this is a good invariance uh from and and if there are any metrics that you guys use uh internally like I see it's outputting Unique instructions and unique code hashes those sorts of things that uh give you confidence in in what you've done so in practice you know you can look at the coverage but usually coverage is not a good indicator and In fairness like you know when we do that we do this in a time box manner so we have two or three weeks to do it and we're going to do our best in two or three weeks uh that's the best that we can do yeah it's it's it's we there is no uh Silver Bullet for this um it we when we do a report we list the invariance that we test so it's it's clear what what we tested and what and everything else was was not tested with all so we will perhaps did Manual review or use all the techniques like Slither to check some some other things uh but yeah unfortunately there is no uh good way to to Define this uh but perhaps I I personally think that talking with the developer early on the invariance it's a really good thing it's usually the case that we think an in barrient let's say that some some value cannot be zero and we go into the into the client and says is this an invariant we don't know because we have not designed the system and they don't know and if they don't know that's that's an issue right we should we should absolutely know what is the behavior of the system and and if we don't know if anybody should should if something should be an environment or not then we should go back and rediscus that and yeah Security in general is not binary it's not you know yes or no it's really a matter of how much resource you want to put into it and moreover social put more confidential thank you thanks I have a question actually more related to the earlier question which is a big uh class of bugs that's been occurring recently and for a while now are re-entrancy bugs right how do you deal with finding um violations of invariance that correspond to external contracts in that way okay so this is a really good question and in my opinion the best tool to find way on Transit is static analysis so the question is more to find which technique you should apply for which problem and for things like Korean transition static analysis is just going to be better you can use further you can create like random callback and things like that but in practice static analysis is just going to outperform any further this work uh that's why like for any any class of vulnerability which is kind of a pattern base you can use static analysis and it's going to be better in my opinion foreign one more question what's your addition for example we have a complex system and we want to make a classical fuzzing with the kidnap and it seems that to really cover many cases it requires a lot of computational power so maybe can you advise some cloud provider or how to do to run it maybe for a week with very powerful computer to get something achievable because of course this pretty simple contracts could be found on my MacBook but if we go a little bit further many contracts many setups maybe it requires more computational power um so do you want to talk about the kinapad so the question was um if you want to run a key down the cloud or on a lot of you know a large like system how can you do it yeah yeah so so so the first thing that uh you should know is that uh uh very large contract it can take some amount of memory so first first thing get a good server with with a good amount of of memory and CPUs um so the second thing is uh every um we have a python companion tool called in a parade that will run echina in any number of uh any number of uh concurrent um uh instances so you can run 10 at a time uh but we're not only going to run it 10 of the time but we are going to randomly Shuffle parameters because in some cases there are some there are some issues that can be easily found with let's say three or ten transactions and some other issues are going to be more easily found with two 200 transactions in a in a in a row right so what we do is we run the tool in different with different random parameters and in different let's say Generations so we run we run akina for an hour 10 times then we save the Corpus and you can get you you can see all the all the all the code that was covered and then we started again but taking the the the output of the previous generation so you iterate over and over again so you can see how your code is explored right or if there's some part of the code that is not explored with 10 different uh instances you can go back and say no I need I need to change this because it doesn't depend on the on the actual execution so we can we can give you the link uh for that it's just a python tool so it's it's it's easy to use um yeah it's also open source like everything we are doing is open source okay so yeah like it's really about spending time and thinking about our invariants and it's not simple like it's the first invariant that you are writing leads to a bugs there is something wrong about your approach uh you should not have like simple invariants that you know are going to work the system so we'll start simple and iterate over them okay to give you some example let's say you have a now with magic libraries what environment can you have um you can have commutative properties a plus b is equal to B plus a you can have identity a one multiplied by two should be true our inverse if you add something by its opposite it should be zero this is not always true right but depending of what you are building this might be like the type of property you are looking for for token we already talked about the first one no no user should have a balance above total Supply let's say you want to look at the transfer function and patsync transfer function what does it do I'm transferring token to someone so at the end my balance should have decreased by the amount and the receiver should have see uh its balance increased by the amount and let's say you try to write something like that once you might quickly realized that what happened if the destination is myself so if I transfer token to myself my balance is not going to increase or decrease quite awfully so this is an example where you might try to Define an invariance on transfer it might seem simple you might write like the the thing in solidity and if you do that again is going to tell you that there is an edge case where if you transfer to yourself like the event is going to be to be broken and in this example if you go through this um it's not the code which is bad it's an invariant that was bad so that's why having this iterative approach uh is really important because sometimes we are going to make assumption about your system and you might actually be wrong and as the system gain on complexity it's more and more likely that it's going to be more difficult to refine the invariance something else which is also important to to consider is um patterning first uh reverting for example an environment you can have is that if you don't have enough phones the transfer function to the revert or a return first depending on how you implemented the token once you have this list of invariants usually you can split invariant into two categories function level invariant system level invariant function over invariant are usually stateless they are things that you can just you know look at a specific function and try to see if it holds so it may take you know environment I mentioned are stateless and our functional leveling variants here you can craft simple scenario just by calling the specific function then you have system level in there system level environments are usually more complex but they're also more powerful and here you are stateful you are going to change the state of the contract and you are going to try to see the environment no matter the state and here is why it's important that echina is calling all the different function because it's actually what you want to try the balance being below or equal to the total Supply is an example of a system level invariant one thing that you can use is a different modern incidence of calling Akinator underscore something we support a session so you can just create function put assertion and try to see if it holds a SIM for system level environment as we kind of already like discuss it might be more complex depending on the initialization of your system uh if it's a simple initialization you might be able to do everything in the Constructor if the Constructor is too large for like the bytical size or for whatever reason you might have to split it and here is where you can use a kid now 18 outside okay all right so let's let's see this uh particular piece of code let's take um uh half a minute to read it um it's it's basically a buy function that will uh call an internal function valid by uh so what we are going to do is we're going to think uh what are the type of invariants that we can have here and what what is what will they are going to test and what type of guarantees we're going to get from this so let's let's take a few few seconds for this foreign yes so we have questions okay so the question is uh testing timestamp dependent so it's clearly not not the case here for timestamp depending code uh um a kid now when it runs it automatically increase either the block number or the block timestamp inside some range right because it it happens that some code will fail uh when the timestamp is increased into a really really large number but yeah 100 years or like the end of the universe so we don't care if if the smart contract has a bug that can only be triggered in the end of the universe will be the least of our problems um all right so yeah any any idea what are the type of things that we can test here first one the first one we can understand that how much token how many tokens we can get as a result follows our expectation when we're sending message value because as you can see it's a hard-coded rate is around 10 so basically it's a pretty simple formula we can change different values we put into the function we have totally prediction how much we can get and then we can try to verify that it works yes exactly so the the property is related with the amount that we can get even the number of uh weight that is sent so um yeah uh we can so the first thing is this this code will depend on the state uh we don't have the mean function so we don't know what is what is inside where we have the valid buy function that is actually abstracting the thing that we want to that we want to test so we will start with valid by which is a pure stateless function um yes so we were thinking about invariance here related with um the amount that we can get so this is these are very simple without going into specific uh this is a very simple invariant if the amount if the Wayside in C is zero then the user should receive no tokens at all right so so that's it's it's even simple and thinking how how much well I a user should receive but it's a Concrete case and it's it's kind of a corner case so it's it can be important to test all right so how we can test this so there are a couple of way to test it this is um this is one so we we can write a function that will take uh one parameter so again I will put any any number there however we're going to restrict the number uh the input of this function to be non-zero uh then we're going to execute valid by um and then we want to know if echina can reach he can reach the um the statement after that because valid by Will revert if if the uh if the inputs are not uh the one expected um so we want to know if we can get if we can get tokens despite sending no um no value right and so perhaps you're wondering what if what if the ceremony is zero uh then clearly this code will not do anything interesting so she was just is going to revert uh when you're writing tests you need to so you can put any any amount of requires or preconditions or people usually call it however if you put uh if the preconditions are too restrictive and your uh your function reverts most of the time it means like you're not going to get value from the execution so every execution reverted in a test in an invariant let's say that every every case that you don't uh that you don't use it's going to be an execution an execution that you waste so in this case you only waste one one execution in a range of in the full range of uh uins 256. so it's not a big deal but if you have if you put a lot of requires that only a very small small amount of uh values well satisfied and it will be difficult to get randomly or even even with the with the techniques that we use you will need a slightly different approach but yeah we will we will uh then go later into that so any any questions yes yeah so as you mentioned uh in this case that we are basically sacrificing only one uh one case which is when it's zero uh but is it gonna run over the whole range of un256 because that's a really large range and and it doesn't make sense to test all of that in some cases yeah exactly so it won't there will there is no tool in the world that can run for all the all the range uh it is always either either uh symbolic I mean you can do it symbolically but it's it's not it's not going to test all the values it's another thing um and uh fasting techniques are going to sample let's say randomly from the from the input or with hubs right um it's in the case of Echidna since we are going to compile this code and it will run through or static analyzer we will detect some interesting values in this case um 10 for instance 10 10 is an interesting value there it's a it's a constant and it's going to be used somewhere so definitely we want to we want to test with that constant okay so let's see what happens if we if you if you run so this is uh uh so kinda will run a number of transactions it will eventually detect that assernal free token has an assertion failure however this is going to be in a context of 100 of transactions random transactions that perhaps will do something that is completely unrelated but what we'll do is input minimization input minimization is a very old technique referred to testing in which you have a list of bytes that affects a bug you want to remove that bytes um one by one or in some random way in order to get a um a list of bytes that will still trigger the bug but it's going to be minimal or or either local or a global minimal depending on the type of tool that you're that yours so in this case uh we can uh a kidnap will try to minimize any any uh parameter here we have only one parameter and the parameter is actually is actually going to be useful triggering about if we have more parameters they are going to be minimized towards zero so if you have units uh then it will be reduced until zero so zero is the simplest um uh value this is arbitrary defined on the uh on the code you can you you can change it if you want and but in this case the parameter cannot be zero because if it's zero the the test will pass right so in this case the minimal amount is is one it's not guaranteed that you will always get this smallest uh set list of transactions to trigger uh this is an uh an MP complete problem it cannot be solved on on linear time so it's it's all going to be always a sample but in in practice uh even randomly sampling removing transactions or reducing the complexity of each uh value will will give you good answers all right so a little bit about ekina apis maybe we can just explain um yeah just explain why it's happening [Music] um yeah so yeah so the issue here is that if you send one desire token what's going to happen is that you do one divided by 10 and 1 divided by 10 is 0 because you are winding down and other results uh the required amount to be sent is zero so if you ask any number of tokens below 10 you are going to get them for free and this is again again an example where we Define an invariant we don't actually look at the formula we are not looking at how this formula works we just Define an invariant that if you don't send ETA you should receive not okay and by doing that akina can find you know how it matching issue and we actually evenly using Akinator for bonding for you know mistake in the formula and and so on yeah oh yeah yeah I gave that this function is for testing purposes but um in a real situation where Cent is not part of the of the signature of the function right you read that from the message yeah yeah yeah this is happy like like deeper into the code right right so how are you doing that okay you read that into the a certain function how you do that so yeah uh uh if I understand it correctly so this this could be an internal part and you can have like a lot of code that put like gets the value from them from the message value and then do something else ah you can do that uh yeah I mean I mean is this depends on on your code here we are testing an internal function right using using some some defined yeah yeah yeah and if it was using message that value um yeah exactly and if you have a constant in your code saying message value should be uh 42 42 42 it will use that constant eventually so you should be able to hit that particular that particular case given the fact that this is random something of course but can you uh moving back to the previous slide to the function what I'm really wondering because we talk about this error whoever tokens less than is uh so way less than it's so small amount and the same problem which could be here is Overflow if I provide a huge amount of ease because we have a multiplication to decimals it could be done on the other side we all of us know that the quantity of s is limited you can't even take a flash loan and get more ease than it produce so what is the best practice follow this formal execution when you write fuzzing tests or take some real examples as limitations as there is no match as zeroom as it exists at the moment and we know it's a deflation so we can simply assume that in the future nobody could take so much to get overflow here yeah yeah exactly so yeah this is is an interesting question and it goes into the fact that what are your assumptions on the test right if you if your assumptions are like I have this token with this limited Supply that should never go over something then you you can just say I require that that the value sign cannot be more than the total supply of something right but in the case of interest is a bit more tricky and and in fact in in Echidna what we do is we have we have externally on accounts that are simulated we loaded with eater every at every transaction because you can have a very large amount of feature you can take a flat loan uh you you probably cannot have as enough eater to overflow uh you into 256 because that will be a real issue for the AVM uh in in itself but um we can we can Define in the Kinder config which is the maximum amount of value that we send per transaction right so if you put like I don't care if the attacker has more than than 10 000 liter because that will mean that they can do other things then Echidna will happily uh take that limit and will never put something more however it's still the case that over several number of transactions the accumulate number of features can go over that that barrier so you should you should be careful with it and there is also no project you can take here so basically you are building an invariant and the invariant of which we thought as like a value so either you start where the invariant has really limited Twitter like really with chain one and you try to see if it hurts if it's working with like a you know like with one meter okay it's already working so you can continue like this if it's not breaking then you can increase this with time from time to time or you can take the opposite approach if you define an invariant where the threshold is really large it's working because it's really large and then you decrease this result so that's how you start really limited and you know depending on the result you remove the limitation or you start without limitation and you reduce like up up to the point where you have a kind of like a value for which you feel comfortable with yeah yeah and and that is also related with the if we start with very large values we we could have false positives but and if we start with very small values we can have a false negative but which are the ones that are going to cause you more trouble that is something to to think about it because if you miss one's false positive your your protocol can be you know destroyed and if you miss one one false negative then it's okay all right hey there in terms of fuzzing mutation uh do you do any clever things like uh say this function has a constant of 10 so would you then uh see the constants in the the function and use that as input yeah we reuse the constant forms of function and we will first I want the constant also like if you see 10 we are going to use 10 we are going to use 9 11 and you know like uh around uh yes there are some there are some techniques I can show you a little bit after a few lines of the code of Akinator that shows all limitations we have mutation interesting mutations on list of transactions in which we Shuffle we do uh we do like splice as well so we take a list a list of Interest transaction and another one and we splice it on a random position so there are a couple of fun things to to look at but uh yeah I think we should move on a little bit um all right so as I was saying we have this uh failing even if you don't understand what was what is the failure um well that is that is a different there is a different Beast sometimes you you you have you put your your um your invariant and your invariant feels and then you start the journey to understand why it fits so that's we are not going to talk about that you uh some people like to re-u run We Run The failure into a unit test to make sure step by step what is what is going on but yeah that's that's a completely different uh type of Beast that is related with what happened after and how we can fix how we can fixation all right so a little bit about ekin apis this is um a topic that um it's uh it's it's still an open debate in some in some cases so what are the best way to test to create properties so Echidna supports a couple different ones it's about Boolean properties in which a function uh is executed um and then it will it should return a Boolean true or false and if the function reverts for any reason that is the same as returning false right so if we go back a little bit we can see over there error and recognize op code that is going that is related with the assertion failure this that is how um on version of solidity used to uh have um this uh assertion failures but if you use Boolean you will just say return false right so you know exactly how how everybody fail uh or it could be a revert so you you say over there you see over there it revert okay so either you do Boolean properties which are the classic way to define invariants and these come from uh uh some some real old techniques uh in particular quick check which is which is a property based testing tool for Haskell and then a couple of other languages uh which was an inspiration for for for this then you have assertion failure so every time you see uh every time uh the the assertion is called with false that is uh that will fail however if in the context of your function you see a revert that will not make the function um the property fail here we can see that if valid by reverts then the this Kindle will not report that because we are using assertion mode fine so you you should be careful if you are using if you if you cannot rewards uh you should have to uh either use the um the type of um the Boolean type or what you can do is if you care about reverts invalid boy and if it's an external function you can do a try and catch and you can check which type of reverse and you can even fail in some type of reverse and not in other because you want the user to get a good message of of alert and perhaps other type of reverse you don't you you want to know so and finally we have the DAP and Foundry API in which um you will uh you will have um a function that if it reverts uh it's going to it's going to fail and otherwise it's not and I hope The Foundry team agree with us and it's uh is correctly implemented um all right so there is testing modes um in the in the um in a repository so we can um you can go there and it's explained a little bit more this is very high level overview so yeah yeah yeah so so so yeah again that's something returnable Boolean uh it's easy to Define uh no side effects that's that that is so interesting when you use Boolean properties all the side effects will be reverted uh before the execution of the actual invariant right but if you're using assert the side effects so everything you change in the blockchain will will remain so this can be really useful for testing some some complex code but yeah we're not going to well um yeah assertion is can be simple to to um Define um and it's it's it will also um it will also be easy to see on the code coverage if it's not if it's not covered or or not however some code especially some old piece of solitary code it's going to have assertion as required and that is a really bad thing you should not be doing it use require if you want to if you want to actually um have a precondition in your call and use assertion for for testing okay um yeah and finally we have the The Foundry and up uh compatibility the only thing well uh the thing that we don't support is pranks so we don't like to prank people so we don't we don't support pranks however we support some of the some of the um uh havm yeah the havm the original ones uh cheat codes you should be careful using it uh we uh we know that there are some uh catch with that especially related uh with what the solid compiler expects and what you're doing in your in your transaction so please be careful because you could have some uh um some some issues so we in we rarely use cheat codes uh we try to keep all our code as close at the solidity possible so you can easily Port it to another tool there's there's little Akinator specific uh but yeah we are also open to discussion if if the community agrees that we need a specific cheat code or we need to avoid some specific chicken then we are open to discuss it all right um so exercise four we're going to deal with uh um one of the um one of the exercise for dumb vulnerable defy so how many of you know this uh um amazing uh CTF um ah yeah sorry you you yeah we're going to keep it up yeah yeah we can yeah we can skip it this is term so this exercise was exactly the same as the first one but instead of using function uh we were using assertion so it's exactly the same invariant exactly the same setup but with a different API just as an example yeah so we will go into a more interesting example um but before that um there is uh something that you wouldn't need which is called the multi-aba mode um so we usually usually testing tools take a specific contract as your main contract to interact so in in the default mode echina will only target a specific contract that you can put in on on your command line or if you have only one contract you will use the first one right but there is something called multi-avi that would call every every contract that is deployed after the Constructor that you have Avi right so if you deploy something in bike in by code directly and you don't have Avi in the won't be able to call it because it doesn't know what is what is there but if you if you deployed a couple of tokens and several contracts and you use multi API Echidna will call any function in any deploy contract uh after after the the end of the Constructor so we will need these in order to deal with the next example because sometimes the the the the debug that you want to detect it doesn't depend on the state of one contract it depends on the state of many contracts and in that case you can you can be surprised by the fact that changing the state in another contract can break your your property and definitely we want to avoid that Okay so uh again how many of you know about them vulnerable defy okay a good number and did you actually well this is these are the first exercise the first the first two uh so I hope that uh uh people know so if you know this this how to solve it you should uh it's going to be even easier uh for you what we're going to do is we're going to uh take a look of this um sample so yeah I assume that we already you already have a code so um is the exercise the the naive receiver one um so what we want to do is we want to be able to drain um the the funds in Flash loan receiver right just to give like a bit of description of the of the challenge um here you have two contract you have the naive um we see the Orlando pool which basically yeah yeah it's it's over there um I can allow you to take a Flash run for a fee and you have a second contract which is a user uh contract that is going to interact with a pool and the contract is going to be the user contract is going to be deployed with some fund inside and the girl is going to try to see if it's possible for this specific contract from the user to be joined exactly so uh we we want you to review the the um the exercise if you have already did it it requires you to send some some some some number of transactions so in this case we are going to prepare everything for a kidnap to ReDiscover this without telling it what is what uh how how it can be uh sold so we will need two things we will need to initialize the um the code to have um too much what the what the initialization is it's um is actually showing us let's see okay so this is the The Flash loan uh the part of the or the flash loan so the the interesting part about this is we don't have to care about specific details in the code we want to we want to um give a kid now the same scenario that we have on the on the actual uh Challenge and we want to know if it can actually find a way to drain the contract so yeah we can uh we can see uh how the reciprocal function um works here but um yeah the interesting part perhaps is the initialization what we are going to do is we are going to deploy in the Constructor of our um test we're going to deploy the the contracts that we have here and prepare everything and then we're going to use a suitable um uh invariant which should be really simple you don't have to overthink and we want you to uh run a kidnap uh with that in order to see if it can drain the contract uh with the of course with a suitable um uh with a suitable invariant so yeah we will take um 10 minutes I think yeah yeah we are running out of time but uh let's take 10 minutes so the first step is really like this is a initialization from the test case of the contract the first step is really just to reply like this into a solidity Constructor and then provide the environment yeah so happy to take question questions or any technical issues that's a goal actually we are going to do exactly what he's doing here but in serenity there there is an alternative way to do it but the solidity approach is is easier to to avoid um because well the other tool is called atino that can replay this in a simulated blockchain like ganache and then send it to the to the tool so uh in that case you don't need to replace on solidity manually but you are still I still know still need to know where is everything deployed right so if you want to interact with the pool you need to know where is which is the address of the pool and you can you can then uh a kidney cannot actually call the Paul functions uh automatically because it has everything but in this case we're going to go into simple route uh that is going to uh take us to uh rewrite it's just a couple of and this kind of much what we're doing here in order we might look at the existing unique tests to understand the initialization and we might translate them into solidity if needed to assign credit for the invariants so yeah the the previous exercises are on the easy side this is a bit more difficult but still shouldn't require more than a few lines um so yeah but please let us know if you if you need some some hints there are some hints in um in one of the one of the branches in the hint Branch but yeah Heather uh hello yeah sorry no worries um is there any thought or current support for mainnet forking or um State forking of some sort not yet yes so not yet havm has support for that but that will that will need us to put uh that requires to do like input outputs on on transactions so we need to check if that will impact on the actual um on the actual um performance on the call um so yeah that will um yeah um I have kind of high level questions so I'm trying to think about what the limitations are in terms of expressing properties as invariance right so for example let's say we have a temporal property that we want to express like we have a wallet contract and we want to be able to say that any user who deposits their money is eventually able to withdraw it is that just like a fundamental limitation of Echidna or is there a way to so if you can so the notion of eventually it's you you need to have some definition on the or on the blockchain right So eventually cannot mean like in 100 years right so if you if you find say I will only allow increment of time up to some limit yes you can you can call it as a bounded version of that property but you cannot you cannot use it as a theoretical thing like you know I have a state which I don't know what it is and then I will transition to another state which I don't know which uh what it is and in that case you will need to know if the original state was actually possible and and things like that so it kind of works on on a concrete on on concrete States so you always have concrete data and you need to put like boundaries on the things that you that you can do so if you say a user should eventually uh receive this amount and eventually means like in a number of transactions and a number of blocks or timestamp then yes otherwise it's it's more like a theoretical proof that you're doing and you probably need another type of tool yeah I guess I'm curious even if you took like the bounded case because that's fair that you're dealing with like concrete traces here it seems like that's not or it's not intuitive to me anyway how you would Express that as like one of these invariants so you you will you will do something like this you will put a function that says uh and and you will need a state to track down like uh you you do a deposit and you will need a user to eventually receive something right so you will need to have a state that tracks deposit like a mapping right and you have a function that is your invariant so if um and then you receive the address of a user and you check in the mapping uh if if the time um between the last deposit is in this range then you were going to check something and if if the time in this in this other range you're going to check some something else so it will be like randomly checking in in transactions um and with that you will be able to cover uh given the fact that you're going to generate enough transactions and enough time times right so it seems like the answer is it's capable of doing it but it requires some like kind of manual adjustment of the code almost to add state of it so yeah you will you so if the if the property that you are testing requires to add State yes you will need to add whatever state is needed it won't be able to track state outside right the only thing that will be tracked outside is the increment between between the uh different blocks for instance so that that will be tracked uh outside a new Aquino will show you from in between this transactions and this transaction I have 10 blocks that will be tracked uh outside but everything else if you need to do a mapping between users and and the time between certain operation you will need to keep that in a different in installation in a different bio I see great thank you all right so we have some other questions hi um is there any feature that allow me to guide the future or the domain of values that I want to try um so in order to in order to guide the the faster into a particular State the easiest way to do it is to add um is is to add a small piece of code that will be auxiliary code in order to uh move the state from your contract into something else like for instance if you have if you have a contract uh the protocol that requires a deposit with a particular uh property let's say that uh you have three parameters and you need a deposit that has uh that has digital parameter in in in the Sim in the same number or in numbers in which in which are difficult to find you can have this piece of code but it's important to let the kidnap to explore freely at the same time that you are allowing information so it's it's actually important to know that as an auditor or as a developer you are adding information into into not just using it as a black box right so every state transition that is non-trivial to find or is really really important you you can have it and make sure that it can eventually execute it because it's going to be another another transaction to to execute but at the same time you want to allow the tool to explore things that you don't expect because if you just restrict says I only expect users to do these type of deposits then you can you can be surprised later because there there is a way to break your your property using things that you don't expect okay thanks and it comes down to the previous question where either you start with a lot of requirements and a lot of you know restriction in what you are trying to explore and if it odds you are going to remove some of the restriction or you start this opposing Direction you don't have any restriction and you know you go more and more restricted foreign yeah thank you okay so did anyone manage to at least uh Still Still start to create the Constructor or even run it uh to have some some invariant or even think about the invariant that you need thank you so in a couple of minutes we'll go over the conclusions and I will show the the solution um but yeah happy to take any additional questions thank you just from an implementation uh side I'm curious what um what actual like virtual machine do you use to deploy and execute contracts so we we use havm uh which is the Virtual Machine written in Haskell I know that it's in the process of uh improving and rewriting so it was moved from the adaptable into the ethereum repository so we are eager to test new features but yeah um if you use the Tino companion tool to deploy your contract it's going to use ganache um and you will serialize into a Json file and you can then load it into into that [Music] okay [Music] uh solution okay yeah we're going to quickly go over the solution uh so we can have a couple of minutes for for this so the solution requires first to uh deploy have a contract with enough amount of heater uh to to match what is deployed um and then um you can see here uh in we we deployed all the contracts that we need and send um the amount of eater that every contract needs and then what is uh what we're going to use we're going to use a simple very simple property that is going to say that the balance of the receiver is at least 10 liter so we don't actually need to follow exactly what the exercise says about draining completely the contract if we have one transaction that allows you to reduce the balance of the receiver then then it's then something is wrong and uh definitely uh it will it will eventually be drained so yeah so quickly if you run it you will see something like this um in which well the uh deflection has a has a parameter that is the the borrower and we can control this to in order to um reduce the amount of balance all right uh so yeah you want to go into the conclusion okay um yeah we're the second exercise on them ruinable D5 but uh we are running out of time this idea was the same we are defining an initialization which was a bit more complex and if you go through this exercise with something a bit more specific is that there is a callback from the contract to the caller so on the Kindle test you need to have like also the Callback to implement the flashlight but yeah [Music] so this is something we kind of touch on a bit during your discussion what about the other tools so there are a couple of other further out there there is Dub Brony Foundry at least this one are open source this funnel might be a bit uh better for simple tests and for like you know ease of useful uh like the first invariant because they are integrated within the compilation framework but in the long run they might not be as powerful as a Kinder simply because we have you know user Kinder for a couple of years and we have tuned it you know where that it provides the best value that we can do I'll get finished okay sorry um yeah okay so I hope you enjoyed the workshop um we have more exercise in building secure contract something that I would recommend for you is to try to write invariant you know in your next project and actually who is going to try again now on his next project nice and thank you [Applause] So today we're going to talk about storage proofs I want to introduce this app yes I'm gonna present you storage proofs and explain why they're cool how to work with them why you need to link to work with them and yeah a bunch of other things why is it even possible all the complexities behind the trade-offs and so on so a few words about storage Crews why I really believe that they are cool especially uh nowadays so might as this is that ethereum is pretty sharded nowadays and with storage truth we can essentially read the state in a almost synchronous manner which is a pretty pretty nice thing to do given the circumstances um yeah and maybe also let me explain why is it even possible so story is essentially this idea that the entire state is committed in a cryptographic manner um using some data structure like Miracle trees Marco Patricia trees and so on um and yeah we can essentially verify any specific piece of State at any point in time on any domain which is pretty nice and does introduce additional trust assumptions you just rely on the security of like the base chain um so yeah that's like storage proofs tldr where they're cool now a bit of like sponsored section of sponsored sections so uh what we're doing at harvardus so our like goal is to make smart contracts sell for in a way by providing access to historical state uh we like I said might as this is that ethereum is pretty short that nowadays we want to unchart it by using storage proofs and we want to enable synchronous data reads because today we do not have really nice ways to make synchronous data access without introducing New State uh new trust assumptions so yeah that's we do and how we achieve that we achieve that by using obviously storage proofs we use snark Starks and NPC I will get why we even use all this tooling but first a few words about storage rules what these are and and so on it's so tricky actually I I need to be multitasking okay so uh what we're gonna cover in today's Workshop so all the basics required to like understand properly this primitive how to like work with it uh how you can generate these proofs why they're pretty useful and how actually you can access this commitments I'll get later what we call the commitment in a process manner and how we make smart contracts software and enable historical data reads cool so um it's pretty that's pretty tricky so about the background that I want you to have for this Workshop so we're gonna like start from the biggest Basics so what is the hashing function just a very quick reminder I hope it will take less than a minute uh like generalized blockchain Anatomy how I ethereum header looks like why ethereum they're not like pretty on only like ethereum focused uh however I think that for the sake of this Workshop it's the best to like present on this concrete example Miracle trees explain me like on five I will just quickly explain the idea how it works and what is America Patricia tree without really going too much into digitals um yeah finally no not finally uh the anatomy the ethereum state it's pretty important to like deal with this uh with this primitive and finally how to deal with the storage layout cool so touching function essential is this idea essentially it's this idea that I can have a function that takes some input of any size and it always always return an output of a fixed size and now what's also important there is no input there are no two inputs that will generate the same output and you cannot reverse the hashing function so it means that given the output you don't know what is the input and this is not what we call like Collision resistance pretty useful primitive like used in blockchains uh I will and I think that's that's pretty much what I assume that everyone is like familiar with like yeah okay why is it important um so generalized blockchain Anatomy so why we call it a chain because we have a bunch of blocks mined together like linked together because each block contains the reference the parent hash and the previous header contains the reference of the parent hash which is pretty cool and let me remind what the hash the parent hash or the block hash of uh on ethereum is it's essentially the hash of the header uh pretty important to deal with this Primitives and make smart contracts software so accessing six Oracle state do you just keep that in mind let's get to the next part so um no ah I think I'm missing one slide no it's the correct one okay so uh this is an ethereum block header uh as I said we're gonna go through the example of ethereum concretely so a bit of anatomy so to access State obviously we need the state route what is the state route is the root of the miracle Patricia tree of the ethereum state we also have the transactions rule which is pretty useful if you want to access historical transactions like their entire body and receive truth so it's really useful to access any events logs and and so on and all of these are like root of the American Patricia tree America Patricia 3's America 3 just think of it in that way and most importantly we have the parent hash and with the parent hash we can in a way go go backwards I think that's it let's get to Miracle tree so essentially it's this idea that I can take whatever amount of data and I can commit it in a cryptographic manner by using this data structure so on the left side we see a standard Merkle tree so essentially all the data goes to the bottom and we essentially hash it you know what the hashing function is then we combine these two hashes together with hashtag we keep doing that until we get to essentially one hush and this is what we call the root mark up to three shot three modified Miracle Patricia 2 to be exactly the data structure that we use in ethereum um what you see here I hope you see on the top we have the state route and essentially the state route is the root of this tree and now how it works and how you should think of this of this it's a pretty complex data structure I don't want you to bother with it today but essentially we have three types of like notes we have Leaf nodes extension notes and Branch notes so Leaf nodes contain data Branch nodes contain data and extension nodes like on the high level just help us to like sort of navigate in that tree but to be honest to deal with storage truth you don't really need to understand this part but to like build on the low level as we do obviously we need to we need to do pretty pretty a lot with that with that part okay so ethereum State how is it constructed most important takeaway it's a two level structure so I mentioned that the state route is the commitment of the entire state but it's not really true because ethereum is a does it still okay it works it's uh it's account based um and essentially the state route is the commitment of all the accounts that exist on ethereum and what an account is made of it's made of a balance like the if balance it's announced transaction counter storage route the storage route is like the root of another America Patricia tree and this America Patricia 3 contains the key value database that holds like the mapping from storage key to its actual value and finally we have the code it's essentially the hash of the of the bytecode so main takeaway first we access accounts and once we have the account storage root we can access is it's it's the okay um cool so to sum it up like the background so main takeaways given the block stay true to you can recreate any any state for this specific block on this network and given an initial trusted blockage you can essentially recreate all the previous headers which is pretty pretty cool and important to get the ideas that I will explain like pretty soon okay so as it's gonna be a workshop it's a short one so I won't let you code but I will show you some concrete examples so what I want you to like go through with me today is how we can prove the ownership of Alliance profile on another chain so a bit of background lens profiles are represented as nfts and lens is deployed on polygon I think that's it how do we get to this so first of all the question that we need to answer to ourselves is how does Polygon commit to ethereum L1 because if we want to like let's say prove the ownership of a lens profile on optimism we need to know the state route of polygon but there is material one in the middle so how do we actually access this on each terminal one primarily so uh polygon is a commitment commit commit chain and it commits to to ethereum a bunch of things every some amount of time and essentially on L1 we do not validate the entire State transition but we just verify the consensus of polygon and this checkpoints how they call it essentially contain uh State routes and so I mean not directly but we can access them and let's get to this to this part so this is taken from polygons documentation and this is how a checkpoint looks like so as you can see the checkpoint is made of a proposal so who proposed The Block start lock and block give me a second I'll get to this and most importantly we have the root question so the root hush is essentially a Merkle tree not America Patricia tree that contains all the headers and which headers the headers in the range of start block and end block cool so now if we get back to the previous part we can essentially prove with this commitment that we know the valid state route of polygon first even block okay A bit of Hands-On so we want to prove that I own a lens profile on polygon forever so number one we go to the contracts we see a contract we go for it and we see that essentially there is a bunch of logic on top of this erc721 this is like the basic erc71 as you can see it's an abstract contract and it's slightly modified instead of having like a standard mapping from like token ID to its owner we have like token ID to token data token data is a struct distract is 32 bytes in total 20 bytes is the actual owner and the remaining 12 bytes represent one the token was minted okay but how do I actually prove it oh and also very important thing when dealing with storage layout we have something that is called like slot indices so each variable has a given slot like in the some sort of meta layout I call it like that it's from the right way anyways this mapping it has like the slot index too I will get to this part in a second why it's two and we have a mapping from token ID so you win to 32 bytes of data represented as a structure just think of it as some bytes okay so uh I guess most of you use heart hot so I'm gonna present on on hard Hut there is a very very cool tool to deal with storage layouts it's called obviously hard hot storage layout this is how you install it it's literally yarn install hardcode storage layout you add one comment to your heart config you write a new script that contains literally eight lines of code you run the script and you get this weird table and what does it what does it really tell you and oh and by the way why this tool is pretty useful as you see this contract is abstract so some other contracts then does it still yeah some countries can inherit from it and obviously why we inherit the storage layout I mean this does this in synthesis can can get more trickier because it also okay so that's it's pretty hard to coordinate like one hand with another hand even though I'm Italian okay anyways um yeah we know this slot in the in the index and that's how we get it we have a column that is called storage slot and as you see underscore token data is marked as two and that's it okay but what do we do with it how do we get this storage key and yeah that's that's it let me check the time okay um so a bit of Hands-On how do we get the actual searches it sounds scary and it's meant to be scary so we know the slot index the storage index I want to prove that it's like 0x35 owns with ID 3594 how do we get the storage key we essentially do this operation so we concatenate the slot I mean the key in the mapping which is 35.94 because this is the token ID as you know we have a mapping from token ID to token data token data contains the old okay so we concatenate this with the storage index we hash it all together this is the storage key that we have if you're interested how to deal with it for like more complex mappings and like layouts back the solidity documentation it's explained pretty well so now that's to make sure we got the proper storage key let's just check it how we can check it super easy let's just make a one liter PC call to get this storage at some specific key please if get storage at so the parameters we want to access the storage of what of the lens Hub lens cap is a contract that essentially is the representation of these profiles and its address is 0xdd4 and so on and this oh is it better oh it's much better and this is the the storage key is 0x1 so essentially that's the hash the 2E got and the result is 0x000. and we know that it's 32 bytes of data where we have 20 and 12.

so let's split it into 12 and 20 bytes and what we have is some number like you can see Zero x a lot of zeros then 62 till D and this looks like a small number so apparently it is a timestamp and the second part is like 35 7 and it's literally our address so we got it correct we have the proper storage key cool foreign but how do we actually get to storage proofs so blurb standardized method in like the Json or PC standard for ethereum clients and this method is called eth get proof which essentially given the contract address so I'm better call it account address in this specific case allows us to generate a state proof and the last argument I mean the sorry the second argument is an array that contains all this Storage storage keys that we want to prove uh there is another argument which is 0x1a it's essentially the block number for which we prove the state um yeah let's call this method oh by the way uh you might have a question how do we deal with this method on non-evm chains because for example on some specific Roll-Ups this method is like not supported actually it's not a big deal because if you think of it we just need the database and on top of this database we can literally build this method we just need to know how the storage is constructed okay this is the proof it looks scary it is scary this entire object is four kilobytes of data and now I mentioned before that the state is like a two level structure first we have a proof for the account itself and then we have the proof for the storage I mean for the actual storage slot it is scary it's meant to be scary one proof is like more or less 600 bytes 700 bytes it really depends like bigger the storage is than bigger the proof is and also more accounts we have than bigger the account proof is so that's a lot of cool data if um if you can imagine you can imagine uh and yeah that's that's pretty bad why because we need to pause this proof on the Chain so it's a lot of cool data but okay let's let's try what's going to be the cost on like an evm chain that's the cost it's like 600k of gas that's a lot that kills almost every single application that you want to build on top of this nice primitive so it's pretty bad and why is it that bad so I explained on the high level what Merkel trees are America Patricia trees are on ethereum we use Marco Patricia trees and essentially there is a trade-off that when using Miracle Patricia trees the proof is a slightly bigger it's like harder to decode it because actually we need to do some a bit of decoding there um but we need to do less hashing so this is a trade-off but depending where we actually verify this proof it might be more feasible to verify like prove that is based on record Patricia trees or Miracle trees okay but there is a solution and the solution is what if we snarkify such such a proof and we verify this proof inside the Stark why is it cool because we can like let's say that I'm gonna verify this proof inside the craft craft 16 circuit um and yeah the verification costs more or less like 210k gas the proof is like way less than 600 bytes so it's good so essentially get rid of the cold data because the proof itself can be the private input to the Circuit um yeah we can like use multiple proving system depending on the on the actual use case and now why is it like very very cool so first of all it removes call data second model it allows us to deal with very UNH unfriendly hashing functions or the evm is the ones that we don't have pre-compiled for like let's say Peterson um so it might be like super expensive to verify such a proof on the evm because first of all that's a lot of cool data and the hashing function is pretty like unfriendly but what if we can like do it inside the snark and just verify snark and yeah so another benefits this really really helps in obstructing the way how we verify this proofs because you don't need to have like one generalized verifier for each type of of proof but you can essentially obstruct it behind behind the behind the snark which is which is great uh these numbers were taken from a very nice article written by a16z like a bunch of uh a few a few months ago um yeah and I think that's pretty much it let's get to the next slide so synchronous cross layer State access so how can actually a control deployed on some layer access the state of another L2 or L1 so I mentioned that we always need the state route but because all of these systems have a native messaging system we can send the small commitments like for example the blockage to like L1 usually it goes off-road one and and yeah we can like enroll it or send the state through directly and also we don't need to rely on messaging but we can for example uh rely on the fact that polygon is like a commit chain and all these Roll-Ups like commit from time to time they're like batches and and so on so this is like pretty important and we sort of can get the commitment from which we'll recreate the state directly on on another one and then send it to another um so if let's say polygon commits another one I can send this commitment then to start and I'm starting to do their actual verification cool so now how do we actually do that so let's break the entire flow into like smallest pieces so the flow is the following we need to have access to the commitment which is either a block hush or a state route and again we can get it or I either by sending a message relying on the fact that is this chain commit so in a sense it's still a message we can relate in an optimistic manner or we can go even more crazy and verify the entire consensus okay so this is Step number one we need to get the commitment step number two we need to somehow access the state route so the commitments of the state from like a previous block or the actual blog because keep in mind that these commitments are only block hashes and with block hashes we can recreate headers but we cannot access the state okay so once we have the state route we obviously need to verify this state storage groups okay and there are multiple pictures to do that all of them come with some trade-offs and let's go through all these approaches so approach number one messaging so I can send the message from let's say optimism to Eternal one I can get the optical I can get the blockers by just calling the proper op code and and I get it take some time but still I get it this is approach number one so we rely on the built-in messaging system which is I think Fair because the security of it is equal to the security of the roll up and if you're deploying an application of the scroll up it's a fair assumption to do so um yeah it doesn't oh they don't know about the downsides so the message must be delivered so it introduces a significant delay especially when dealing with the withdrawal period in the in in the middle uh and it requires we it requires interacting with multiple layers so first you need to send a message and then actually you need to consume it so it's it's not ideal but the trust assumptions are pretty occasional another approach consensus validation by the way this like Gremlin is supposed to verify a bunch of BLS signatures I I hope it's self-explanatory uh okay so maybe a few a bit of an intro um right now we have POS as the native like consensus algorithm on ethereum which is pretty great because verifying the consensus is finally doable because before like verifying the hashing function eth hash which was used for proof of work was very memory intense so not possible to do inside the snark um on chain directly so it was almost impossible to do so um so now we also have this Workshop called lmd ghost which is implementable but doing all of this like directly is pretty expensive so we need to ideally wrap inside the snark but there is another downside so a few words about the trust assumptions you well you verify the consensus directly so it's it's fine he do you introduce any trust assumptions not really but the biggest downside that generating the proof actually takes some time so to be honest this approach is feasible but comparing to messaging like quite often is like almost the same and you pay a lot of improving time and requires like having more advanced infrastructure okay last approach that we actually use is something that we call like an optimistic relator based on NPC MPC stands for multi-party computation maybe before I explain how it works let me explain the the image I hope it's self-explanatory so it's an NPC protocol we have multiple parties it's multiple parties attached something then we have an observer that can challenge it and then we have finally the commitment given to a specific chain in this case start net once everything is fine how does it work so we have a set of trusted three layers validators however and they attested a specific commitment is valid so how does it work if we want to get the commitment acreated block hash of block number X on startnet then instead of sending a message that will be delayed with a like slightly delayed we can essentially make an offshing call just get the latest one and essentially relay this message directly to start net but it comes with a few downsides because while we introduce some trust assumptions uh but still it's okay okay how does it work so it works in a way that we have a bunch of off chain actors who essentially make this calls and it works more or less like a multi-seek but the reason why we have NPC is because more validators you have than obviously more Securities but more validators you have in it like standard multi-sig approach you have more signatures so more in a way decentralized it is then it's more expensive to verify because you need to verify multiple signatures and you need to like pause the signatures it's a lot of cool data such approach is not feasible on chains Oracle data is expensive so at one optimistic rollups and yeah okay so how does it work uh what is uh actually NPC part doing the MPC part is very simple it's essentially signing over like a specific curve some specific payload and the payload is the commitment itself and that's it okay so this is how we actually attest but now how why this approach is called optimistic and why it's still secure so first of all we just posted some something on the actual L2 and as you may know we can send messages from L1 to L2 and such a message can contain like the proper commitment so essentially even if the validator set will lie L1 will never lie so you can just challenge such a message and now to participate in verifying this validators it's super easy because literally two RP sequels one call is gonna check the actual commitment on the actual chain and the other one checks like what is the claimed Commitment if you disagree you just send a message it costs roughly 60 K of gas and that's it everyone can do that um and again the fraud proving window is pretty short because it's essentially how long it will take to generate like the proof of consensus if it's possible or how long does it take to deliver the message and what is pretty cool in this approach it's not gas intensive we verify just one signature so that's about this approach let's make a recap and let's identify the trade-offs so we have three approaches the first one is messaging the second one is validating the consensus and the third one is having this optimistic layer so I categorize it in four categories the first one is latency the second one is the gas cost the third one is trust and the last one is what is the off-ching computation overhead why do I even list it because if we do some sort of proving then obviously it takes time because we need to generate the proof so messaging in terms of latency we are quite sad because well the message needs to get delivered so once the message gets delivered to some specific L2 L1 will be able to generate already new block so we don't have like access to the newest values in terms of gas cost it's not bad but it's not perfect because we need to interact with two chains at the same time so first we need to send a message and consume it in terms of trust we are pretty happy because we trust the roll up itself and it's a fair assumption option computation overhead we're very happy because there is no computation to do off-chain verifying the consensus so in terms of latency we are side because we need to generate the proof that we've done it it takes a bit of time in terms of gas cost we are I would say sad because we need to verify the actual ZK proof which is way more expensive than just consuming a message or verifying a signature in terms of trust we are happy because we verify the consensus itself and computation overhead it's significant right because we need to generate the proof Final Approach this optimistic layer so in terms of latency we're happy because we simply make a claim and we post it on the other chain that's it gas cost we're very happy because the well we just verify a signature in terms of trust well we are not that happy but also not that sad at the same time because it still can be challenged in an optimistic manner using a fraud proof computation option computation overhead are pretty happy because we participate like an MPC protocol so essentially the overhead comes mostly from communication not computation itself cool so this is part number one these are the three approaches obviously I'm not gonna say which one is the best because all of them come with some trade-offs um okay accessing the headers I hope it's self-explanatory because we literally unroll something from The Trusted input and The Trusted input is again a block hush for a specific block X and if you follow the initial slides that's essentially each block we given a blockage you can recreate the block header and knowing the block header we can access the parent question by knowing the parent hash you can recreate the previous block header to essentially go to the Genesis block so given this very small input we can essentially unroll the state or whatever was present on the chain from this block till the Journey's block okay so as I said I'm gonna explain everything on on the example of ethereum and today all the block headers together are like roughly seven gigabytes of data so it's quite a lot but okay this is how we actually do that this is the high level concept and what are the approaches so the first one we call it like on-train accumulation so essentially we do this procedure this computation directly on the Chain so we provide all these properly encoded block headers inside the call data and the blockers that we might receive as like The Trusted input by sending a message relaying it in optimistic manner or validating the consensus and yeah like recursively go through all these headers and and verify them but there are many many downsides because first of all it's very cool data intensive it's very computational intensive and now we can store all these headers on the actual chain but you know even storing on an L2 storing 7 gigabytes of data is still a significant cost because the state on an L2 is reflected as call data on L1 so it's still expensive either way but the cool thing is that I have direct access to like State router or anything that I want to access next approach is unchain compression so we can still use the same approaches previously so literally unroll it and process this seven gigabytes of data but instead of like storing then we can just update the miracle tree it's a nice approach but comes again with a few dump sites it's very computationally intense because if we have like millions of headers we need to perform millions of hashes on the Chain that's that's expensive but at least we we save on on storing data and also we need to update the miracle tree which is which is another cost um last downside is that we need to index all the headers that have been processed why we need to index them because if I want to up the access a specific block header I need to provide a miracle tab because as we update the miracle 3 and we just store the root in the contract itself then I need to know the path right so I need to index the data and essentially once I it's the moment that I want to access it I need to provide the miracle path this approach is okay it's I wouldn't say way better than the previous one but it's way cheaper last approach so there is a very cool primitive called Merkel mountain ranges love it and the idea is let's do the same that we do previously inside this Arc so we can provide this tremendous amount of data as a private input to the circuit and essentially do the same computation like unrolling inside this record itself and now we have a public input which is the blockage so essentially the commitment from which we unroll it so the trusted input the public input can be literally asserted when we do the on-train verification and why we unroll it we can accumulate inside the miracle tree or American mountain range why American mountain range is is cool because well let's imagine that you want to have like seven gigabytes of data processing one star like the proving time is going to be horrible and why would you even like prove this commitment for like the entire history like do you really need that probably not so let's chunk it like into smaller pieces and Miracle mountain ranges are pretty cool primitive that allow to do this to do to do this to give you like a bit of intuition how how does it work it's essential think of it as a tree of trees um yeah so once we do all this proving like of chain we simply verify the proof on chain as you know like refine the proof is is way cheaper than doing this directly on the chain and still we just provide a miracle path and that's it we essentially have access to any sort of data we want let's do a recap again so approach number one on the accumulation on chain compression of chain compression three categories prover overhead gas cost storage cost actually gas costs should be computational cost okay so prover overhead on-chain accumulation do we prove anything well not really so we are happy answering compression well we still like need to update the miracle tree I think actually there is uh there is an issue here so I'll just skip this part after in compression you're very very sad because well we need to prove actually significant computation so the proving time is significant okay now in terms of gas cause the third approach is horrible because it just costs a lot because we do the entire computation engine compression well we're a bit happy because we just do a bit of computation but still it's a lot of cool data a lot of computation but at least not so much storage storage cost uh oh sorry gas cost in the second approach while we just verify approved so it's cool um okay storage cost for the first approach well seven gigabytes of data it is horrible so we are very set on chain compression uh sorry storage cost for launching compression we just the root of the miracle tree so we are happy and in the second case we're even more happy because we again we just essentially keep updating a tree and we don't even need to post a lot post a lot of cool data because the cool data we passed is literally just the proof so we're very very happy but again I don't want to say that all of the one of these approaches is the best one because as you see there are trade-offs and yeah so this part is actually pretty easy so as you know as you may notice here I was explaining like the second step when it comes to two linguist storage proofs and now there is the the last part which is essentially verifying the proof itself so approach number one is verifying the proof directly on the Chain approach number two let's verify the proving side the star can then verify the Stark approach number three let's verify multiple proofs inside the snark and then verify the snark we can aggregate multiple sharks together and so on but obviously there are some trade-offs especially when it comes to proving time um and yeah so now why the first approach is feasible on on ZK rollups for example on structural data is very cheap and what we want to avoid in this specific processes called Data so this approach is for example feasible on starknet but for example if you want to verify like a proof on optimism or a collate is very expensive you want to reduce it as much as possible so for that reason you might want to use a snark and finally if you have like many slots that you want to prove why can't you just verify them inside one snark you're gonna pay improver time but you just present one proof at the end so this approach is cheaper is the cheapest one but only if you have multiple actions to to take so there are trade-offs so let's identify them categories approver overhead latency verification cost so verifying the proof directly prover overhead doesn't exist latency doesn't exist because we don't need to prove anything verification costs well it is significant because we need to post School data and we need and we need to do the actual computation so like going through the entire path and each step in the path is one hashing function oh and also let me get back to the previous slide I forgot this is very important why wrapping inside this wrapping inside this Arc is pretty important if you're like dealing with a storage layout that is using a specific hashing function let's say for example Peterson Peterson is not available like on on the evm like you just need to implement it's not the pre-composed it's gonna be costly but if you do inside the snork and Peterson is pretty smart friendly it's not friendly then well it just verifies in our control one and you abstract it so it's going to be way way way cheaper but again there are trade-offs let me get back to this so I went for this the normal competition 3 star Cricket fight proof through the overhead it exists so we are not super happy latency you're also not happy because we actually need to spend time on improving this this thing verification costs we are happy because well we we just verify your proof so it's fine and it's an artifying multiple proofs the prover overhead is still there latency is still there it's even bigger because it takes a bit longer in improving time and verification because we are super happy because essentially we can mutualize the cost of verifying multiple proofs by just verifying one single Stark proof okay went through quite a lot of things let's put this all together so let's imagine we have three chains and we want to have interoperability interoperability between them so we have chain Z chain X and chain y so it all starts with a message AKA commitment we send a message in order to get the commitment so let's say that we send a message from chain Z to chain X because on chain X we want to access the the state of changing so what do we do once we have the commitment we literally recreate all the headers using one of the three approaches and once we recreate it the header is still the point for which I want to prove the storage I just verify a proof and again for verifying get proof there are multiple approaches but now let's say that on chain y I want to access the state of change Z and there is no direct communication between chain Y and chain Z so it must be routed through trainx by the way I'm like talking about this in a pretty abstract Way by Chain X I just mini room later one um yeah so from chain X I'm just gonna send again the commitment about change the as a message and then simply recreate all these all these headers as you may not notice it's pretty redundant because we perform the same computation on two different chains and we don't need to do that especially if you use like the third approach which is generating the proof on chain but now there is another problem how do you actually know what you should do like you need to be somehow aware of what is happening and for that reason we introduce an API we don't expect like developers to deal with all that complexities choosing the right approach for the direct thing essentially right now our apis optimizes cost wise soon we'll be able to optimize latency wise um and yeah and essentially that's it um just about our API I highly highly encourage you to check this out um and yeah like a few final words about the API it acts as a coordinator it optimize the costs it optimizes the cost because we can batch multiple things and once the job is done we get a notification like via webhook VIA an event like whatever you want so essentially you're not you don't need to be like a infrastructure maintainer and you can just focus on essentially building on top of this primitive and I think that's it um questions so the API essentially is a rest API for now we also have a Json interface we have option function entry points so we can request the data like by making enough jingle like calling a rest API or like calling a Json or PC method or if you're a smart contracts like wants to access this data then you just submit an event we're gonna catch the event and later on like after a bit of time fit this uh the specific data inside the smart contract so we have like a bunch of interfaces and by the way speaking of like the off-train entry points once the entire leg work is done on our site you can get a notification it can be like a web hook we can like send you a bit of information like using a websocket uh it can be essentially whatever whatever you want foreign oh yeah so uh that's actually a great question so different chains use a different like storage uh I would say architecture they might commit to America Patricia 3 Miracle 3 uh maybe even vertical tree and obviously like I said having a generalized verifier it's like pretty it's not a clean approach so we essentially abstract it but by using a snark and inside the snark itself we just do the proper work like you know you go for the for the tree like for the for the um through the elements of the proof and then we can like use a specific hashing function so for example now Poseidon is Poseidon is uh is is pretty popular um I think that scroll uses Poseidon and also SDK sync uses Poseidon on the avian like performing Poseidon will be pretty expensive so for that reason you cannot verify the proof directly but what you can do you can do the entire verification inside the snark and then on the one you don't really care about the Strunk is like doing you just just verify it so that's how we actually did it deal with it if we need to have it abstracted we have it abstracted if we don't then we just don't foreign oh yeah oh yeah that's uh that's actually a good question because I think I went super technical uh so actually what we do at Herodotus every two weeks we have some internal hackathons and right before the merge uh we built a proof of concept that we called merge Swap and essentially we allowed anyone to dump their proof of work if on proof of stake and the way how it works would you literally build the bridge on top of this technology and the bridge Works in a way that you can lock your if proof of work inside a smart contract on if proof of under if proof of work chain you can prove that you've done it on ethereum proof of stake you can once you the proof is verified you can meet the erc20 token and you can do whatever you want with this token and then if you want to withdraw back to if you're in proof of work you just burn it you prove the fact that you burned on the other side and and yeah that's it also in terms of other use cases I think that cross-chain collateralization is pretty cool because this is the place where you want to avoid latency as much as possible and you want to be asynchronous as much as possible and essentially that's that's what we do here because our latency comes only from from the proving time but again using some optimistic approaches and so on there a lot of things we can do cure I hope it answers the question okay I think that's it I have like three minutes so I guess we can wrap it up and yeah thanks