Preventing billion dollar coding errors with scalable formal verification - Mooly Sagiv, Alex Joesph

foreign [Applause] [Music] thank you for coming uh I'm going to talk now about formal verification for many of you it's probably a foreign concept how many few of our developers fantastic that's their talk for you how many of you know about formal verification sound great so I've been working on formal verification for a long time you can see and I think it's actually an interesting domain for many things I think it's a perfect application for D5 we had Jeremy's talk about balancing and actually it's related to what we're going to show you it's technology for checking the correctness of D5 and I have an hour for the talk I'm gonna use only half of it and the second half will be a demo without a tool which is publicly available you can try it and you can get a free version of it there's also paid version of it it's a subscription hello it's just what do I do I have to do something okay I Okay so what is a company for checking correctness of code so Torah is a company which is global we have a we have 90 people on the team I didn't write the list of all of them uh our team consists of several people and I think the we have about 25 people this PhD in formal verification from top schools in the US in Europe as well and we combine it with other people who are Security Experts I mentioned only few of them here and I think we are very very grateful for collaboration in particular I have a collaboration with Rajiv from Sacramento and basically this help us to embod people into this domain and some of them are here and working with us like Alex Joseph and others they're actually bringing more people into this space and we are looking for more we are looking for more and there are different ways that you can collaborate with us you can work in theater but you can work in in customers that work with a tour you can also work in the community for example we have a large Grant which was just so basically you're going to write correctness and we are doing it with other protocols we are also working with some of the Auditors for example spear beat and code Arena so basically they are kodavinizing is a Content company and as part of the content you would write correctness rules and you will check them with the Satora folder uh we also of course acknowledge to our connection in Israel specifically to the IDF so we have I think Amit heavy was a senior person in the idea for code vulnerability and he leads our security team so everybody knows about this bargain we had about bugs in many places there are a lot of bugs I want to actually point out to you D two ones which are my favorite this is the normal pack and the other one is the compound so these are cases that basically the quad actually was good actually it was even audited and for example in the case of compound it was even checked the compound is is a they use a very good Auditors and they're also paying customer of Satora and they use satura but what happened after they checked the code with Satora somebody changes the code without one Etc and as a result there was a hack which was exploited so this is why we want to use this technology to check the code before it is deployed so in the domain of security oops there are different tools uh the simplest tool you can use is testing basically you test your code and all all developers will use testing or we use fuzzing there are also tools that help you make the fuzzing easier in the area of web tool there is AFL this is a very very nice tool which was used to find many many bugs and in the area of web3 people are developing similar technology in particular 12-bit is developing in kidnap and found an uh Paradigm is developing Foundry these are very very nice tools they basically test behaviors the the problem with these tools they are very very useful but to promise them that's hard to find bugs which are somehow happening in real situation and I'll give you one like this but you can see many of them in the sector approver that actually these are bugs that happen after many states and it will be hard to detect them if you start running from initial step so that's one technology it's not unique to web3 it was of course in web 2 but it's also useful in web3 it's probably less useful in web Suite than web 2 because many of the security bugs in in web3 they are specific there's a managed environment the second technology which has been around for ages is static analysis so static analysis it provides more coverage than fuzzing and there are tools available there are industrial tools mainly for web 2 that checks the code for correctness and it covers more Behavior than testing but the problem is these tools and uh that basically they have the ability to basically Miss errors and they have false positive and false negative in this context Satora actually has built a very interesting case in the Serato approver we analyze the byte code and actually we can prove certain properties automatically without the human and this is something which is integrated into the search of approval there is a static analysis integrated the right hand side these are techniques which are supposed to provide more coverage but they are potentially more expensive and they are called formal verification intuitively formal verification means showing that your program does what it's supposed to be and there are two branches of formal verification the one which I'll be talking today which is called automatic formal verification the idea is the human rights the properties and the Machine is trying to reason about these things and this is working by compiling the tool into some kind of mathematical formula and this is what integrated into the software approver and there are a lot of Open Source Tools in particular the Daphne tool by Microsoft research it's a similar tool it's a tool that basically compile your code into a mathematical formula the difference is that the Saturn approver is more scalable and you can see the for example the software you can run it on thousands of lines of code which is not something and if this is unique not just in web 3 the ability to run on such a huge code and we have a proprietary technology that we develop that help us scale this this is why we have all these Talent people that are helping us building this stuff so this one is effect it's to give you effective proof and Bug finding because it doesn't start unlike fuzzing it doesn't start from an initial state but it is expensive because the problem that is computationally expensive we usually in computer science we call it undecidable it means that the computer will not always do a perfect job and the other branch which is which is also useful it's called interactive sometimes called manual formal verification so the idea here is that not the computer is doing the job the human is doing the job and the computer is only checking you and there are tools in the area of of web3 there's the K framework in web tool there is tools like lean so these are tools of o'clock these are tools that check your proof you are writing your proof so in this case you can never get wrong you write your proof and from the proof you extract your code this is a nice tool which has been used in a nice methodology which has been used in many cases the problem is this kind of approach that is very very hard for human to use even for small things like erc20 you may have to spend 10 months to to prove this property so this is very very hard this technology so maybe just to give you a a hint on static analysis so this is one of the most useful static and other tool which is called slitter how many of you know sleeping great so I just went little on the bank bank is a very very simple code and it has many many red lines do you want to guess how many of them are real error zero and the reason is not because leader is such a technology which is bad of course you can improve the technology behind Twitter but the idea of the slitter does not know what the quad is supposed to do this later is basically running a generic test on your code in terms of comparing the tools so I try to compare you have basically The Other Extreme so this is the extreme that you get very high coverage I mentioned K Rock lean so these are the tools that get High coverage and the Other Extreme these are the tools which are easy to use and I mentioned uh Foundry but there are other tools which are easy to use and certain is trying to build something in the middle we are trying to make something easy to use as the the or maybe not as easy but uh close to using a father but give you almost the coverage that you get from interactive term program and I think we are there we actually have a lot of things that we have done in particular we are analyzing the executable code we are not even trusting the compiler we are checking the executable code we also make the tool very easy to use and you will see if you see Alex will show you and you can switch with the demo and the other thing that we do we involve the programmer in the loop when when the Tool when it's hard for the tool to analyze the code you can use modularity you can basically make your code more modular or tell us how your code is modular and the more your code is modular it will be easier for our record to analyze so what do we do in satura we do two things we have an open source language called CVL is for a language for writing properties this is something that we want everybody to use and it's something that you the properties of your code this is the CVL and then we are developing technology we are developing three kind of Technologies the first this is the technology for checking the code at the moment it's proprietary but you can use it and you can use it as much as you want the second technology which is coming actually very soon is developed by changanandi and Chandra what she's she's leading she's leading the project for checking the specification and this is an open source tool it's essentially a mutation testing for solidity in which you can check if your specification is okay he's checking that the CVL is okay and it's making the task of checking the writing CVL easier and the sad technology that we are building now is a monitoring technology it is the idea is that we want to monitor the CVL when the code is executed and when the transactions are so what I want you to get from this talk and hopefully this is what you get when you use the Satora is the the ability of the beauty of invariant and in variant these are sort of the essential properties of program which basically means these are the properties that if they they have to get to be right and if they are wrong something is bad okay so in area of D5 the interesting thing is like solvency it means the bank has enough money to cover the loan it has some kind of property and these are the invariants that you have to work when you are using Satora so let me give you a very simple but interesting case of insolvency so the solvency the most intuitive solvency says that if everybody goes to the bank the bank can still pay the money pay his debts and and solvency is it's an interesting property for all the D5 D5 protocols and what's mentioned by Jeremy in the previous talk Serato works with customer and usually we work with them either before audit or after audits these are the cases that we work with customers after audit which means they completed the audit and after that they checked the code with the Satora approver and you think you can see here these are bugs that are found by this technology after the audit was completed and all of them these are by solvency I'm going to show you one like this but the idea this is bugs which allow you in a rare situation to take the money from the contract and this was found by our little and it was found after a very very good auditor of course an auditor can also find bugs after us we are not replacing the auditor we are complementing the auditor so how does the Satora prover where you will see in in Alex demo but the idea is the user is a static analysis like Slither but you are not only writing the code you are also writing the environment and the tool can do to fix it can give you a mathematical proof that the environment is maintained that's very interesting but the most interesting case and this is what I showed in the previous slide it shows you a violation it shows you a potential rare case that the program starts from a state which satisfies the environment into a state which violates the environment this state is not necessarily the initial state it can be a state which happens many many uh uh after many steps of execution and that's the beauty of formal verification it gives you an inductive reasoning why your program is correct independent of how many time it's executed so of course since we are talking about the computationally hard problem the tool is doomed to fail in certain cases and in our case the failure means not false positive or false negative but it means timeout it means you run the tool for two hours and you don't get a result and we have a technology that we are building to improve it but it's always doomed to fail in certain cases and here you can use modular reasoning we are doing many many things but you at the end of the day if the code is complex enough the tool is doomed to fail the technology is very useful and I already mentioned that as part of your CI we integrate like two like Circle and cheat so basically every time you change your code you want the tool and that's the difference with a manual audit in the sense that this is a continuous process you run the tool you change the code and assuming that the environment Remains the Same you basically maintain the same environment throughout code changes so this is essentially the tool that you want to integrate into your CI to make to keep the code safe actually is fairly complex technology and I won't be able to explain this in this talk but there is a white paper they encourage you to read which actually explain everything behind the sector approver I'm just going to give you the basic idea so basically we want the compiler the solidity compiler and then we have our own decompiler we have our only compiler that decompiles the evm code into something that we understand so this is these three others code it's actually something that that we understand at the moment we are supporting evm but evpf is coming and web assembly is coming so we will support other blockchain so we are basically building this stack to support all the blockchain that is important maybe Cairo maybe others so this is all in these three others code and then we have our secret Source we have actually tools that simplify the code and that's very interesting we run some static analysis but this static analysis is not used to find bugs it's used to actually simplify the code uh so basically and the interesting thing about this and I don't know if you have seen in the process of simplifying code we are making certain assumptions about what the compiler generates but we're of course checking them so we are not analyzing arbitrary code we are checking some properties and I don't know if you notice we actually produce many of the bugs in the solidity compiler so these are bugs which will automatically identified by a tool and they are bugs in the solidity compiler itself that so this is actually an acknowledged from the ethereum foundation uh the other thing that we do we take the code and generate a mathematical formula here we are building on smt how many of you are familiar with smt few fantastic so smt is actually a technique I mean if you ask people in computer science they think that satisfiability is a hard problem they're of course right but the idea is even though it's a hard problem there are actually tools that work that that actually can solve many many instances of that and the idea is there are even tools for smt and we actually use all of them we contribute open source to them so basically part of the things that we do in the in this thing is we make smt reasoning easier if you don't know what smt think about linear programming think of some kind of mathematical reasoning so what we do we actually and we we also going to do more we do a lot of things to reduce the number of timer to reduce the failures and in particular we care about financial systems because this is where all our clients are so I'll give you a very very simple example we'll give you more so this is a very very simple code you see you transfer and the invite that you want is that the total is equal to the sum of the balance and you run the tool you see the tool automatically identify a bug in which L is transferred to herself and basically the the money is gone and this is a case so sorry actually increased so the the sum is increased my mistake and this kind of bugs these are the bugs that we are finding with this kind of techniques these are the violation of your environment and so this is the case it was found by the tool when you are correcting the code we can actually produce a mathematical proof that the environment is maintained it doesn't mean that the code is bug free but at least it means that the rule that we check is maintained so that's the idea ah actually we have two type of customers and maybe now three one of them are security researchers which is fantastic they are using the tool which is great like in the spear bit and now with us Ave code Arena the other one our our developers and the third is us and the interesting thing people that use us the maker team they have actually a very very good team I think about seven or eight solidity developers that are using this tool and they are checking environment about the code and the environment that could wanted to check is that the code is the the coin is stable so everybody know what makers does right so make your Implement a stable code so the environment says that the coin is stable and in fact the tool found that an example in which in certain cases it is violated so this is something that was found by the tool and basically you see there is a niche function and they need function the invite that has is that the depth is equal to the sum of the collateral and when the two will actually find that in certain cases you can violate this environment and when you fix the call it shows you that this environment holds so this is a very very good use case of this technology finding bugs in your code and these are potentially hard to find bugs that we are finding with this kind of Technology I want to basically close this first part by showing you uh a critical bug which again found by the tool and and Alex will show it later so this is the sushi swap trident it's a code and actually related to the talk that we've seen by Jeremy it's a basically Implement what Jeremy said the Dual dual uh liquidity pool and you see the code here there's been single this is a chord which is in solidity uh uh you it's probably hard for you to see the bug but I mentioned it in red basically the quad is not using it's it's more interesting bug than the bug that we have seen in the previous slide because the code is actually not using correctly the API and as a result there is aware back in the code and this wearback is found by our tool and this will bug will allow you to completely deplete the code the the money in the Contour okay so what is the nature of the bug so you have to say What is the invariant and the simplest environment about liquidity pool is that the multiplication is constant but I even use something simpler it's basically say if you have two tokens they they cannot be that one of them is zero and the other is is not zero so if one of them is zero the other one better busier and here you see Bob and Alice in the trident and there is an operation in the court that says burn singer in which Alice Banner holding and what happened this actually you see there is the number is 400 and the number of B is zero so basically you see that the invite is broken now okay so this is a violation which was found by our tool by basically running our tool we found the this violation we found this I have to say before the code was deployed most of the bug that we found of bugs that were found before the code is deployed when we are finding code box after the code is deployed we are very very quiet about them uh so what's going on so in fact what's going on here this bug is a bug which is very very you notice that the system also always start from our environment so the question you can ask yourself how can how can you have this environment how can you violate this environment and what are the implications of it so this is the case that you see what happened here it is deposit a hundred coins uh Bob deposit a hundred calls and then Alice transferred 200 coins so basically in a is 400 and the token B is 200. now the band singer that basically violates the environment and finally what happened early swapped the money so basically at least give one coin and get all the money and Bob lost all his money so this is a bug which was found by our tool but our tool doesn't see all of them that's the beauty our tool only reason inductively so what does the tools do it looks in these two states he looked you into one state which satisfies the environment into a there is a transition from this state into a state which violate the environment and that's the beauty of the induction of course if you work with in manual formal verification it's exactly the same you you where you reason about uh execution we start from a state satisfy the environment into a state violating so that's the idea I want to close before I let Alex uh present the the the the demo I want to actually sort of tell you some things and these are of course not just my own uh experience this community has been along for a long time formal verification has been used in Hardware industry especially after several High uh important bug were identified so the question is what's the value of formal verification and this is something that we are trying to understand some of them of course are not just for web 3. so the first thing that people think about formal verification in particular on web3 you see a lot of people speaking about it formal verification is about proofs but I think the most value of formal verification of bugs these are hard to find bugs that you are finding during the process so that's the and I think that's we see and I try to make it in this talk and when you use this Auto approver you can see that it generates a proof and of course the proof has a value especially if your environment are okay but the most interesting thing these are bugs that are prevented the other thing already alluded to that is that the hardest problem people think about formal verification is go back to life theorem and others that say this is a computationally hard problem and of course it is the case but we think that the hardest problem is actually come out coming up with these invariants and actually that's why we need the second wheel that's why we need people like you to help us write interesting environment and we are trying to incentivize people to write interesting environment like for example with the other we are encyclic Vice people with money if you write a good environment you get a reward for that the other thing is that and that's also think people are thinking about it when you think of formal verification people say oh I formally verified it and one of the giant of computer science knuds how many of you know news oh great so close of course is a fantastic computer scientist at Stanford which has contributed to many fields including formal verification and one of the jokes that they say I don't believe this code I formally verified it and I've never tested I think this has a very good thing the idea is that basically formal verification is just one thing it doesn't guarantee that your code is correct it only guarantees that the environment are meeting which is of course increase your security but it's not a bulletproof uh the other thing in the web tree that people think and they approach us they say look auditing is expensive we want you to replace formal uh auditing it's not what we are trying to do we are trying to complement auditing I already mentioned that there are Auditors who use seratoa the human and the computer are are actually uh they basically help each other it's not like an automatic automatic car when you just have it and you because you need the human for example the human can actually find bugs after us if we don't have the right words and then we can update the rules the human even already we have seen Auditors but found bugs in our Woods which is fantastic the it's just another artifact of the code to analyze and we want the human and to come and and the auditor the human auditor and the tools to help each other they are not we are not replacing the auditor and maybe the last thing I want you to take and that's again something that the formal verification is something that you need to think as early as you can whether you engage with certain or not it doesn't matter but you need to think of formal verification in particular form of specification as early as you can and use the tool even use our tool as early as you can even when it's feature complete use the tool so this is the idea you want to use this uh technology as early as you can because it will prevent bugs and it's easier also to use it because the code gets more complex it's harder to use this technology so we want to you to start use this tool as early as you can so in conclusion I want to basically come to tell you sort of three feet one is that bug finding is hard without a tool without a tool it's hard but actually makes it interesting by using this inductive reasoning by the idea that you write an invariant and we are looking for violation of this environment the other thing that I didn't get a chance to explain but there are talks that we explained that and there are technical people on our team we are actually producing something which is interesting in terms of uh new algorithms we are actually innovating in the area of static analysis and innovating in the area of constraint solving and we are combining these techniques and you are welcome to listen more what I talked to you is the idea of automatic formal verification this is the idea that you write in variant and it's like a quality assurance tool that checks the environment and either find a violation and this violation can be rare or prove absence of violation so this is it please if you want to scan the technology paper I I suggest what we do now I will answer some questions if they are and while I'm asking questions but maybe just let people scan uh uh uh Alex will set the demo please take the demo is interesting but I'm happy to to take questions on on my talk on formal verification uh please if they are question I would love to take some maybe what you said you can set them everybody scan yeah you have questions yeah would form a verification still work for systems that are not closed so for example for let's say a D5 application like Unison upright you can probably write an invade invariant where the total USD value of Assets in a pool will always remain same enough after swaps right but say for our system which is not closed so it's like a cross chain liquidity pool where tokens are coming in on one chain but they're actually leaving on another chain so uh what formal verification still makes sense in a scenario like this or what do you suggest here interesting so the question is uh will formal verification make sense in a system that is not closed so the answer is it makes the most sense when you have free system which is not close but it's more complex yes okay so and we work with compound for example who's calling uni swap we work with a business that actually some of the code is not available so the idea is modularity you basically have a requirement on one thing for example uni swap is monotone and then the question is do you trust this thing or do you check it so you can do two fix when we analyze the code of compounds for example we made certain assumption on the unit Swap and the question is do we check them or we don't check them at the moment we don't check them we can check them statically or dynamically so the idea is when we work with some clients they actually call other clients and it's actually the beautiful thing of formal verification and you even seen it in the that you are finding an API violation you are finding a case that I'm calling your code and I'm not able to actually satisfy the precondition for this so yes this is actually the most useful application of formal verification is called and us that actually there are a lot of interaction between the code and and yes we can do it either statically or dynamically we can do it statically it means that we need to analyze both pieces of code we can do it dynamically or sometimes it's just assumption because sometimes it's code that we don't see somebody is calling an oracle or somebody is calling something that is not in something that we can only lies it's a it's a bridge for example so yeah but it actually is the case we are finding bugs because if you have a bug with respect to the Assumption now you are implementing the the compound money money market and it is calling the uni Swap and the question is you're you're writing these assumptions and then you are checking the the correctness of the code not with respect to the actual code with respect to the assumption that you made so yes it is very very useful and it is one of the most useful application of our clients but it's not easy that clarifies a lot thank you [Music] there's another question here so when you have these formal verification specs um and you like you say that formal verification is computational uh computationally expensive do you mean that uh you're fuzzing the invariant and you're checking all of the states like in a brute force method or do you does that competition go into calculating a mathematical proof uh that this state will never occur or is it like a Brute Force so so our technology doesn't do fasting we don't enumerate the behaviors what happened is that we compile your code into a mathematical formula and the mathematical formula enumerates all the behaviors and this is the and the question when it's working when it doesn't work it's a very very hard question in jail for example when you have linear equation it's easier to solve so we are not enumerating the behaviors that's the beauty of this technique it's actually giving you exhaustive think like if you have for example in the story in the ethereum you have like an integer which is 256 by 2 to the 256 we model it as an arbitrary integer so we give you a mathematical proof and when is it hard when it easy it's very very hard to know we actually have a lot of algorithms and sometimes they surprise us how well and how sometimes it's really surprising these constraints over that they can actually succeed on things which are very very complex for a human but sometimes hard for example when you have interest rate it's actually we we we came to know but it's actually it's we are not doing further we are we are nominating all behaviors that's very very different it's of course more expensive but we are we are doing fuzzing we are not doing fasting we are basically enumerating all behaviors and of course it's it's done by the by this reasoning about formula you write a formula like say x square is is is equal to four and then basically the system will find out that X is two so that's the idea we write a formula and then we have open source tools that we are we are using to to find the solution to the formula and the solution to the formula which means you have a bar and if you find out that there are no solution we can generate what we call a proof tree which is actually indicate that you don't have about but this proved to enumerate infinite number of behaviors we are not looking into final Behavior that's a very big difference from fuzzy we can do fuzzing for example to get initial answer and we are actually doing it because sometimes it takes two hours until you get an answer and the user is frustrated you yeah great thank you which smt solver have you used and why and so which smt solver have you used I am assuming either Z3 or cvc4 and uh which one uh do you think has given you more empirical empirically can you comment on the performance of these yeah so that's a very difficult question because I'm I'm fond of all the people so but fortunately actually it's very surprising all so it's actually on different benchmarks on a different code they are they behave different and historically yikes is much older and people have invested a lot less but we find that in summer for example the ice does fantastic where z3. CVC we also supporting setova we raise money to support here we are supporting of these kind of things and we are improving we are adding uh now support for C3 for for a large bitwise operation we we are we are working with the so the answer is that and also we are thinking of combining them because they have this idea of learning lemmas and sometimes they'll even when you have a timeout you learn something and we can actually combine them so we are we are agnostic we are at the moment we are using the three of them and our user I think there's a flag but I don't know Alexia they reflect which one to use but I think most users just let the system choose yeah and there are machine learning techniques that we are doing to optimize that yes so just to extend on that I mean since I've seen it in your tool so just for other people this smt solver these are techniques that are used under the hood here which are used of course in Microsoft Visa we basically compiled the code and the environment into huge mathematical formula sometimes few megabytes actually it's interesting that it works and these few megabytes of formula it gives to the solar and the solver gives the solution yeah so great tool chain I've seen that you have a lot of custom software right uh for your certain applications for a certain requirements right similarly uh have you thought of just creating your own solver combining all the strengths of if at all yeah yeah so that's a very interesting uh so the question is have we thought of construct creating our own smt solver we don't know at the moment we have been around for four years I think it will be difficult for us but maybe we are more thinking of contributing small things to existing solvers and and supporting them but yeah it's it's very interesting to build some specifically for D5 what we are thinking more is sort of thinking something on the opposite trying to tell like some kind of design pattern tell people if you write the code at the moment one of things that we are doing we used to charge a flat price for using the service but we are no longer charging flat price if you have code which is complex you pay us more but the idea is we want to actually reduce the price by telling you if you write the code this way and if you write it more modular it would be easier for us and it will be cheaper for you we are we are trying to scale up and it's uh but yes down the road maybe developing a server for D5 I know data on Foundation is interested in that but yeah it's interesting uh so the challenge now has transferred to writing specific and very tight invariance uh that doesn't seem like an easy task for a complex project invariants might get easily complex and there might be bugs in the specification so you mentioned there's another project which kind of checks the correctness of invariants could you please tell a little bit more about that yes yes so you're absolutely right so the the issues that if you know I mentioned in computer science we mentioned close but another giant of Computer Sciences I'm sure that most of you you know is diagster and I mentioned the Daxter of course in Van go back to a platon but Daxter said that you cannot write a program without writing the environment that's of course correct in principle but it's very hard to write invariant you're absolutely right and we also find out that when we are writing environment for our clients we made them wrong and and but the idea is the question is what does it mean wrong if it's wrong in the sense that it finds a bug that our tools say and then we check the environment that's one thing but the thing that we are aware we are aware from environment that actually holds and give your first confidence on your code and we already have one client who actually use us in addition to auditing and then basically if somebody found a bug and they didn't accuse the auditor so the user the the and the the customer actually wrote the environment and there was no failure of the tool the problem that the invite was tautology you write something like seven is greater than five and the tool of course was able to prove that seven is greater than five but it's and it's increased the confidence of the of the of the of the of the protocol so we now if you look into the Satora even if you look into the version that you have this cannot happen we have basically a vacuum the qut chat we have something that checks if your code if you have a bug it's a bug but if we verify your property we try to check if it's vacuous we try to check for example this kind of bugs we can avoid and what we do we do mutation testing we mutate your code we take your solidity called then you change it and if we change it in the environment still holds we suspect that something is bad and this is very good for us because as a company we are basically engaging with larger community and the ideas people are submitting environment and we have no idea this is are good or bad so we are using these tools to evaluate the environment that the community submit for example in the other project I think we have 25 security who are submitting environment so we are using these uh tools to check the environment both the environment that are produced by our team but which which are written by other people so you mentioned about the correctness preserving Transformations could you elaborate a bit on that like how do they preserve the correctness or like how do they work or give an example of that maybe so I mentioned the correctness of preserving transformation we have a so this is of course uh us we basically uh did uh wait uh so I I don't know how much the way code is just in in the evm but it's basically what this idea was called bumper locator so basically memory is allocated topically and what we observe certain properties of these uh bump allocator and in in order for that to simplify the code this is how we identify many of the bugs in the solidity compiler itself and we are actually submitted an article about that and we will publish it of course the the so these are results that basically these are techniques called Static analysis which actually infer some properties of the code and intuitively the ideas for example you have a load and a store and instead of letting the smt vision about it we can reason about it and this is a game changer it's a it takes something from time out and convert it to 10 seconds it's a game changer of course the smt it's a complex technology the the less you can call it whether all the smt is solve it better and we want to do more like understanding the values and this is how we say correctness preserving transformation but of course we haven't proved that they are correctness proving transformation it's called that we are written in our tool but it's uh we of course up to a bug in our tool they are correctness preserving transformation thank you think without you uh so I'm gonna take you through uh a bug that muli also spoke about uh it's the bug that we found in the uh in the Trident uh constant product liquidity pool uh the idea is to give you some sense of how you work with this order approver to find bugs so um I'm gonna and you can also if you want you can also start working with me if you go to demo.satura.

