ETHWarsaw 2023: Jan Gorzny, Quantstamp - Lightweight Formal Methods in dApp Development

all right hi everyone uh we're you know the last talk so I don't blame you if you want to walk out but uh if you do stick around I will tell you a little bit about lightweight formal methods uh so my name is Yan I am a head of L2 scaling at quantstamp means I'm usually involved in a bunch of things like scaling Solutions and the the security of those systems but I have an academic background in um in a lot of things but one of the things I I like to study is formal methods lightweight for formal methods and uh as a security company it's sort of a natural fit and today I just want to talk to you a little bit about what lightweight formal methods are and how um how they relate to web 3 so it's a bit of a a survey a bit of an introduction it's it's technical in the sense that I'm going to drop some buzzwords but not technical in the sense that there's any math on the screen or any proofs uh you know there's no code nothing like that um and then the sort of second half of the talk is sort of like a call to action so if you're looking for something to do this weekend um at the hackathon it's a particularly good topic so first I'll give you a quick introduction and if at any point you want to download the slides you know the link is there it'll be up throughout so why why do we care about um formal methods or security well I think the obvious answer is that people have gotten screwed pretty hard here in this space right this is these are some headlines that are kind of recent I think there's some older ones uh you know this is stuff stuff goes wrong all the time in crypto and this is true uh in sort of the public sphere and you know it's it's very common in in sort of everyday knowledge that that crypto has kind of got some risk in part because of these hacks but it's also been studied academically and and there's a lot of work going into trying to figure out how to um overcome you know these issues to learn from them and never make sure it goes on again and unlike other software development uh sort of areas or domains crypto is actually pretty good at adopting some really strong tooling for this which generally is referred to as formal method so it's a way to prove you know mathematically that some properties of your system hold and I'm not going to go into a very formal definition of about that but you know if you've been in the space for long enough you've seen you know at a bunch of conferences people will regularly get up on a stage and say Here's how to sort of prove something uh they can't show the whole thing usually because it's a very complicated process very slow it requires a lot of expertise but things like theor improvers static analysis tools symbolic execution things and even lters are really prevalent in this field more so than other fields and um this is largely in part to the fact that you know you deploy smart contract on ethereum or most other blockchains you can't change them they're there they contain a bug and if they contain lots of crypto uh someone's going to try to exploit that bug in order to take the funds out of that contract so to prevent this you know you want to be as sure as possible as you can be um at the beginning of the deployment so priori didn't deploy you know you try to prove that everything is correct and and that's that's the that's the dream uh it's nice you know in some settings it definitely can be done uh you you know in crypto it's a little bit easier to because you have bounded execution right a transaction cannot run indefinitely long in ethereum you have a gas bound and therefore a number of steps it can take and so the search space of proving you know if there's a counter example is also shrinking doesn't mean it's easy it doesn't mean it's sort of quick um in fact most of the time it's still very expensive and very much requires domain expertise you know usually you have people with phds you know sitting down with you and saying here's how I'm going to model your system formally and here's the property I'm going to try to prove and then they're going to go put it into some custom language that you probably never heard of and then they're going to you know come back with a result saying actually you have a bug here or actually we think it's fine there's a lot of caveats there though because uh even when they do that that's a manual process more or less like most of the time there's some tooling that can automate parts of it but if they get the specification wrong they've just proved something wrong and that's that's not ideal so it's very important oh I think I got to I guess be more active I need a password over here sorry sorry uh I'll click through much more quickly um yeah so typically you know the these systems are still Out Of Reach of the average uh hackathon participant and and maybe even the average Dow because they're really expensive and they're really slow to do this so you can hire out or you have to hire like you can hire a firm or you have to like hire you know an expert an experts are expensive so um what I'm trying to say is is that great and it's really helpful but we also want to capture sort of the the less experienc and less technical people in in this space and one way to do this is we can add this this keyword lightweight in front of the formal methods and here the goal is not to formally verify that the entire system is correct but that very specific functions and properties hold um and so you're going to abstract away a lot of the system and you're not going to prove you know everything is Totally Secure but maybe you'll be sure that actually there's only one way to withdraw something from your from your contract and if you can do that that would be great because then maybe there's a whole lot of other bugs but you know you know no one's going to rug pull you or no one's going to like exploit the funds and that would be great and to do this we we want to leverage a whole bunch of tooling from the software engineering community um usually there's tooling that's based on Sat solvers and& solvers I'll talk a little bit about uh sort of the high level of how those have been applied but not Define them unfortunately um and and they work by just reducing the problem to something mathematical and it's they very bounded so they won't prove arbitrary execution but because blockchains are limited you know the the transactions are are small in size it's often good enough you've probably already seen tools like this heard of them uh there's another slide coming up where I'll list some of them that you may have seen if you've been in the space long enough um and I think it's what I'm trying to say is that really this is the approach to take because while proving everything correctly is very very nice and expens very nice and and you know great it's also very expensive uh it would be great if everyone could do it be great if everyone could learn it and be great if everyone you know could take advantage the reality is people won't and so why not Leverage The tooling that the community is already kind of built again this will come up in a slide and do this in only small small bits and you can even like decentralize parts of this verification if you really want to that would be a technical problem but you know you could you could spread the workout and most importantly you could make sure you're sure of certain things certain things that your users really really really care about and although we've started taking advantage of this in the web 3 space using smart contract analyzers and things like this I'm going to show you that there's a whole bunch of other places that we can use this and this is uh you know probably a great place to hack on something if you if you need ideas so before I go any further I said I won't won't Define formal methods I probably should have but I didn't I will definitely Define lightweight formal methods very precisely so what I want to say is that develop things small and incrementally care about the properties you you want and this is a definition from Daniel Jackson he's a professor at MIT uh he's been doing this type of work for for 2012 he's got a great book on some tooling but just focus on the parts that matter in your code so don't try to prove the whole thing in the same way that when we get an audit as a security company most people don't bring us their front end because if the front end sort of goes wrong you know you can fix it that's that's totally fine you can't change the the smart contract in this pure smart contract sense there's probably also parts of the smart contract that maybe don't matter quite as much as some other parts right there are probably some convenience functions there's probably some view functions there might be some things that you know are nice to haves but if they go wrong your system's not going to break and you're using aren't going to be totally upset with you they'll just be annoyed and obviously you don't even want that but one is definitely better than the other right being annoyed is better than being you know really really angry at someone so don't throw away the tooling don't throw away all the math but just focus them focus them a little bit get them down to a scope where you can do it in a couple of of days or hours and that would be really really great and it won't prove everything but you'll be able to find very very local bugs and this is great because you know you're still making quality improvements to your code I mean we see things all the time where we don't have you know even specifications or tests this is still you know well beyond that you probably need those things first um but even just proving that particular behaviors work right this was I was talking about specific paths like withdrawals this would be the place or technique to use it right so you don't have the whole system necessarily working as function but you have one property and then once you have that one property you can also you know consider the next property if you have withdrawals well now also check deposits and see what happens and if you can do this at a at a level that's more you know abstract than the code itself you can actually get a lot of wins from the tooling I don't have the numbers there to prove it to you but really what would be great is looking at the specification because often we get like most of the bugs we find in client code is not reentrancy it's not you know math errors we see those sometimes probably often but uh what we really see is people thought they wrote a Dap that does something and then it it doesn't do that for one reason or another either because their specification is wrong or because there's some conflicts at the end of the day and while some testing will catch that if you can prototype that really quick at the specification level before you write code and say look I have two features and one of them is going to conflict with another uh or with the other then just don't build it and now you saved yourself a whole bunch of development time and if you can do this in 3 or 4 hours you know you've possibly saved yourself hours of auditing time not to mention you know days of development time potentially and when you get to an audit you also have additional artifacts to show your people that actually we knew what we were doing and we know what we want you to be doing so this would be great and this turns out to be less costly and often it can be more accessible so bear with me as I'm still flying at a th feet here but I'll give you some examples right now uh most of this will come in the form of symbolic execution you've probably seen some tooling for this already if you're a developer if you're not a developer you can check these out um you know re-entrancy was a cause of major issues so there's a lot of tooling to capture exactly that right and that's a good starting point because that's a nice property to be able to prove and say oh I have no re-entrant functions and there are to Ling to catch this so you know there's a bounded model Checker there's mantore or an slyther is really good slyther is probably one of the best tools out there to catch things uh and probably all three of those except slyther all the first three use a SAT solver so this is sort of a general purpose mathematical solver at the end of the day and it works but it doesn't give you a proof it doesn't say this will definitely never happen it just sort of says I didn't find it now or I timed out and usually that's good enough uh if your program's small enough it will give you an actual proof but typically you know for a complicated D5 protocol it's it's not going to do that depends what you're trying to prove though of course uh but but you know these tools exist and that's the point most of them are non-trivial to use um so there's usually uh push button so you can probably download that you know you aren't install or whatever and I think it just works out of the box they've done a good job I haven't actually used uh the bounded model tracker here but if it's a bounded model cheacker and you're writing your own properties to prove it's going to take you a little bit more time doesn't mean it's not worth considering and like I said the goal is really trying to use this in addition to your other things so what you want to do is you know make your test as good as possible it's always difficult now it's very rare that we see clients that come with 100% test coverage because most Protocols are very very difficult and so instead of you know trying to capture 100% test coverage you can spend resources somewhere else because often when you're writing a test uh sweet you have diminishing returns on on getting that last you know 5 10% in coverage you know the first 80% is really easy the other ones are are much more difficult or you got to mock up things or things you know need to be in very specific situations that you're almost coding for and expecting to never happen um but you would like to have some Assurance of that writing uh a model for your specification for those Coral cases might help you do that a lot quicker uh and because most of them are almost push button button but not quite uh you know it's less time right so if you can learn how to write a test Suite you can probably learn how to do this might take you a little bit longer you might not see the value at front but if you start to see you know how it can guide your development not just your your sort of correctness checking you might actually really like to love it uh and and more importantly um you know you can help contribute to the ecosystem with these tools so these tools are often built at hackathons exactly like this or they're you know enhanced or you can do things like formally model other systems at these hackathons and I think that's really really interesting so there's there's not a lot of um daps out there for which you can say what is this actually doing what's the specification uh there's probably a couple I think maker does this but most of them you know when you look at the the code you don't know what it does so unless you're willing to sit down and read all of their solidity code and maybe their documentation if they have some it's it's really painful but if you can do this exercise even as part of a hackathon um then you could also check its correctness and you have additional documentation that your users can read and if you target the specification level you know you're you're doing it in such a way that no one's reading variables of a specific type and size it's just here's the flow of what's supposed to happen and here is a variable and they don't need to be specific I'm sorry I was just about to hit the next slide I need work okay good so how can we actually you know do this so I've already hinted at one thing which is um building this type of tooling and and process into your specification design um you still have to take a lot of my a lot of my stuff at face value but um what else can we do so first I want to caveat this with no matter what you do here it's not going to be a silver bullet it's going to take time and effort and it's probably not going to be a push button solution that works for every dap everywhere and certainly it's going to be not a silver bullet right so you you can't just say I spent 4 hours writing my model why isn't you know everyone convinced my stuff is correct it's not going to be the case um you're still going to need those tests because if your model is too far uh removed from your code it's not a very helpful model uh ideally you know it's it's close enough that it's meaningful but far enough away that you can prove something useful on it uh and you'll still need code audits because both of those things can still go very much wrong and you know therefore you want to be sure absolutely sure that you've got everything so audits and tests are still absolutely critical but since you know tests maybe guide your implementation and audits are definitely the last line of of sort of defense for most people because they come when the everything is developed um doing this type of exercise helps get security from the Forefront right so from the very first you know thing you do you can be more sure that your application is going to do what what uh what you wanted to do and then when you go to get an audit like I said you do get one extra piece of artifact back to share with them um and so you know can we use these methods to do better absolutely and do we need to mostly yeah if you write me uh an implementation of an erc20 token you know if you're still building tokens just tokens that probably doesn't need to be modeled I think everyone studied that interface well enough and it's pretty simple these days if on the other hand you are doing something very new with uh Bridges or defi or rollups or whatever it is uh where you have lots of moving parts and lots of variables that you can't track you need some level of abstraction anyways right most people can't just Speck out a rollup on a whiteboard no one can do that what they do is they draw a components and they draw lines between them saying there's interactions and flows that's just the model right so if you do that model slightly more formal that's where you get these wins and you know if you do this you can do that feature interaction I've talked about the existing tooling that this ecosystems already using has been shown to do this in other areas of software engineering so there's a call to action here to just read those pap papers which are kind of dull software engineering papers are not exciting bring those over to web 3 you can get a new analysis tool very quickly is it going to solve everything absolutely not but if you can prevent one $500 million hack you're doing the ecosystem a great great fail uh job or great benefit um alternatively you know there you can look at other things uh so things like software product lines what we're seeing now uh is that everyone is building one piece of code and then they want to deploy it you know everywhere or at least that's the sort of claim and and and joy of evm equivalent rollups you you build one piece of software and solidity and you say I'm going to put on CK sync I'm going to put on scroll I'm going to put on whatever I want it to be as long as they take my solidity it should be exactly the same but there there was a talk at L2 Warsaw uh yeah L2 Warsaw yesterday where we saw that actually everyone tweets op cod's a little bit different more or less it's you know we haven't really reached exact exact equivalents maybe there's one chain or two chains that do it but uh a little bit of a change can have a big impact on how your code is run so you you you write it you expect it to be exactly the same but it's not the case so instead you could build your software in a way that's sort of it's a product line where a feature is supporting you know ZK sync or supporting scroll or supporting whatever it is and then oh sorry I need you sorry I'll just try to keep touching it um it's almost done anyways uh so if you build it as a software product line then you can catch these bugs right away and you can have actually your your code configured by these tools so you have you write a library that's like this is my you know withdraw meth method that definitely works on ZK sync and you know over here is is a withdraw method that definitely works on on that on our scroll uh and you have the system to configure which import to to to import um inside your your SDK that's also really cool big companies do this all the time companies like auto companies and tele telecom companies they do this all the time because they have to deploy on a whole bunch of different you know specific sets of Hardware depending on say the car uh and different user configurations why don't we start doing that like why is everyone still just building it once and assuming it's going to work all the time uh you know it is the pipe Dre that's nice but I also think that in 5 years we're going to have a whole bunch of chains that don't look like the VM evm at all they're going to have their own stuff right we're seeing things like Risk zero come up people are going to want to deploy the same code elsewhere it's going to require different languages or at least different implementations within the same language at certain times so to get into this practice now you know if you've got nothing better to do this is this is great would be absolutely good and the last benefit we get from targeting uh specifications and product lines and all the sort of high level abstractions very quickly is that it scales a lot better right you can look at a 100 models which now each model might represent you know some implementation of 200 to 500 lines of code and suddenly you can reason about that whereas you know reasoning about 100 times 100 lines of code inside of a solver directly might not be possible so you get scaling benefits which is which is really really nice and and so I've already said yeah some people can do better we can also do better in other ways um there's been existing research that shows using these tools you can generate test case automatically wouldn't it be great if you wrote solidity and you just had test case automatically spit out are they going to be perfect absolutely not I don't think there's any research out there that says they're they're perfect but I haven't seen this at all in web 3 please correct me if I'm wrong if you know of a library that does this by all means but the same type of underlying ideas and Technologies can be used exactly for this so um this is even more straightforward perhaps if you can build a tool um which is not going to be at all this is you know it's a big task uh generating test cases automatically would save a lot of people a lot of time right it would be helpful and then they just have to go refine the the the test cases and and make it better but um you know it's still better than than nothing so again boring ideas from other places and then once we get to that point where we have all this nice tooling which would be nice and it's probably going to take a couple of years but you know I'm here dreaming and I I want to inspire you guys to be dreaming uh we can also you know go the other way so This Is Us boring previously I was talking about how we are boring a lot from the software engineering community and I think that's that's really good and we shouldn't discard those ideas but once we know how these tools work in our domain we can start going back the other way too right we can start saying here's how you model things really nicely and here is how you get specific operations in these tools to work a lot better uh and when you do that you contribute back to how these tools can be optimized and now there's a feedback loop where you know they develop an idea we implement it we get better techniques we give it back to them they improve on the idea we develop better tools and the process repeats and eventually we have everything we want sort of in in some reasonable sense again we're probably never going to be able to prove full system completeness for a lot of systems but you know in in a lot of places we have really really really good tooling uh and then you know the next most popular thing probably other than n nfds is is zero knowledge so zero knowledge proofs are um you know massively complicated most people definitely can't do that on the board even if you could do a rollup uh I know a very few people and most of them have phds who can actually you know get up and and and write down the proof system and the constraints or at least the structure of the constraints um they're so big and so complicated that here we don't have a choice but to use automated tooling to do this if someone says I've written a circom circuit can you tell me if it's correct I can look at the circom code and I can say oh I think it is but if I don't trust that circom compiler I'm actually not really sure that I trust the code at all so I have to look at the code that outputs but the code that outputs is just a bunch of constraints and I can't look at that because I don't have enough time in my week to do that right two to the 19 is also probably too much more than you know my my lifetime or at least my my work life balance lifetime so you know at some point you need to have automated tooling anyways and one place that's really really underdeveloped is any type of tooling any type of tooling inside uh a Zer knowledge proof framework so we've developed one tool I know there's a couple out there that are other um they require sort of fundamental sort of modules inside the tooling that I've been telling you about these sat solvers smt solvers but uh at some point we're going to need them because we won't be able to manually check zero knowledge proofs so you know why not why not start looking at tooling now which thankfully I guess we are but we need a lot of help there there's a lot and there's going to be you know probably a dozen more proof systems coming out in the next I don't know how many years right the number of papers for proof systems is already high so as soon as some of them get popular we're going to see a lot of problems with uh with detecting them with the existing tooling and we're going to need help you know and then it also means we're going to need a lot of help in Improvement so there's things you can do better this is I promise you no math but there's a little bit of math here uh you know the the idea that once we actually build these tool Lings they need to be optimized they need to scale if you think scaling to you know a million lines of code is hard scaling to two to the 19 constraints is is even harder and you need to do you know a lot of clever stuff so if you're more mathematically inclined this is also for you um but it's the last talk I want to leave a time for questions because I'm I'm sure I skipped a bunch of stuff and people have have some questions uh you know we've the community is already doing really good at formal methods I'm not here to say don't do formal methods uh if you can afford formal methods and your project is valuable enough to do formal methods by all means do it probably don't need a for nft if you're doing Defi and you can afford it absolutely but there's a middle ground right there's a middle ground where if you're doing something that's only kind of valuable maybe or kind of complicated you can do formal verification on just parts of the system and when you do that you drive the cost way down you get your insurances way up because you still get some things proved uh and it's going to be a lot cheaper it's going to be a lot quicker so I'm encouraging everyone to try these unfortunately what I haven't given you is a whole bunch of tooling for this I listed some things there this is the call to action part right there's technical challenges and a lot of the tooling doesn't exist but if you have interesting you know software engineering ideas to Port over in this space I think you will get so so many users it'll be you know great uh then the challenge will be keeping up with with the tech and and scaling in all it so I'll stop there uh if you got questions for me and I don't get to you here or or you can't think of them now please you know contact me um and Quan snap is mostly a security company but occasionally we do some research and grants so check out our our grants from the ethereum foundation on the bottom right there we talked about L2 block Explorer apis and uh L2 security assessment which I talked about yesterday if you were here so I'll stop there great thank you very muchan any questions um we see that qu stem does a lot of uh things but do you uh experiment somehow with AI in securing uh code we experiment yeah I I don't know what I what I can or should say um you know it's it's a very new area and obviously on Twitter there's like a whole bunch of things about you know let's just plug chat GPT into something um the the privacy concerns about that are not something that we we take lightly so uh you know I don't think we're uploading just code to an arbitrary thing where people are going to learn uh from their from our code but we have been exploring different local stuff we have some internal tooling unfortunately I can't show you that uses some version of AI or another or or intends to in the future um so experiment yes do we have a product for it no I don't think so maybe you can say if it's mostly llm based or it's some other unfortunately I'm not the AI guy in the company if you send me a message I can definitely you know ask you to someone who has way more experience than that I think it's very interesting but you know you can only study so much in your lifetime and I chose not that great anyone else hi uh can formal verification do or treat the economic uh attack vectors yes so we actually have a tool for that uh we have a tool where we can formally model the system and and we it's not my tool again we got quite a few researchers where we we have a representation of of your D5 protocol and we can tell you if there's uh like a flash loan or Other M issues I don't know the numbers on the accuracy but it's pretty good we just launched it so ask me more about that offline than I can share awesome uh so if no one else has any questions then uh thank you very muchan once again see you tomorrow or on the Parker