Jan 2023 Online Event: Scaling Formal Verification to Find Bugs in Complex Smart Contract Systems.

okay so uh we are now recording uh first of all uh welcome everyone to um to another session of if here online workshop and uh this this month we are very proud to have uh mulik and Alex from the Satora team uh and thank you so much guys for doing this and um another note from uh from the speakers is that if you feel free to ask any questions along the way just admit yourself and uh we will see how it goes if it gets too noisy uh I'll moderate but uh in the meantime feel free to admit yourself and uh enjoyed it enjoy the talk so uh I guess um money can take it away thank you very much g i it's lovely to be here and to talk to you guys uh I've been working on on this domain for quite a long time but I think this is a first time because basically with the team trying to actually make a tool that everybody can use and actually this tool you will see later a demo it's a tool for securing your code it's already prevented billion dollars mistake and you are welcome to try the two so uh wait I don't know along my screen so uh our team we have actually assembled this is a tool which has a lot of Technology coming from formal methods which is a topic in computer science and we have many many experts in this domain who are helping us to actually make this tool build these people have PhD from top school in the US in Israel in Europe in many places and they actually they are using their skills to build actually this kind of technology and complementary to them there's some noise maybe question I don't know no okay so there's complementary to the technology we have the the people who are actually the Security Experts who are helping to actually make this tool a real tool as part of checking the code security and you you will meet Alex Joseph basically these are expert in security while actually making this tool into a product that everybody can use uh I'm sure I don't this is not useful to you but I want to point out that a lot of bugs in the space of crypto happens due to coding mistakes and these are few bugs but there are many more everybody knows the Norman Bridge which is a small change in the code also compound a governance which is actually also a small change in accordance compound governance is interesting because they actually ask a customer of Satora but somebody have changed the code without using the setup book so the idea is basically the you are you can have a lot of mistakes in the code and and this is something that Serato is trying to perfect so Satora is not the only tool there are different kind of Technologies to prevent bugs or to find bugs before the code is deployed all of them are useful let me point out high level the the tools so the first technology that you can use is basically test or even you can have automatic testing called fuzzing that you basically try the in the tool on many many inputs and there are techniques like in the in the area of General code with the American fuzzy loan and for smart contract basically they're using kidnap which is a tool by 12 bit and there is Foundry which is by Paradigm and community so these are fuzzing tools they're basically doing testing that you can do before the code is deployed this is very useful to basically try the tool and many inputs uh it is easy to use the problem is this kind of technology is coverage that if you have a bug which is very very hard sort of deep bug The Logical mistakes it's a bit harder to find with this mistake with this technology the other technique that is useful and has been around also in the computer science for quite a while is static analysis so static analysis this is the idea that you basically check your code you are you are doing some some search big syntactic or semantic to check your code there are industrial tools like coverity uh uh vehicle check marks white sauce in the area of blockchain it's a it's a smaller domain there is tools Leader by 12 bits which is check the code how many of you know slither uh everybody is muted so me I know okay good so Slither is a tool for smart contract and and and usually and there's also other tools in these domains so topographer also has specialized static analysis the power of static analysis is the Precision basically because these tools are not aware of what you are doing it's actually they have very high level of positive and false negative and we are seeing it and many people have seen that sort of the limit of this kind of Technology the cell technology and this is what we're going to hear today this is the shutter approver it's called automatic formal verification sometimes it's referred to as deductive verification so the idea is that you are checking your code not on your initial state or an arbitrary State and the way you do it you essentially compile your code into a mathematical formula and then you solve for the mathematical formula to find the box and this is a technology which has been around there are open source tools like Daphne smt checkup by the Italian foundation and cbmc but the idea is that software approval is another technology it checks the bytecode the difference between that and the academic tool that it's more scalable and you can see that it actually runs on much larger code the the problem of the former of the automatic formal verification because the computer is it is good in necessary to give you a very high coverage but because the computer is is ultimately limit there is a question of how how expensive it is and and this is what the central team is trying to do make this technology we and the first technology which is also existed is called proof assistant so both assistant is the idea is that not instead of the the computer the human is the loop so you are writing your proof as a part of your proof you are actually extracting the code so basically for example you're not writing your code in solidity you are writing your code in K on Coco and other technology and then you can from it you can derive probably correct score people have used it in the past for compilers in the area of of smart contract there is a company right verification that that person this uh the the think of which is the limit of this technology that the effort is very high because you have to really uh really understand basically the mathematical properties of your code and from that you derive the code usually the way program will work is not this one the program before and then they verify so this actually requires you to fit in a different way that that you what you normally book so just to give you an example to motivate you this is slither running on a very very small contract called bank and you see the red lines it says these are mistakes that this little uh reported and you see a sweeter reported several bugs does anybody want to guess how many of them are real so there are a few bugs here do you want to guess um probably none no yes because later always give us like a false uh positives exactly exactly that's so that's exactly the problem none of them are weak okay so just sort of giving you the idea sort of explaining you this in a more graphical way you see here this the idea is that the you have on the left hand side you have this powerful tool Isabel Daphne this is very very powerful but it's actually very hard to use on that on the other hand you have the thing which is easy to use but not as part of the kidnap the meat and what is trying to do is build something in the middle and you can judge yourself where we are so the idea is we want to make it almost as expensive as expressive as com and we are not nearly there but Coke is a very explosive tool which is open source so but we want to lead by Microsoft which is also very powerful but we want to make it easy to use almost like like beach wheel or kidnap it's not it's a bit harder but we want to make it almost as as easy as as this kind of fasting tools and one key idea is that you write the spec in an easy way and you will see it uh basically later Alex will show it to you and also another key idea to scalability is modularity if your code is modular this technology will work much better so what does the Torah do we have this language called CBL so it's not a programming language it's a language to declare the properties and it's application specific you declare The Logical mistake and then we have Technologies we have the sector approver this is a proprietary technology that you can use basically by by the cloud to check the code this is automatic form of verification there is a Gambit this is open source it's already available now on GitHub it's an open source for checking the spec themselves so the idea is you mutate the code in order to check the code is actually available already starting last week it's available you can take the GitHub and use it and we are also building four sites we are building a technology that can work this set of approve on on individual transactions so this will give you more coverage because we can check certain things and we can check fix that will not wearing something that is wrong hey what there uh sorry I think someone unmuted themselves and uh sorry about it no way so so we are building three Technologies today I will focus on the first one but the second one I said is already available and the third one we are we are working on but I will focus on the setup code okay so in fact what I want to show you what Alex was showing you too I want to show you the CBL I want you to show you how we write spec and one of the most interesting thing about formal verification is the idea of environment so environment these are properties that actually are supposed to hold in your program it's actually some kind of good properties for example the casino is always we know for in the case of blockchain that you have solvents basically the assets that you owe that you hold they exceed the liability so you're not back up so these are interesting properties and you go back to a restore or in computer science there is dark stuff this is the idea of writing these kind of properties and the interesting thing that Satora based technology that finds automatically finds violation of these properties so let's look into solventy solvency is the most interesting property basically for example if everybody wants to the bank the bank can still fulfill the commitment so these are examples of political that work with Torah and they work with the Satora before the court was deployed but after the odd completed audit and basically the the audit was done by the best auditing field and you see that these are mistakes that were found by the shutter approver after the audit was completed and I think Trident I'll be able to I actually be able to show you later this kind of and you see here the value which could have been lost has this because been uh actually released so how does the sector approval work it takes the environment on one hand this is the CVA it takes the code and the other hand actually we don't have an exhaust code we had the Dubai code but that's a detail and we either give you a proof we give you a mathematical book that all the behaviors of the code are okay but actually the most interesting case that we give you a violation it gives you a violation which is potentially very hard to find and this violation is actually something that says at a certain condition you have some a logical mistake in your core that breaks this kind of thing line unfortunately this is what I alluded since this is a mathematically hard problem the tool is due to fail and sell it then what sir toy is trying to do is to make the technology robust enough so there are fewer failures and that's why we have a lot of people working on that and trying to actually improve the tool and reduce the time up make the tool easier to use a almost like unit test the other usage of this tool which is uh uh basically is is into your build process so we integrate into your build process and every time you change your call you run into and assuming that the environment do not change you run it again and again technology is fairly complex I won't be able to explain but there's a lot of things that is implemented here there is a compiler there is its own representation we have this unique static analysis here which is actually analyze the bytecode but in fact it also checks some environment and we have reported several uh security bugs in the compiler itself that were found found by our technology when we took the environment and we're also doing a lot of things and this is basically what these people which are expert in this domain are doing in order to scale the technology so that the mathematical solving the constraint is easier and this is actually something that we are doing in order to make the tool easier to uh faster to use so let's start with a very very simple example I'll have more examples I will appreciate uh audience so this is sort of a hello where the simplest example of a code you are transferring a balance from one account to another and the environment that we want to maintain is the total is equal to the sum of the buttons do you want to guess if this environment holds or not so this is a very very simple in terms but even there it could be broke do I guess somebody here in the feel free to just unmute and um just give it a shot so of course so you're you're not subtracting the balance from so I so it will uh of course uh so in the second last line so it's never subtracted say it one more time so I I I said that uh this invariant will not hold so it will fail why for what input I mean you are yes okay you are subtracting here and you're adding here it looks like to me okay yeah but if we should ask me before I use the tool actually I would say it's okay it will be right that's the idea I mean usually formal methods is good to find some some behavior that sort of supplies and and the more the complex is called you can get more surprising behaviors so there so here even though so maybe basically let's find the two let's see what the tool found the tool found actually is L is transferred to it to our cell then you see that basically she gained y because the way the code is written it's actually not actually taking care of the fact that if you have the same address and actually even though it's a simple bug people have stole money which is kind of very very simple but okay so that's what is found and if you change the code for example here it's a simpler code that you don't actually use this intermediate result and as a result it can give you a mathematical proof that the sum of the environment before and after is the same so the sum of the environment the sum of the balance did not change so that's the idea so and maybe I can give you a more interesting example which was not found by us it was found by our customer so we have one customer I'm sure you all know making one of the top players in this page so they wrote their own environment and they wrote an environment on the die so that is a stable quantity Implement and they wrote the environment that says it's a stable coin and guess what they have thought actually they've pulled the tool but actually the the tool for the the file that they've improved the environment but the tool found this bar and this is a four year old buck so basically the quote was for you all called and actually they found a mistake and if you look into the mistake it's basically there is a degenerate case in each function that this environment here which the basically it's a stable condensation the sum is equal to the sum that you hold and the the tool found that there is one behavior that actually allows you to violate so this is the thing this is the use of this technology it's a like quality assurance before code is deployed to find interesting how to find bugs so maybe I give you uh sort of a a one interesting bug which is more tricky which was for fun in the Trident and later on Alex will demonstrate how the tool finds it so this is the the Trident Implement what is called uh uh basically this there's a pool with two tokens and and basically it has an operation called band single where you can ban one of the token and this actually had a bug you see instead of using the they actually even not use the correct API so instead of this chord it should be this and what happened is the tool find this plugin it's actually of course the tool doesn't know how to write a code but it knows the environment and it checks the environment and then it finds the violation so let's see what happened and by the way this is a tricky call it's about 2000 line of solidity code and it's 24 lines of evm code for comparison open source tools for example Daphne they usually handle up to 100 lines of code so this is actually you can see here how mature is this technology and also you notice if you compare to Slither and other this tool actually has many many behaviors so it's very very hard to find this kind of bug with spicing or unit test so how does the tool work the tool actually starts in arbitrary stage in which this is the environment that you have that if one of the token is zero the other token is easy so they're either box zero or neither Z and it's once destroyed and you see we have Bob and Alice in the game and basically Alice does something which looks a bit weird she builds a holiday and get too hard to talk and as a result you see the invite is broken and you can ask yourself what's the significance so this is actually was found automatically by our tool but later on of course our Engineers look at it and see and this is of course manual by Head we look into this bug we see the violation of the invite and we try to understand what is the implication and what are the implications of this kind of power so did you see the invite is broken see that now token a is 400 and token b0 so one of them is zero and the other system so what is the implication the application here you see a trace that actually there is the following basically there is a at least deposit 100 talk a and hundred B both deposit hundred and hundred B uh L is transfer uh 200 so now there is a lot uh the lot of token hey then there is balancing and finally Alice walk one token for the rest of the token so Bob is left with nobody so Alice took all Bob's body and essentially this is the behavior which was prevented by the Satora program it's a behavior that will allow you to completely deplete the sushi code and this is what we want to do with formal verification we want to actually uh avoid these kind of uh behaviors so and how does the tool work it looks into a single transaction it looks into a single transaction we start from an arbitrary S10 into an arbitrary State notice that it's very different than fuzzing that you start with initial State this is starting in an arbitrary State and of course this is powered by mathematics it's powered by the ability to reason about about the code in a mathematical way and I'm not explaining this here but this is the idea it runs on this kind of transaction and it checks this purpose foreign you go from a state which satisfies the environment into a state that uh violates the environment so basically this transition start from a state satisfying the environment into a state violated Libra so I I want to actually finish before Alex actually does the uh demo I want to tell you sort of few high levels about formal method is actually a mature things in computer science but we have written a Blog trying to explain what's the issues here many of them actually is not specific to blockchain but some are specific to blockchain so the biggest value of formal verification this is known of course in the hardware in this formal verification is not just for moving bugs formal verification is for BA for finding bugs it's not for proving absence of bugs it's actually for bug finding so basically when people tell you that they use formal verification ask them how many bugs they have found and this is the biggest value of formal amplification is this preventing of battery we have seen the sushi with the maker that the other question about formal verification formatification is a very hard computational problem we have keywords like why stereo and computer science and other theorems that basically say that the computer can never do formal verification but in fact it's of course true these three also too but we think that the hardest problem in formal notification is actually coming up with the environment and this is where Satora tried to come the other thing is that formal verification like any other techniques and other security like auditing or like like like fuzzing like like bug Bounty it's never a bulletproof you always want to do everything and formal verification is a tool for drastically improved correctness and we are seeing with our customers work with formulasification that in fact it does improve the code correctness and it's improves the code security but it's never Bulletproof another thing since it falls in the area of smart contact and D5 there is a standard of using auditing some people think that by they can avoid auditing by using formal notification that's not the case these are two complementary things that work very well together we work with Auditors usually before auditing but we can also work after auditing and the auditor if they work after us they can review our specification because one way that we will miss box is we will not have devices and maybe the last thing about formal notification is formal verification some people want to delay it as much as possible because they see it as an expensive procedure both in terms of human and machines so they say let's make the code more stable before we do formal verification with our experience this is usually a mistake you want to shift security left you want to actually start formal verification as early as you can because first of all it's easier you will find wall bugs and also you'll make the code more amenable to form a verification because that the idea is that when you if you work with it especially if you work with with our tool but either if you work with other people with other tools it doesn't matter you are starting you write this environment even when the code is not feature complete and of course even if you're not using our output you buy a thinking of invite early it's a very very good thing before you even start when you write your white paper you write everything you are you have to to basically write to use use this kind of tool that use inviting balance uh to conclude bug finding is very very hard uh in their smart contract we have Smart contact they are eventually even advising is a good technique but it doesn't find uh many of the errors static analysis in smt which we what we Implement is works better together I haven't explained to you the technology but the idea is that the static analysis actually is reduced as a decomplexity and the S of D the mathematical solving it is introduce the false positive and false negative that you get from tools to forms leader so the idea we are combining two techniques together and in particular we implemented this automatic formal verification that you will see soon see in action it started out because it states and not in initial state it finds tricky bugs and it can also prove high level probability like solvency and also if we do not restrict your programming style so you can write your program the way you want you can write it imperative you can write it functional we can write it object oriented we let you Love the Way You Are so I don't know what the organizer suggests maybe we we so do you want to go to the demo before the Q a or or what what would be better um I think uh generally we are very used to having the Q a after everything so I think we can move on to the demo and afterwards uh we can go to questions because I personally got a few questions already great so Alex take it from here all right thank you and Alex go for it all right uh I'll talk a little bit more about I hope uh I'm Audible uh yes we can hear you yes all right uh I'll uh speak a little bit more about the bug that we found in the Trident liquidity pool platform uh that Molly also touched upon a little bit because it's sharing my screen um yeah so I hope you can see the SIM code here uh uh the the contract that we're trying to verify here is uh it's a very simple classic two token concent product liquidity pool um for those of uh you who aren't familiar with liquidity pools it's pretty Central to the way automated market makers work uh and uh whenever you swap in a text when you from our token to another there's electricity pool in the background that contains both those tokens and EU exchange one uh for the other so this uh contract that we are looking at here is uh one uh search contract uh it has two tokens that it uh maintains in the pool it maintains the reserves for the two tokens and it keeps the track of the constant product which will be used uh when you are trying to swap from one token to the other in order to determine how much quantity of uh token will you get in return for a certain quantity of another token uh this token I mean this contract also implements crc20 functionality uh because every time you add liquidity to this pool it will mint a certain amount of lb tokens and give you those LP tokens uh as a proof of you having supplied liquidity to the pool uh so as a liquidity provider you can withdraw your liquidity by uh burning these LP tokens that were given to you in the first place when your supply liquidity uh so that's a very high level view of what liquidity pools do and what this contract is trying to do and uh before we delve into the spec or the code I want to uh get you to think about security properties uh from the point of view for liquidity provider as a liquidity provider when I provide liquidity to a boon I uh I should be very sure that in exchange for the liquidity that I've provided I should be able to get some proof which is to say that I should be able to get I should get liquid community pool tokens lb tokens which is like a proof that I have provided Liberty and I should always have the ability to exchange those empty tokens back for the for my share of the the underlying uh uh liquidity uh pool tokens uh so that very high level property when we think of that without diving into the exact implementation of the contract uh so we can uh you know transcribe that uh that property that just we just spoke of into a very simple logical expression that basically says that if there's any outstanding supply of uh liquidity pool tokens then uh there should be some reserves to back those tokens it should never be the case that there are LP tokens in circulation but there are no reserves to back them uh and it goes the other way around as well that if there are reserves in the in the in the liquidity pool then there should be LP tokens uh corresponding to those reserves because if that's violated then that would mean that there is still liquidity in the pool but there are no LP tokens to claim that liquidity which means that some uh liquidity provider did not get LP tokens in exchange for the liability that they provided to the pool uh so this very simple intuitive property is uh is an invariant in the system uh and this is what an invariant looks like in uh in the sadora October world where you just State the expression that you want to always hold uh in a code and uh that's that and uh so uh we should first uh without looking at the contract let's first run the spec and see what happens the way we run the spec is uh through a script where we call the call the tool we give it the serenity file specify the contract we want to verify in the file uh we also provide the spec that we want to verify the code against and then we run the uh we we run the verification uh the two things compiled uh and uploaded to the cloud where uh the processing happens uh I will show you what the Run looks like uh without waiting so this typically takes around a minute to go through um without keeping your guys on hold I'll just show you what a run looks like on the left side this is for a typical report looks like for the verification on the left side you have uh this pane where you'll have a list of all the rules that you've run and those rules will have a green circle with a check mark in it or a red circle with a cross in it that says violated which shows you if there's an issue in this case we see that it's being violated the invariant that we just wrote is being violated and when we uh dive deeper we see that it's being violated uh in the preserved state so I'd like to talk a little bit more about how invariants work in solidity in Satora in variants of uh first [Music] um contract at that point uh the state contract is the important um yeah your internet was not so good maybe you can repeat okay um yeah so uh what is the last thing you heard you said and then maybe you start from the beginning I think I at least all right so invariants are checked in two stages the first we uh first the code the contract is deployed and the Constructor is run and then the tool checks whether at this point the state of the contract agrees with the invalent uh and the next thing to do is so the tool assumes an arbitrary state which still uh agrees with the invariant and then the tool calls a function in the contract and then again checks after the function execution as to whether the state of the contract still uh adheres to the invariant uh using these two steps we can buy induction proof that uh the contract if it passes in both these steps then by induction we can say that the contract will always uh adhere to the invariant and if in any of these states it vibrates invariant it means that it's possible to uh to break this environment in this case uh I hope I'm still uh you can still steam ice cream yummy clearly yes we can see the tutorial.com website all right all right so in this case when we uh when we click on the invariant we see that it's uh following it's failing in the preserved state which is the second stage uh after the construction has happened and you you assumed in arbitrary starting state which at least with the embedded and then you call the function and then check again uh where the theme parent still holds if this is that state we click further and it shows us a list of uh functions that were called and in this list we sh we see that there's a function called burn single which is failing uh now let's go back to the code and I'll tell you a little bit more about what the code is doing so as I said it is a it's a classic two token liquidity pool where you can supply liquidity in exchange of that liquidity you get LP tokens which you can again burn at any point and get your liquidity back so the way you get your liquidity back is by burning your LP tokens typically or the way it works in a liquidity pool is that uh when you burn your liquidity pool tokens in exchange for correct the contract will give you a certain number of each of the two tokens in the pool and that's basically your share of the liquidity pool in that time but in this contract there is a special there is a function of special interest to us which which is called burn single this takes that burn functionality to a little bit further where it allows you the convenience of withdrawing your liquidity in not two separate tokens but one single token so it saves you the uh the hassle of then uh swapping from one token into another after you've withdrawn your liquidity so the way this function works is that as as parameters it takes three parameters one is the token that you want to withdraw your liquidity in second is the liquidity that you want to burn which is basically the number of LP tokens you want to burn at this point the third is the address of the recipient who is supposed to get the liquidity which is which will be withdrawn uh so what it does is that it first fetches the current reserves and the balances of the contract for both the tokens and then it calculates your share of the the liquidity pool which is supposed to be paid out to you now the way it does that does that is that it looks at the total Liberty that liquidity that you are burning uh calculates a fraction of stat with the total supply of liquidity pool tokens out there uh to get to to understand how much of what share of CLP to the liquidity pool you own and multiplies that with the balances respective balances on the total pins to calculate the amount of each token that is code to you at this point it will burn the liquidity that you've supplied and then it will proceed to convert one of these tokens into the other uh depending on what token you've opted for uh to cash out in and to do that it causes a function so so it basically needs to now convert one of these amounts into some amount of another token for which it can it calls a function called a get amount out if we look at this function uh we see that this function receives three things it receives the number of tokens that need that the user wants to trade out of and it is a and it receives the current state of the of the liquidity pool which is the the reserve amounts for each of the token after the withdrawal has happened uh and it calculates the amount as such here and uh now let's go back to the call Trace and see what's happening here so so when you click on uh the the violating function here uh the tool will show you a call ratio which is showing you a detailed uh flow of the execution that the uh that the tool went through uh when it found this uh this counter example that violates the invariant so we see that the assertion which is checking the invariant this assertion has failed and we see that the reserves uh have gone down to zero for token zero in this case so uh so clearly there are there's a total Supply still there for token zero but it turns out the results have gone down to zero so let's find out how that happened this since this happened in The Preserve state it happened when some function was called and we know that that function was the burn single function and we see that the burn signal function was called with these these parameters where we've specified that the token is 2714 you can see the two tokens that we are working with uh that the tool is working with here are 2714 and 2710 uh I should also tell you that the typical report has three different panes the one on the left shows you a list of uh rules uh which you can uh dive a little bit deeper into to see exactly which functions are failing in the role of the events that you're trying to take you're trying to test uh the central pane will show you a detailed call Trace yes and the pen in the right will show you uh values of the variables that a tool is working with and it will also show you any call resolutions uh with respect to calls that happen to external contracts uh so yeah so we see that the two tokens that are in the liquidity pool are 27142710 and uh I'll take you back to the code so you can follow along uh easily um so so when they get amount out function is called we see that uh sorry I'm checking the wrong place yeah so we've we've pulled we've checked what the current reserves are what the current balances are and the tool that shows us that the the random state that it had started from uh in that state the reserves for the two tokens are five and seven and the balances are five and thirteen and the total supply of the LPA tokens is uh 744 uh and the liquidity that the current uh user the liquidity provider who's trying to withdraw liquidity uh the liquidity held by that user is three EB uh as opposed to a total supply of 744 now when uh the get amount out function is called uh we are saying that uh the amount that we want to swap out of uh is seven tokens of uh token two which is 2710 and the current state of the reserves of the two contracts and this is where we first see a problem we see that the current state of the con of the pool which is after the uh the liquidity has been pulled out uh it turns out that one of the reserves has gone down to zero and when you look at the execution when you look at the calculation that happens in the get amount out function you see that if the reserve amount in uh parameter this is supplied as 0 then the output is basically the reserve amount the entire Reserve amount of the token that you want you want to pull liquidity out of and that's exactly what's happening here uh the liquidity amount returned here uh which is three this this and the the amount that was calculated for uh withdrawal for this token which is token one uh which was two which we'll see later uh three and two together is five and that is what is being transferred out to this user in The Next Step where we see the transfer function being called the transfer function is being called and we are saying that the total amount we pulled out is this which is the entire reserve for token uh token 0. so at this point uh uh so the tool is basically telling us that it's possible to get into a state where uh you can draw the entire liquidity out in theory if the person who's withdrawing the liquidity has to pull out the entire reserves for a token then that person should basically have all the lp tokens in circulation that person should should be holding 100 uh shares of the liquidity pool but uh in the call Trace we can clearly see that the total uh liquid the total Supply is uh uh total Supply is 744 and on LP tokens held by the user was clearly smaller than that so how did it happen that uh user with a smaller with a share less than 100 is able to withdraw the entire uh reserves underlying reserves for a token it happened because uh the amounts that are being calculated here are being calculated on the balances and the tool shows us that the state that it started in the balance uh is not necessarily the same as the results in fact the balance for one of the tokens is uh significantly higher than the reserves that the contract is tracking and uh so what's happening is that your smaller share of the liquidity pool is being uh multiplied by an inflated number which is the balance here which is giving you an amount which happens to be equal to the total reserves of uh that token and so uh when you can when you call the get amount out function uh the reserves the updated results that you are specifying to this function happens to be 0 for token 0 because you've basically subtracted seven from Seven you've calculated and uh inflated value that is owed to you and that is being subtracted from the resource and uh that zero value then leads to the calculation that allows you to drain the pool of the entire liquidity available for token zero uh so so the tool told us that it's possible to take this invariant and if we think further we can take this attack even further where now that the reserves for token 0 is 0 we can call this contract we can call the burn single function again with one token for uh token zero and this time since the reserves are 0 for token zero the calculation will uh the get amount of function will allow us to withdraw the entire liquidity for the other token so in the end what happens is that by supplying one uh by if if you can manipulate the balance of the contract in such a way that your share of the lp tokens can give you the entire liquidity for one token you can then proceed to call the burn single function again with just one amount of amount equal to one for token zero and then this so whatever liquidity is remaining for the other token as well and the tool showed us that this is possible and the way you can actually do this is by by you know getting a flash flow and sending that money over to this contract and in the process inflating the balance of the contract uh while the reserves uh continue to stay uh as they were earlier and this is and when you send the money over from the flash loan you don't call any function that that updates the reserves and makes them equal to the balance and so when the burn single function is called the for the contract will calculate the amounts owed to you on an inflated balance and give you this attack method so that's uh that's how we found this uh potentially very serious bug uh in the tribe called Trident platform any questions um not so not not uh not for now but um yeah we do have I do have some purpose questions but uh if you have uh something I mean if you have more things to go you can go go for it right I think good to have actually a person because there's 10 minutes RX maybe we should have people with questions probably there's only 10 minutes left on the web okay um just let me so um thank you uh muli and uh Alex um we would normally um do like a quick fireside chat to get to know you guys first and then we'll proceed with some q a uh and I think they are quite there'll be a few questions uh actually quite a lot actually for me so uh before we start um so um so I understand that blockchain is a really new space a really relatively new space compatible should be compared to the former verification techniques uh so what made uh you guys um jump into the world of blockchains and uh what do you think is why do you think it's a good idea to form a formerly uh formerly verify a small solidity code and one other probably difficulties when it comes to uh start what is what's the difference when it comes to a formulary fighting a smart contract and a normal program great great question so the so just to repeat the question the question is why are we doing it in a in a in a smart contract so first of all I've actually used four multiplication on many other domains avionics software uh other things uh basically data structure operating system I think for uh promoting verifying smart contracts and D5 is very interesting because a the code has a lot of value so this small code has a lot of values so mistakes have a significant impact B the code is fair even though it's it's small it's actually fairly complex even the code that you're seeing by Alexis has many behaviors so it's hard for human see that's correct trees but basically once the code is deployed it's hard to modify okay and and maybe the most interesting reason if you look into safety critical quality it's actually not change a lot but in the area of crypto basically people actually you see Sushi such as version one version two so the business dictates a smart contract are being updated so let's make it in some sense an ideal domain to form a verification because you have this small code or modular code which carry very high value and this code is being updated all the time so I think it's it's a very sort of a clear application of this technology and this is actually what motivates me to take ideas which have been developed by academic colleagues and actually making them into industrial tools and try to make this tool as easy as as possible thank you thank you for the explanation uh there's a substance this is you can think about it like uh smart contact is almost like Hardware I mean Hardware is very interesting to verify because once you have a dog in chip there was a bugs in the internship and that say you has huge cost so smart contact is almost like like like like Hardware in a sense that once this code is deployed it's really really hard to change it especially if it scares values so that's why you really want to invest any effort and formal method is one of them to basically make sure that your code is correct before the code is deployed cool so we have we have talked about uh the the awesomeness of former applications and what it can do like five bucks what do you think for example I'm pretty sure uh like as a lot of smart contract developers found the Trap that oh my contracts audited so it should be bug free and I'm pretty sure there will be people who thinks along the line oh my my contract is formal verified so it should bought free what do you what what do you what do you have uh do you have like a word of two for these are these people who have this this thing discounting thing yes yes I think one some level of paranoia is very very good when the Tool finds a bug it's very good but when the Tool doesn't find about the biggest mistake would be the device itself is not like and you're making certain assumptions so I think the formal verification if you're not using right it's not a good thing and even if you're using it right you you all always have to check things like maybe price manipulation you always have to check some properties and I think the you should think of formal identification as one of your tool enough to learn to make your call more secure but it's it's never 100 secure and I think you have to have back bounties you have to have everything to to make sure your code is is correct cool thanks so much for the for the advice um a bit of a key question from my side uh have because former education help find blocks so have any uh hackers a whitehead or blackhead users probably your tool to find bugs and existing contracts and exploit it uh have you have any experience or maybe you guys have found like a bug in the in a contract that has a very high tvl and you guys try to exploit it so has there been any uh incident or any any thoughts of doing that yes yes so this is definitely a big risk we try to monitor our tool and this is a big risk ourselves when we found a bug in it in contact with high tvl we didn't we basically contacted the the team we are we are responsible back disclosure we actually contact the team and and waited for them to fix the the calls and yeah so so the and also we nowadays they are the Bounty program like immunify but yes this is a definitely risk of this kind of using this technology our technology is cloud-based so basically in principle we can monitor and somebody can monitor it and also it's the technology which is available to everybody so hopefully the the owner of the protocol can check it uh check it too but yes you are right if it's a it's a tool which is a whiskey in the sense that it can find these rare behaviors and actually use them to to to uh five bucks we have few customers who have been using all the devotee tool without paying us but I hope they're not sounds like so far they're using it on their own code which is fun but you are you are we are also aware that somebody uses not only the code that they all and maybe we need to make our technology more advanced and somehow at the moment you don't even need that access to the source you can run on the bike but maybe you are saying that in the future we want to make this technology that you make sure that you only run on the code that you owe and but that's not at the moment what is checked but it's definitely it's it is a risk it is a risk of uh if you if you uh find a property with this tool you and you don't disclose it it's each of it yeah I I always use the analogy Like a Knife can be used to maybe um like help you in cooking and also can use we used to inject others so it depends on how used to I guess that's the same analogy exactly so we have another question by Hafiz uh he's interested in using formal Communication in a small school project so uh he's interested to know like what are the prices and uh any education plans for University and so and so forth so we have an interested user here yes so the the pricing is zero we we will I mean we charge pricing for SAS customer but if you're not developing a D5 you can approach us and we can uh in terms of Education there is actually this is how we want Alex to work with us there is well which is a free uh good scheme we also can do and actually there was one that we did last year there's another one which we'll do next year I think Alex do you remember where we launch I think there's one coming now I don't remember I actually know when it's spread I don't know yeah I think it's uh ninth March starting ninth March going after 22nd yeah and there is also macro this is a a us-based team which is doing a courses for for which are uh but basically for profit we're also interested in uh and and we we are interested in in the in uh we we are interested in in doing courses with universities there's also you've probably seen this code Arena so basically there is a competition for writing rules and it's starting a few days actually next week so please join it and you can get start writing rules and you can get bounties or writing rules for the customer and uh and uh and there's no fee you get actually money for participating you get money in this case not from us from the customer for which you write the books so you get a money from the customer you get reward for writing rules for the customer it's an also called Arena also Etc thank you thank you I heard you mentioned macro is that Xerox macro the auditing company yes yes oh yeah interesting because I graduated from one of the cohorts and I'm currently going to uh in partnership with them uh I will I'll let you know shout out to macro okay fantastic fantastic so that's good and we and if you guys are in University and we'd like to hold your own course I'm always happy to help I think we have other people on the team uh Thomas Adams Michael George who will be willing to give material and help you with the teaching so please help us we want to yes and yeah it's easy to get access to the tool and if you want to teach this I think we always get better with the with the teaching lovely uh yeah uh for sure I would I personally would like to see like a workshop or formal verification so that's very cool uh a bit more of a technique question uh I'm so sorry uh do you have like a bit more time for for a couple questions uh we I we have as much as time as lately lovely thank you so much so a bit question a bit of a tech more technical question so is Satora approval only uh applicable for solid code uh are you also able to formally verify um non-evm languages such as sui or even evm language such as Viper or fee or maybe Cairo us and um some of the more upcoming smart contract languages out there yes so the answer is that uh Satora approved I actually work on internal representation which is called top three others code and and this is actually more generalized than evm but we do have some limits at the moment we are targeting mainly the uh the uh uh the the evm base so we have version for solidity there is version for Viper which is coming there is a version which evpf and ebpf is for Solana and this is handling vast and later it will handle move so the idea is that we want to handle as many language as possible we are not handling Cairo at the moment but that's definitely interesting fast because of the reasoning about finite Fields but it's not something we can do at the moment but it's definitely if we spend enough our needs we are looking to understand where do people write contract and usually for us there's an r d cost of developing the new tool so we are we are gonna actually develop already on our world map for 2023 we have a version coming for Viper very soon and the version which coming for rust and Solana also very soon I think movies also definitely on our world map interesting so we have a question from ifrin I hope I get your name correctly so he says if I'm planning to use the Torah for professional bug hunting uh will will I be incur any costs yes so the the hope is that the answer is no the the answer is that we we are really want to make this basically this is a tool for developers at the moment for now when we have people who are engaging us on a private basis we are not charging anything having said that we want to make sure that the tool works so so uh but I think yes it's uh it's a it's a uh yes cool um another technical question so uh at which level does the Satora approval operates do you operate at a bike even by code level or like in the U level so uh how exactly does Satora analyzes the code it works on a bytecode level it worked on the bike level it worked on the bytecode level it's first one the compiler and get to bytecode level and then it runs with something which we call decoupaler because it goes from the bytecode level into much higher level representation because actually the bytecode level is a stack machine and we bound the machine so we do a lot of techniques to make the analysis easier and we probably will do more and we have static analysis that simplifies the code for example recover variable recover types you cover information from the source and sometimes even more easier for formal verification thank you uh so another another question so recently uh in the L2 space we have seen a lot of um emergence of ZK evm and uh I we know that there are a few types of zika VMS such as scroll users like a direct byte code and a Hermes polygon Hermes uses like a like some micro op codes representation so um they have been worried worries that um because of this not direct mapping uh it will be a security risk for um developing on probably one of these events so what are your stunts and what do you think like Satora can come into into play so that's so you're talking about policy Layer Two exactly so policy Layer Two are very interesting we have a customer like uh media who's actually uh working with our tool to secure Layer Two we are interested to secure Layer Two maybe showing some kind of equivalence between the one chord and the other code we actually are using the tool the tool where we haven't seen on your demo but the tool actually can take two pieces of code and check if they are equivalents and under certain restriction so we can for example check code with inline assembly without internet assembly and see that they behave the same and I think checking cohes of L2 is very very interesting fast uh we want to basically do that but usually the way we work we work with clients and the and and if our clients want to do that we we will have them usually we we engage with certain clients and yes L2 is very interesting for our clients and for us cool thank you a bit of a quick question for those who are wanting to learn formal verification uh what are your tips and advice or is it even possible for probably people like me who have no official um formal verification education in University to pick up formal education at least the basics the answer is definitely yes we see some of our customers it's actually come without any background informal qualification I think Alex also Alex you did you have formal notification in the school products I don't even have a computer science.com yes and Alex is doing fantastic so I think that that I think it's sort of uh it's very interesting to to know what who what made your formal verification net I know I talked to a guy named Bowen crypto I don't know if you know him he's like one of the founder of Crypt of sushi and he said look I I saw for my notification I got it in five minutes I don't know it's it's a I I've been a work in this domain for a long time it's either you get it or you I think it's a hate a loud thing I mean either you hate or you like it and I don't know when when is it for example if you like functional programming I guess maybe formal verification be interesting but I don't know if it's a necessary one and you don't need to have a formal notification back on and our tool you saw with Alex Alex talk it's actually it doesn't look like a bus it almost looks like a unit testing you're writing some rules I mean it's not exactly like you testing you should definitely be more effort and you don't want to uh uh tell you it's more effort than you need texting but it's it almost feels like you need testing with some additional thing so you start with the unit testing you you start making tool like Foundry which are very good and you write expecting solidity and very there from there you maybe start writing something more in the CVN and understand where you can write more properties cool lovely so uh for those who are wanting to pick up uh do not do not give up hope there's always chance to for you to pick up and probably work professionally uh like Alex yeah yeah and you can if you are for example we have this other God now that we are giving for people who are helping us secure our way so the idea is that it's actually and I think if you look into the auditing space everything is tricky too I think with formal notification auditing together can be very interesting so basically the idea to read the code and also write these properties yeah I've been thinking of you doing the same as well writing invariant as well as looking on my own and then try to see if there's anything I miss out that it seems really cool um that's sorry there's there's another question uh by Hafiz very interesting one so can Satora for me verify other codes like python Arduino uh it's like a same like spin model Checker or TLT Etc some of the terms I'm not familiar with yeah yeah so so these are this is very interesting tool the spin model Checker is an explicit State model check so explicit State model Checker is a kind of very very exhaustive test so toy is kind of the opposite we never work on the concrete level we work at the formula level this is uh giving us some headache for example if there's a non-linear arithmetic but on the other hand we handle infinite States so in the case I think that you see the example that Alex showed you there's a uh you in 256 if you try to enumerate it with speed you need two bits here's two 256 bit so the ideas we don't explicitly remember at all state we are having an infinite State and this is based on the fact that we convert to smt forward the downside is if your code complete contains uh complex Mass it could be harder so we are kind of it's it's it's essentially the opposite to Speed it says that speed is explicit State model checking and we are doing what basically uh in places to formula it's not actually representing there so it's not like testing what we are doing is it's something much more magic it's this mathematical constraint and it's very very different right I'm getting a very technical I think if you are familiar with the open source tools like Daphne or or Viper from uh from the from the eth so if it's similar to us so this is the so that's a very different than speed if you ask but speed is definitely interesting especially if but in the blockchain it's a bit hard because you have a lot of big numbers and big things so enumeration and also it's inventory so an elevation is very very hard cool thank you uh if if uh I Pro I'm not I'm not explaining this view so if you feel that I'm not asking a question properly do a mute and ask uh for yourself because I believe that you're able to explain better than I do another question about Ephraim it's a tutorial on tutorial GitHub uh is it is there a tutorial on Satori GitHub is it possible for to follow those exercises using like a demo license I I think so I think always on the call yes yes it's possible just use the free demo license you don't have to install anything besides the tool itself super cool uh and uh one Kang has a question can you elaborate a bit regarding the relationship between CVL specification language and smt checker yes so CVL is the higher level language it looks like solidity but it isn't that's what Alex demonstrated an smt check here is something very very different this is not developed by Satora smt is a common library for writing mathematical constraints uh this has been around now for three decades and a lot of tools are they all open source yikes cvc5 uh uh V3 by Microsoft research and software uses them all and also contribute to them so these are tools that they are very powerful they are they have usage not just in in certain people using them in in other domains it's the the solver these solvers have been used in many other domains in computer science so these are very different the CDL is a is a language developed by Satora and smt is a is basically a standard developed by the community years of academic effort and they are the sold these so over they all support the same soga there's also smt competition every year where they are trying to get better actually Satora continued benchmarks so the smart contact Benchmark are part of the competition so basically we contribute Benchmark in order to improve we also give grants to these smt companies in order to improve the the smt solving solvers cool thank you uh wow that's uh thank you million thank you Alex I I learned a lot today uh and I believe we are out of questions um I'm taking five four three two one any questions last call I think Jafar asked the question oh oh yeah sorry um so sorry thank you I totally missed that uh the question was um do you have any graphical representation to see the whole process and he mentioned that uh the process means graphical draw automata shapes uh on the basis of how verification process is done so whatever you want like a graphic with a graphical uh representation of how the verification is done I think there is a there is a graphical representation I think basically Alex showed the trace of the bug but you want something to show the thing about the proof I think that we did thought about somehow to see something like uh basically which passes were explored so that's as far as we were thinking is we we are thinking that sort of to explore which spices to were explored by real proof I think it's coming I don't know we or Alex we know but I don't know if it's something that is available now is there some way when the two say that it is verified can you see something no currently not we do have um in our back end some sort of of a call graph of the program but it's currently not not yet exposed outside it's also very technical we found out it doesn't really help most people yeah yeah I mean the the issue is that why do you want it I mean do you want it to understand because the code that we analyze even the case that Alex showed you is like 20 000 line it would be the the graphical representation I don't know how clear we will be a large program if you have usually we we used to have this kind of academic examples the five line programs and you do that but these are very very complicated programs I don't know if you have a bug to demonstrate the bug that's very interesting but to demonstrate the proof maybe one thing you can do with with smt you can have this idea called core on Sat maybe that could be useful we are using it for coverage the idea is that when the sad solvers say answer you can ask it to give the basic example for the answer because maybe you have proven a property that because it's not interesting cool uh um if uh feel free to admit yourself to ask questions in case you you need more clarification or in case I'm doing a little better job in EX in asking on your behalf um another question uh buy one come so um is there a situation whereby it is not suitable or not possible to be uh for a code to be verified by former abbreviation and what are the limits to it definitely definitely there are many many limits to formal verification and there are limits to our tool the limits to our tool is engineering if you have a code which is too complex we keep improving it but at the end of the day it's a very hard mathematical problem so it's job to fail in certain cases there are also things that at the moment the CVL doesn't support for example properties like liveness usually what we talk about is the tallest properties which is called Safety in the sense it says that something bad will not happen and maybe some things you want to prove is it something good will happen and this is something that you can do with the Satora but you have to tweak the CBL it's not it's not natural so there are some things that you cannot do at the severe level and there are some things that you can write in the CBL and steal the tool phase definitely and all of this must exist they are limits to this technology and it's always the case that we usually try to make the tool good enough for our clients but it's a it's it's it's a constant better cool uh another question by wankang uh is it possible to Auto generate severe on a given code based on some assumptions perhaps some simple constraint and a variant that can be inferred from the code itself that's something that we are working on because part of the program that we are seeing is that customers that don't work with us and don't use our professional service it's hard for them to write the spec so we are definitely thinking of fighting some kind of a security booster that will give you a rules maybe it's not the rules which is generated by the best team that work a lot of time but at least to give you some common rules to start we can also start by taking rules from Foundry yeah so giving some kind of a starting I mean if you look into the way that you have in the CBL I think you have seen it in Alex example there's some code which is boilerplate it's just called which is not needed any thinking and then there's some other things which need thinking and maybe we can do something like for example talk about something like we enter the sea talk about some kind of common mistake that people are trying to avoid and use the CVL or some kind of reverting condition try to use the CBL to to prevent covet mistakes that's their definitely a useful Direction in the product world map of Center cool thank you so much uh well uh he is very impressed by the answer and uh speaking of recently I do have a question on my own uh we're interested in a contract probably uh it's not difficult to detect by formal lubrication too but what about re-entracy among a cross-contracts so uh will uh is Satora able to find bugs when it comes to a cross-contract re-entrancy I I will defer to Alex probably or Alex the question is can we find a we enter c back across multiple contracts I imagine dances yes but yes so if you're referring to my multiple contracts if you're referring to a re-entry see coming from external contact that's I guess that's how it happens and then the answer is yes we can so it's just a matter of writing your invariant in such a way that it covers the spec uh I presume yes got it got it lovely um well um I guess we are also out of questions so any last questions in before we uh oh Salim uh feel free driving yourself and ask questions yes hello guys uh nice to see you again uh I have a question about the verification of uh smart multiple smart contracts that call each other uh sorry if that was already in the presentation I was also doing other tasks and so is it for example uh like you said uh um Modi or Alex there are complex smart contracts that's called other smart contracts and so on so is the formal verification also jumping from uh one call so does it verify I don't know if it's a stupid question but does it verify also uh that the the call to to the other smart contracts so that would be a transaction I assume um or a call so uh and the Can it can it trace this uh [Music] long chain of processes so it's like I'm thinking like microservices so it's difficult to test microservices because a lot of calls and asynchronous and so on and so on so yeah our tool works with multiple contracts in fact most uh projects that we work on in real world are not sim single contracts there are multiple contract setups and there are ways in which we handle that if we have exact implementations to call two contracts where we have calls going uh we can link those external contracts with the contract that we are trying to verify and the tool will be able to handle that easily because it knows exactly how to handle those external calls there could be cases where you don't know what the exact implementation of that external contract is if you could be dealing with certain interfaces where you don't know what the exact implementation is on the other side in that case we can we have a few different approaches we can we can give the contract a few a few different Implement implementation the samples to work with it can check with a bunch of different implementations or it can it can assume a certain behavior from that code from that external call if you are sure about uh or if you if you're trying to verify a property which only cares about maybe the return being true or some number being greater than a certain value if if that sort of an approximation is okay then we can summarize these external function calls or we or if we don't know anything about that external call and we don't have the implementation then we can and then the default behavior of the tool has to assume that anything can happen we call it have a king where it will uh consider all possible cases but yes when the Tool is capable of handling multiple contracts and uh depending on your access to those and the actual implementation of those contracts the tool can handle all the scenarios but as Molly said it's a very difficult mathematical problem uh the more complex these interactions get calling into another contract which might call other functions within itself might have a lot of math so it could cause problems so the total in terms of computational difficulty but it is capable of handling it I I think also I'm not a solidity expert I imagine X but things like delegate code I think are very complex in the code that's why we want to build this extra layer this here is foresight that basically call the same tool but later in the in the thing because we operate on the evm sometimes the sometimes the we make certain assumptions like usually you engage with us usually the team engage with us either self-serve a full serve before the code is deployed so we uh and but it's interesting also to of course check the code after it's deployed it's also interesting it's not and thank you for the explanation thank you uh and um for those who would like to learn of how to use Satora approval that's the GitHub is github.com tutorials and um URI is also in our EPL uh telegram group so a feel free to ask questions in a group and I'm sure he's more than happy to answer all your questions um maybe I don't know I'll share with UE but some people I saw in the text that they want the slide is fine I will share with Umi and maybe you can share it on telegram it and also if you want to have other information which Alex or we have me and we will help you uh it's a it's a we can give you more information and more more available information and please uh yeah thank you thank you for offer and I I I'm sure I hope that everyone will take advantage and learn something and uh do foreign for yourself uh we are 9 25 at least Malaysia time five more minutes um any more questions and if not I would like to remind okay before I before I uh officially end this I would like to remind everyone that we have an upcoming uh note Workshop uh it's a Offline that means in-person Workshop that you go through a setting out of a simple ethereum node and how you can contribute to the um the client that we see uh of of ethereum network so uh follow us who have sign up um see you there and uh for those who have not I'm pretty I think it's recorded so check it out in the YouTube so as similar to to this talk it will also be recorded and uploaded to the YouTube so um just for those who do not know where our channel name just go to youtube.

com and search ethereum Malaysia and uh you'll see that uh this recording will appear uh pretty soon and I will of course remind everyone by sharing the link in the in a telegram group afterwards and yeah that's all and any any last words from muli and Alex or probably URI do you want to say something uh any last words for for the community and uh yeah thanks for having us um we're happy to answer your questions and uh yeah please reach out and try it it's a new exciting technology thank you and yeah I would like to personally I would like to personally uh thanks Satori muli Alex for taking your precious time to share this wonderful technology to the Malaysian community and it's something that I'm personally very interested in and thank you so much for doing this and yeah that's all for me thank you very much for having us thank you so I'm gonna pop