com or just go to satora.com and look for the demo button on top right you will land on this page uh just go to the interesting box part and click on the custom product broken uh piece and uh this page will open up so on one side you have the solidity code that we are trying to verify on the other side we have the spec that we've written uh and the tool takes both of them together and uh mashes them together does a bunch of optimization and then comes up with The Logical formulas which are then fed into the smt solver uh all that stuff that mooli spoke about but uh yeah let's let's uh first look at the solidity code uh and uh and then we'll look at how we went about verifying this so uh it's essentially uh as I said it's a constant product uh liquidity pool uh which uh implements any rc20 protocol also for uh the the lp tokens that it mints and distributes so for those of you who don't know uh a liquidity pool is basically where you provide liquidity and people use that liquidity for various applications in this case this liquidity pool was going to be used for an automated Market maker and uh it was a constant product uh tool where uh if people like you and me we can supply liquidity to the pool and as an IOU we get back some LP tokens these LP tokens uh from a liquidity provider standpoint can be redeemed for your share of the liquidity so you get back uh some part of the protocol uh so you will get some some part of the liquidity pool so you get back some some amount of both and uh so the idea here is that okay I'll talk about the properties later I'll just quickly run you through the uh through the the contract here so it's an erc20 contract uh on top of that it builds uh functionality for the liquidity pool so we have two tokens it's a classic two token constant product uh sort of a pool so we have two tokens uh the contract also keeps a track of the reserves that we have for each token uh it also keeps attack of the product that it uh adheres to when it's swapping uh tokens uh this product of course goes up and down based on the liquidity uh overall liquidity in the in the pool going up and down uh but when you're swapping uh uh before the Swap and after the swap the the product needs to remain the same uh there's uh there's a mint function which basically mints uh the lp tokens whenever you add liquidity to the pool and these LP tokens are essentially shares that you hold in the liquidity pool so uh when you redeem it you get a part of the liquidity with the tokens that are sitting in the liquidity pool this is a bunch of logic in here that is not relevant for this discussion so I wouldn't go into it uh this this is the most important or most interesting function here uh so typically you know in a liquidity pool contract when you're redeeming your liquidity pool tokens for uh the underlying Assets in the pool uh you would redeem the tokens and the contract would give you back two tokens some amount of each of the two tokens in the contract in the pool but there is a special function here which is called burn single what it does is that when you're redeeming uh your liquidity uh it allows you to pick uh one token that you want to get paid in instead of two tokens it allows you the that extra functionality where if you choose to get paid and just token one or token 2 you can do that so what this function does is it does two things first it withdraws your liquidity uh based on the amount of tokens that you have essentially what share of the liquidity approval you own based on that calculates the amount of each token that you're supposed to get and then after that it does a regular constant product uh amm sort of a swap where it exchanges one token for the other uh the token that you want so uh the functionality for finding out the amount that your owed uh by the pool is here where it's calculating uh the amount of uh tokens you get for each token by looking at the liquidity and the total Supply so that's your share of the pool that multiplied by the balance to each token and that gives you the amount uh and then when you come further down this is where it's taking a token uh and looking at the amount of that token that was calculated in this step before this and then it's uh based on the new state of the liquidity pool where of course now the reserves have gone down because you've withdrawn some amount for from each of the tokens so based on the new state it's going to figure out how much tokens you are eligible for of token B uh for the given token a amount and then it adds that amount that is calculating here to the amount that was calculated here and that's the total amount it will transfer to you uh in one single transaction so um okay now I think I'll go to the spec after this and uh so the idea here was that as a liquidity provider there are certain things that you would be wary of uh if if I'm providing liquidity to a liquidity pool I would want to be sure that I should be able to withdraw that so if I have LP tokens I should at any point in time be able to exchange those LP tokens for the underlying uh liquidity pool assets uh similarly if I'm depositing something into the pool I should definitely get some LP tokens uh which is a proof that I've submitted that I've supplied liquidity to this pool and so I'm eligible to withdraw the money that I've supplied back so the idea essentially is that from a liquidity provider standpoint uh if uh if you have certain reserves in the pool then there should be liquidity pool uh LP tokens out there in circulation otherwise uh that there's no way to uh withdraw the the funds that are in the liquidity pool similarly if there are liquidity liquidity pools in the in circulation liquidity pool uh tokens in circulation then there should be reserves in the liquidity pool itself because otherwise the tokens that you hold they they don't mean anything because you don't get to withdraw any liquidity that you supplied so uh all that uh all these properties that I just spoke of these are fairly high level properties you don't really need to look into the exact implementation of the of the liquidity pool everyone can get that concept that if you invested I mean supplied some liquidity to a liquidity pool you should be able to withdraw it and uh you should get liquidity uh pool tokens uh which are essentially a proof that you've Supply liquidity so when we uh paraphrase that into a logical expression this is what we get so this is essentially uh the invariant that we had written here where we're saying that the total supply of liquidity pool tokens Can Be zero uh if and only if the reserves of the underlying assets are zero for both the tokens and uh when we run this very simple intuitive invariant which doesn't need you to look at any implementation just a very high level thing that makes sense to you when we run this against uh The Tool uh it shows us a specific bug that we found and yeah so so when you run the Tool uh uh we're essentially uh I'll tell you how we run the tool so uh we invoke The Tool uh and we give it the contract that we want to verify we space we specify the contract that we want to verify in the solidity file and then we specify uh the specs that we want to verify the contract against and uh any other helper files like we would need some rc20 implementations here to model some of the the calls that are happening to erc20 contracts and then the the compiler that we need and some other flags that uh I don't think we need to get into right now but yeah essentially we are giving the the tool the solidity file that we want to verify the contract that we want to verify and the specs that we want to verify and uh this is uh what the report looks like uh on the left pane here you have a bunch of rules and invariants that you've written and so if you've written multiple rules and invariance that you've run uh with the tool you would get a list here and uh for each rule it will either show you a green circle with a tick mark or a red circle with a cross on it that says violated uh and uh when you uh it lets you do a deep dive so here uh so this was an invariant and this this tells me that this invariant failed in the preserved state of the event so I want to talk a little bit more about how invariants work with Satora approva uh and Bully feel free to add if you want uh so invariant we prove invariance uh using induction uh invents are proven in two stages uh first when the contract is deployed and the Constructor is run after that the tool verifies whether the invariant that you've written whether that invariant holds or not and then if it holds after that the tool will assume an arbitrary state which still conforms to the invariant and then from that arbitrary state it will call any function in the contract and after that function is executed it will again check if the state of the contract adheres to the impedance that you've written once you've written once both of them are verified once you've established that after the contract has been deployed and constructed the invariant holds and after starting from an arbitrary state which conforms to the invariant and running any arbitrary function in the contract uh the the state of the contract still conforms to the invariant that you're testing against by induction you can prove that this contract this code will always adhere to the invalent that you're trying to verify so uh the first stage of the invariant is what you see here what we refer to as in State this is what is verified after the the deployment in the construction uh and we see that the tool tells us that uh what's happened here just give me more guys okay so in state is as I said the first state of invariant checking where it checks it right after construction and preserved state is this is a second state where it checks after that when it assumes an arbitrary state which conforms with the invariant and then checks against all the functions in the contract uh so the the preserved state is what is failing here so uh this has to fail for at least one function uh in the contract so when we click on it and do a deep div figure it shows us that burn single is the function uh I hope everyone can see this is this people on this side able to see this uh so burn single is a function which is causing an issue for us so again we further click on it uh click on the error and now you start seeing things popping up on the right side uh then it is a bit wonky yeah so this is a section that shows you all the rules that you've written within those rules if you drill down it'll show you further exactly what part of the rule or the invariant has failed and specifically which function has failed you this part will tell you the call Trace call Trace is essentially showing you a detailed view of the entire execution that the tool has gone through and it'll help you understand exactly where the error is this section is where we have the variables in call resolution this section gives you more information about the exact values of the variables so if you so in invariant since we don't have many variables you don't see much here but if you like if you write a rule uh and I'll show you what a rule looks like you've already seen what an invariant looks like if you write a rule in which you've specifically defined certain variables that you want to track the State against uh that you want to track against the state then all those variables will get populated here and you will very clearly quickly clearly see your snapshot here of what the value was for those variables before and after some function was called and it's it makes it a lot easier for you to understand the counter example now I'll take you through the the call Trace to explain to you what's happening here I'll get to the preserved block after this uh it's it's uh it's an additional functionality we have uh on invariance which makes it uh a little more useful uh where we have additional specific preconditions that we want to apply with in variants but uh yeah you see here that the tool says assume invariant and please State because that's where it starts when it comes to proving uh specifications proving invariants uh in resource state so it uh it assumes an arbitrary State uh and it ensures that that arbitrary state conforms with the invariant and then it runs a function in this case it's running the the burn sign the burn single function uh we click for the uh it and it tells us more details about it so at this point uh let me take you back to the burn single function so it'll be easier for you to understand what's Happening Here mint burn single yeah so so the burn signal is getting an uh getting us parameters uh and uh a token address uh liquidity which is essentially the total number of uh LP tokens that the person has and the address of the recipient so the address that gets all the the tokens that are withdrawn from the liquidity pool that address so what it's doing is uh it's using this liquidity to calculate the uh the amount of tokens for both the uh tokens that need to be paid out to the uh to the user from the liquidity pool so it's using the liquidity the total Supply uh using that fraction on the total balance of the contract for that token calculating the amount similarly for the other token and then uh it's uh burning the liquidity tokens because now you've withdrawn the liquidity and then it uh based on the token that you've supplied here it decides which token needs to be swapped into the other token and uh that calculation is done here through the get amount uh out function where you supply the amount of the token that you want to swap out of and you also uh provide the latest state of the liquidity pool so this is uh the reserves of the two tokens after the liquidity has been pulled out so the amounts are updated by Reserve minus whatever amount of your withdrawing from the liquidity pool uh and then after that that amount is added to the amount of the token that you want to withdraw and uh then we do a simple transfer of that token that amount to the recipient it seems fairly straightforward but uh where things go wrong is that the the specific example that the tool shows us here is that when we call this the burn single function uh with certain amount of liquidity uh and some recipient that's not important right now but uh we see that the tool is showing us the in call Trace these steps where first the function is checking for the reserves it's checking for the balances and these balances are being used to calculate these amounts so we see that clearly here that it's checking for the results it tells us that it checked for the reserves and the values that it got back over five and four for both the tokens uh similarly the balance amounts that it got was 15 and for for both the tokens and then it checks the total Supply that is a certain amount uh bear in mind this total Supply uh and uh the liquidity that's been giving us so this liquidity is smaller than the total Supply it's supposed to be a a share that you hold in the liquidity pool and uh after that we call the burn function so uh so right now we are here so we've we've seen these steps we've seen this step and in between we've gone past this calculation where amount 0 and amount 1 has been calculated based on the liquidity and the total Supply that you saw we've seen so after this uh after this we go to the burn function and then we uh then you're looking up the tokens for uh so this is a lookup that you see here for the tokens and uh eventually we end up calling the my start call yeah So eventually we end up calling the get amount out function and that is this function which uh which is helping you swap from one token to the other and uh one peculiar thing that we see here is that the uh so basically you're providing it some amount of a token that you want to get rid of and that's this amount and uh you're telling it that right now the state of the liquidity pool is this and if you notice that one of the reserves for uh the liquidity pool has already gone down to zero and uh that begs the question as to how this happened if one person we can clearly see here that this user has a certain amount of liquidity which is clearly less than the total Supply uh which can be seen here if if somebody's really good with hexadecim in math you you can see that it's uh it's clearly a subset uh which means that the person does not own the entire liquidity so if they've done a withdrawal there is it shouldn't be the case that they've completely drained out the reserves for any one token but that seems to be the case here so uh that takes us back to the code and we want to understand what happened and uh that's when we realized that the way these amounts are being calculated is is wrong because we are using these liquidity shares and multiplying that with the balance of the contract and we see here that the tool shows us that the balance of the contract is different from the the reserves that it's tracking the liquidity pool against you can see for token a the reserves of five and the balance is 15 here so uh if you calculate the same small share against an inflated balance amount for a token it could very well be the case that that share of that inflated balance could be equal to or greater than the actual results being maintained in the liquidity pool uh and here in this specific example was it what the tool is telling us that uh the balance was such that for this given amount of liquidity and total Supply this amount uh ended up being exactly equal to the result of token zero in which case when we called the get amount function this value ended up being zero I mean this value ended up being 0 and the other value was whatever was left after the swap so uh and if we look at this function in uh in more detail we figure out that uh if one of these reserved values is 0 then what happens is that the output value that it's returning which is basically the number of tokens that you will be able to swap out swap into uh that number is essentially equal to the total Reserve so what's happening here is that uh this particular in this particular case when you call the burn single function it's allowing you to withdraw the entire liquidity of the of the second token so your the balance for the first token is inflated because of which the share that was calculated was wrong it was equal to the reserves of that token and then when you called the uh the get amount out function it ended up giving you the entire liquidity that you had for the second token uh so at this point we've already broken the variant uh and that's what the tool tells us the tool tells us that we've reached a state where uh where there is uh we have uh uh one of the results has gone down to zero when the uh total supply of liquidity pool tokens is still non-zero one of the results is going down to zero so uh this has told us that uh that that intuitive sort of a property that we had thought of in the beginning that if there are liquidity pool tokens in circulation then there shouldn't be a case where you uh where you can get to a state where one of the reserves or both of the reserves uh are drained to zero but that's fairly possible but another question is how do uh how can someone exploit this weakness of the code and uh we looked into that and uh the attack basically is that uh you take a flash loan uh to inflate you take a flash loan send that money over to this contract and in the process you end up inflating the balance of the uh that token in the contract uh the way this contract keeps it track of total reserves uh versus the total balances is that there's a function called update that's called um you should see that function yeah for instance here so uh every time it's messing with the reserves of the contract uh after it's done messing around with it it will check what the latest balance is and then update the results accordingly the same thing happens in the mint uh function when when you've added more liquidity to the pool and it's given you some liquidity tokens uh at the end of it it'll make sure that that newly added liquidity is also captured in the results that the contract is tracking so uh so if you uh take a flash loan send that money over to this contract uh and jack up the the balance uh for one of your tokens but you don't end up calling the mint contract then what you've done is that the the reserve continues to be what it was but the balance is uh inflated Way Beyond uh there is a value at this point if you uh using your tiny share the limited number of LP tokens that you have if you call the burn single function you will be capable of uh uh your your essentially your share gets inflated so uh what happens is uh all these numbers get calculated against uh these numbers they get calculated against an inflation an inferiorate balance number so for the same small share you're getting a much bigger number and if you manage things such that this big number is exactly equal to the reserve value at that time then you can make the get amount out function to give you the entire liquidity of the the other token and once you've done that the next step of the attack is that you call the swap function here and the swap function will uh again this time you reverse it this time you give it to the other token with one which is which is one amount and uh it will again because one of the liquidity pools has been drained the token B has been drained so this time around because that was zero in the computation it will give you the entire liquidity for token a so uh what you've done essentially is you've drained the entire liquidity uh for both token a and token B there are still uh LP tokens in circulation and uh there are no reserves to back it so uh so our tool told us that it's possible with the get uh get single function it's possible to get into a state where you break the invariant and then looking at that example and thinking a bit more on how to make it a complete exploit we figure out uh this uh this this overall larger exploit so uh that's uh so it should give you some sense of how powerful the tool is because uh you've not even uh you've not even had to look at the the implementation of the protocol you've just from a liquidity provider standpoint thought of the very basic thing that the protocol should give you in terms of security and that is the ability to withdraw your liquidity at any point of time and just just put that down into a simple logical formula and done that against the tool and the code and you get this invariant uh the tool obviously is uh much more Dynamic uh while the strongest properties that you can verify with the tool are in variants which are as simple as this one because they covered a large part of the code an invariant like this as broad as this can break because of any small functionality any small function in the code so you're not you're not restricting your checking to any specific part of the code but you're looking at the entire contract uh so these are the strongest invariants if you could think of high level invariance like this which pertain to any part of the contract they'll always give you the best results but the tool also allows you to write more specific rules we have something known as yeah so you can write rules rules are essentially uh a combination of a pre-state some function execution a post State and then an assertion on based on the state transition that might have happened you can write rules for uh specific functions uh you call specific functions then track what happened uh in the state change and assert uh the change that should have happened and see if see if the contract breaks out of that rule in any case you can write more general rules where you can have so what we call parametric rules these rules are run against every function in the contract so you write some preconditions about uh the state before then any function here it so this this call basically means that the tool will call every single function in the contract with any arbitrary arguments so this call data args is is a dynamic data field which the tool populates with all possible ways in all possible ways and uh so so to fit all possible function signatures and it gives you complete coverage in terms of the inputs that you can feed into these function calls and then it checks the state after that and any assertions that come after that so you can use some parts of the some aspects of the tool to write even very specific unit tests for small functions so like as muli mentioned that sometimes the code I mean this tool is bound to fail it's only a matter of how complex the code is and when we encounter very complex codes sometimes we have to take a more modular approach which involves uh you know looking at the most bottom level contracts looking at individual functions in those contracts verifying the functionality of those contracts and once we are very sure that those functions work exactly the way they're supposed to work then we summarize those functions and we assume that they work correctly for the more higher level contracts so that sort of eases the job that the approver has when it comes to verifying the more higher level contracts uh yeah so you can write rules very specific to certain functions you can write more generic uh parametric rules to test out function execution or you can write very high level properties uh using invariance and uh the tool will tell you if your code uh is capable of breaking out of it so yeah that's what I had any questions what's that uh the tool is free movie has said this many times but uh let me say this again go to the demo page uh work with this as much as you like uh it's free you can plug in your own code here your own spec here uh we have tutorials free tutorials on GitHub please learn uh I'm very new to it as I went through securium I learned the tool in a matter of two two weeks and then used it on a project uh it's very easy we have a very strong Community Support uh internally in sartora we give a lot of importance to that so if you're curious if you want to learn the tool there are a lot of people out here to help you uh it's all there it's up to you it's rather easy to learn our language CVL is uh very similar to solidity so if you're familiar with that it should be very easy for you to learn approval and uh yeah I use as much as you like it's free and get more used to it uh and talk to us if you're interested in working more with us anything else moving yeah good um no no we are you asking if we work with multiple contracts these these properties they don't necessarily have to be from one contract uh like if you have one higher level contract and that contract interacts with multiple lower level contracts which then again go and interact with other low level contracts these properties will be verified on the system as a whole so the invariant is checking every function that it gets from the high level contracts all the way down to the lower level contracts unless you apply some sort of function filter that's again again another feature that we have but yeah it's it runs across the board and when it runs on higher level contracts there are nuances to how the tool models that interaction that inter contract function calls if you like it can make it uh it can assume the worst case scenario assume the the most arbitrary Behavior coming back from that external function call or you can if you have specific implementations that you want the tool to work with you can link specific specific implementations or you can we have something called dispatcher which again uh it has adds more nuances as to how these calls are routed but uh yeah our philosophy is that we want to be extra careful so we we always over approximate when in doubt we over approximate so if you don't specify any particular implementation or if there are multiple implementations but you don't tell the tool how to use those implementations the tool will go ahead and assume the worst case scenario that this call could return anything though so it will do all that heavy lifting of checking all possible scenarios there but if you're very sure of the nature of that interaction the implementation on the other side then you can make life easier for the tool by giving it the exact implementation so again the tool is bound to fail if the code is complex enough and it's these interactions uh happen with a lot of what we call havoking Havoc essentially assuming that you know Haywire uh so if you give it a lot of high-working chances are it will fail but uh yeah I mean the the art is in finding that balance how do you get this very powerful tool to work uh for your project so uh like uh the tool can sometimes uh time out so before writing rules specification yeah do we get a sense that this particular rule will time out or like after running the tool only so usually what we do is uh before starting on a project uh we do something known as a sanity check sanity check is a very simple rule which says that this is the function it's so it's a parametric call if you remember seeing the parameter call where we just call do an F args call which is a call to every single function in the every single external function uh in the contract and all the contracts in the in the scene actually and uh and we just call the function and do an assert false so an assert false is bound to fail as long as the proa gets to that point but if uh your the code that you're trying to verify is extremely complex so complex that the tool is not able to get to that point but it's just too caught up in all the execution and all the branches and all the loops that are happening in the functions then it will never get to the assertion and it will timeout before that in that case your rule will pass because you never got to the assertion and the default is it passes or it times out if you do a sanity check then it times out so uh the first thing that we do with any complex project not just complex any any project unless it's uh just one single uh solidity file and it's very obvious that it's a very simple thing which which is the Rarity we I mean I've never seen such a project in my time Etc but uh yeah the first thing we do is to do a sanity check which gives us an idea of which functions are passing which me which tells you which functions are easy and which functions are failing or rather timing out which tells you that it's too complex so it gives us a sense of uh where we need to optimize things and how how do you need to break it up anything else are you guys curious about Satora do you want to work with it yeah yeah hello yeah if we complete all the challenges whatever you given uh like can we become our official formal verification engineer or something like yeah uh I think Molly would be the right person to answer that so yeah we partner with communities like that and we pay uh people in the community who write rules using our Tool uh right tools and verify code using Our Roots uh only he's interested to know if um yeah obviously you become a formal verification engineer like a certification I don't know if you do that but yeah but that's not the point of these challenges these challenges are to get you a sense of how the tool works yeah so we have engagement with secure well we have engagement with the program right is that the question of how to study is that what you're asking so we have an engagement I think there is online there's an online uh so Satora has collaborated with like uh Alex said Community online communities and one of them is securium and securium is an online community of ethereum security smart contract security focused interested you know aspirational experts the whole thing right so um the collaboration in this particular case was um really to learn I mean Satora had a workshop that goes deeper than these challenges I think Alex Point here was these challenges are really for educational purposes right they don't lead to a certification but sultura has collaborated with securium and our way as well uh where you know once you learn the tool right you can apply it on the code base that is within the scope and uh the top performers are given uh I think there were certifications as well I'm not sure but securium has issued nfts that show that here you have uh you know you've got this Satora knowledge and expertise right and there have been monetary Financial incentives as well foreign [Music] guys come talk to us if you want to know more [Applause]