Episode 284 - Using Formal Verification on ZK Systems with Jon Stephens

Transcript

[Music] welcome to zero knowledge I'm your host Anna Rose in this podcast we will be exploring the latest in zero knowledge research and the decentralized web as well as new paradigms that promise to change the way we interact and transact online this week I chat with John Stevens a computer science PhD student at the Utopia group at UT Austin and the co-founder of verdice a blockchain auditing firm that is increasingly specializing in ZK systems we talk about what led him to work on

Smart contract and ZK system security what tools are available to test the security of ZK systems and what the process of doing formal verification of CK systems is like we talk about some of the security vulnerabilities that could be found in a ZK system and then wrap up with a chat about disclosing security vulnerabilities methods to incentivize disclosures and some of the challenges that ZK brings now before we kick off I just want to let you know that the application to attend ZK Summit 10 is now open this time around we will be hosting our event in London and this is happening on September 20th as always we aim to bring together the top researchers and Engineers working in ZK to share their latest research and new findings check out the show notes for the application form please note spots are limited and only folks who have

applied will be considered to attend hope to see you there now Tanya will share a little bit about this week's sponsors polygon Labs is thrilled to announce polygon 2.0 the value layer for the internet polygon 2.0 makes Mass adoption possible by offering users and developers unlimited scalability and unified liquidity this mission is fueled by groundbreaking ZK Innovations including a first of its kind ZK powered interoperability protocol and the next generation of the industry-leading and widely adopted plancky II proving system polycon 2.0 will change the way we experience web 3 by bringing the security and decentralization of ethereum to the scale and usability of the internet itself polygon 2.0 and all

of their ZK Tech is open source and Community Driven reach out to the polygon community on Discord at discord.gg forward slash zero X polygon to learn more contribute or to join in on building the future of web3 together with polygon anoma's first fractal instance nemata is launching soon namata is a proof of stake L1 for interchain asset agnostic privacy namata natively interoperates with fast finality chains via IBC and with ethereum via a trustless two-way bridge for privacy namata deploys an upgraded version of the multi-asset shielded pool circuit otherwise known as masp which allows all assets fungible and non-fungible to share a common shielded set this removes the size

limits of the anonymity set and provides the best privacy guarantees possible for every user in the multi-chain the masp circuit's latest update enables shielded set rewards directly in the shielded set a novel feature that funds privacy as a public good follow namata on Twitter at namata to learn more and join their community on Discord discord.gg forward slash nomada so thanks again to Noma and now here's our episode [Music] today I'm here with John Stevens a computer science PhD student in the Utopia group at UT Austin and a co-founder of varadise a blockchain auditing firm that is increasingly specializing in ZK systems so welcome to the show John hi good to be here I feel

like this interview and basically this topic that we're going to be covering which is like Audits and ZK security ZK circuit security it's coming at a really important moment in our industry right now we're seeing so many ZK systems move from the theory or proof of concept or testnet state Into the Wild and the issue of ZK security has been raised but I don't know that we as an ecosystem yet have like a rule system or like a sense for how to address this so I'm very excited to explore this with you yeah yeah I I think this is a really interesting topic and I'm excited to you know chat more about it cool let's first understand a little bit of your background as I mentioned in the intro

your student at UT Austin tell me like what were you studying before this and actually what is your PhD focused on yeah so my PhD focuses on an area of computer science called formal methods so this is kind of a a sub area of programming languages that focuses on how do you reason formally about other software and so this includes you know designing tools that are capable of looking at other software through you know techniques like formal verification or static analysis so basically the way that this got started is during my PhD one of the tools that I developed was a tool called

smart pulse and that would verify formally these types of properties called temporal properties within smart contracts so basically that that is where we started is we start by looking at this particular smart contracts or particularly solidity contracts because you know we were noticing that there were a lot of attacks in this area and that auditing at least is a very manual process coming from formal methods it seemed like in order to increase the quality of this particular ecosystem and hopefully prevent some of these attacks more tooling should and could be used and so we basically took this work as well as

some other work that were done by was done by some of my other co-founders and kind of wrapped that up into this company interesting I did an episode many years ago with Martin loonfall from maker at the time he was part of the maker Dow engineering team I think I think he's moved on to other things now but um he had been doing sort of this formal verify or like was exploring formal verification of solidity contracts do you feel like did something happen in the solidity landscape that made it so this all of a sudden was more viable or could it always have been done do you know about this work at all like had you seen previous work on formal verification of solidity code yeah so at least when it comes to formally

verifying solidity code there had been quite a bit of work even when I published about you know performing formal verification in that space however part of the issue is uh a lot of these tools including mine is a research prototype and so that means that it's not really production ready so for example one of the Annoying parts of my tool at the very least is due to dependencies it was stuck at solidity five and stuff like that and so there were a lot of other tools that had been created that you know were just in a research prototype phase and weren't ready for anything production ready and so a couple of other companies like uh sartora for example took a verifier that they worked on and as a research

prototype and actually expanded it so that it could actually be used for verifying real solidity smart contracts and so there wasn't really anything that changed that would have allowed this it's just there needed to be more work put in because solidity has some really annoying design decisions like uh you know dynamic call resolution and stuff like that which makes formal verification very difficult but not impossible and so for that reason really there wasn't anything that changed it's just people started putting in more effort as they were able to tell that oh people in this ecosystem do actually

want to use tools like this and without having to actually perform the formal verification themselves that's cool I think it's worthwhile to redefine formal verification and how that actually works right because I I sort of want to understand like you built this tool but like yeah what would this tool actually look like or how would one use it with code so let's first start though what is formal verification okay so just to give a little bit of an overview about formal verification um basically what formal verification does is it reasons very precisely about your program in order to validate that you know any particular input is going to satisfy some logical specification

and so this logical specification can take in a number of different forms so for example it's typically an equation over program variables so you might want to validate for example that you know if any particular input is given to this contract then after you transition to this state you can never transition away from that state so for example let's say that an auction has been completed an auction for a solidity auction I guess and so normally there they have some sort of gating where they say the option is going to become complete and once that happens you don't want to open the bidding again most of the time and so uh for that reason you might want to verify

formally that yes there is no combination of calls to your contracts that could allow people to bid again in that episode that I did many years ago we talked about like formal verification the trick was you have to specify the exact Behavior you're checking it for it's not going to necessarily notice bugs that are like outside of that behavior like if that auction software had some like when it starts or like some other part that you weren't formally verifying the formal verification would not catch that it will only capture that specific behavior right yes that that is true however one thing that I'll note is when you're formally

verifying you're doing it with respect to a specification and so if something is completely separate from your specification then it won't be caught by formal verification but one interesting thing that we found during this paper that I published is you can actually end up finding really interesting attacks that don't seem to be related to your specification but are so for example some of the attacks that we ended up being able to find in this paper that I published was uh without actually specifying I want to look for something like an integer overflow or a re-entrancy attack the verifier would be able to synthesize counter examples that

corresponded to these without having to be told you need to do X and so while it won't find something that's unrelated to your actual specification I can still find some pretty powerful attacks and pretty powerful zero days without having to be told to look for it so it's a it's really interesting and a little bit different than how people typically go about this the interesting part of it is it's not just going to look for a particular type of vulnerability and I don't know I guess one of the interesting things that we found during the evaluation of this paper is you might have something that says like a user can always withdraw their funds or something like that and then basically

what the formal verifier will do is it will try to figure out a way to steal funds using any method that it can from that contract and so it ends up creating some really interesting and odd counter examples that you might not have thought about otherwise interesting though I so this is sort of surprising that it sort of can find things past what's been expect for I guess I'd always gotten this impression that it was a very precise testing tool but a very limited one it depends on how you perform formal verification and exactly how much you kind of constrain the problem and so for example if you're testing by or if you're only trying to verify pre and post conditions or something like that

where a precondition States the assumptions about the contract before execution and then the post condition is going to State what should hold after you actually execute that function it it's not going to be able to find some of these attacks that I was talking about before because it doesn't necessarily or depending on the architecture of the verifier it won't necessarily try to manipulate the state of the contract in order to find ways that are within the precondition that can still violate the pulse conditions so the verifier that I created was actually very flexible in that it used a specification class called temporal specifications which basically State Properties over time and because we were using this very I guess flexible but particular specification language it was

able to find you know attacks that required a series of transactions or that even would require fallback functions to be synthesized and so it was really interesting and so it depends largely on the the verifier that you're using because you know people say formal verification a lot but even within formal verifiers there are different ways that you can well build them and uh different specifications that can be provided you mentioned a paper what date did you publish that like what what era are we talking I think it was either in 2020 or 2021 so I think that the paper was actually published in 2021 but was

accepted in 2020 if I remember correctly and is that paper was that the thing that kicked off Paradise or did that come later so yeah it was part of what kicked off Paradise so Paradise started in well I guess a little over a year ago now and so basically what happened was I had published this paper and at the same time ishel my advisor was visiting yufeng who was her former PhD student who's now a professor at UCSB and he also had in parallel been developing some you know other techniques in order to find bugs and smart contracts and he

had been approached by some VCS about you know the possibility of making that into like a security company and so uh those two got pretty excited about it and asked me if I wanted to join and so yeah that's kind of how varadise got started I see this actually makes me want to ask sort of we were talking about one tool in the auditor's toolkit right the formal verification tool but what are the other tools that are out there and that you would be using maybe in tandem there's a lot of tools that are available for Auditors formal verifiers aren't used very frequently because they require a little bit of

expertise because you have to know about the formal verifier in order to kind of provide extra and variants and reason about why the formal verification might not have gone through and so some people find that very frustrating okay and so the most commonly what's used by I would say Auditors now are in this particular domain are fuzzers and static analyzers and so what a fuzzer is going to do is it is going to randomly generate inputs to whatever your program is if it's a smart contract it will randomly generate transactions and inputs to those transactions and then feed them to your program and so what has been found is in a lot

of different areas like operating systems they were able to find that fuzzers can find very interesting and deep logical violations or violations within your your program because they they generate weird inputs that people don't commonly think about and so but that could happen in in the wild but that could happen in the wild and that and that's the the point is typically the the things that get exploited are not what programmers are thinking about or developers are thinking about it's these other uh these other side effects and so fuzzers are a very powerful tool but the problem with the fuzzer is they they don't come with any sort of guarantee everything is generated purely randomly and they they kind of have this

probabilistic guarantee that eventually if you run them forever they might Converge on a particular solution and so if you compare a fuzzer to a formal verifier a formal verifier is like you took a fuzzer and you ran it on every possible input to the program and validated that the output was correct and so you know technically that's not possible but a fuzzer on the other hand is just going to provide random inputs and so they can be very useful particularly when you're performing something like property-based testing where you want to provide random inputs and check a particular property after each particular test was run by the fuzzer and is static analyzers in a

similar category to fuzzers or is it its own thing yeah static analyzers are its own thing so what a static analyzer is going to do is it's going to reason statically about a particular program and so there's a couple of ways that you can do this you can look for particular patterns within the program so for example if we're talking in the ZK domain one thing though static analyzer might do or a very light static analyzer might do is it might look for instances in circom where people are using the single Arrow assignment in order to assign to a signal right so that is a very light static analyzer that just takes his input the source code it doesn't run anything and it reasons kind of abstractly about the

program itself and so the nice thing about static analyzers is similar to formal verifiers they can come with guarantees because if they aren't able to find a particular pattern or whatever they're supposed to it's guaranteed not to be in that program ah that example you just gave would that have been a bug that it's looking for or like something that causes bugs basically static analyzers are going to be looking for specific types of bugs and so this would be they already knows look yeah this is a bug that they already know of and so static analyzers unlike with uh what I was talking about with the flexibility that you can get from formal verifiers they are targeted at looking for a single thing normally and so they're again

different types of static analyzers that can go all the way from I'm just going to look for the single syntactic pattern by just looking at the program itself all the way down to I'm going to reason in an abstract way about the program itself and maybe prove something about the program itself over these abstract semantics I want to now go back to like what does a formal verifier look like or what is it as a piece of software so the way you've sort of described this like you have a piece of code you have a program or a circuit or something you've written and then you kind of like do you feed it into it or do you set the formal verification upon it like I'm just curious how these things interact no I I

like you you set the formal verifier upon it so so you've got you've got the source code and what the formal verifier is going to do is it's it's going to reason very precisely about the semantics of the programming language in order to prove something about the software and so there's a couple of ways that you can do this but essentially what a formal verifier is going to do is it's going to take as input your actual source code as well as a specification and so this is just you know the The Logical formula over uh the program that I was talking about previously that's going to go into this let's just call it a black box for now which is the formal verifier and what is going to spit out at the very end is it's going to say yes this was verified and or no it wasn't

and in the more frustrating cases it might say I'm not sure and then you then you have to go and try to provide it with a better more proper invariance in order to get that formal verifier to actually verify and you're going for you want it to come back with yes it's been verified yes this does what you're supposed to do I'm curious about the code in the program that you're actually putting into it does it always have to have a certain structure like when you create that black box are you only making it for certain kinds of contracts or certain kinds of programs yeah so so typically it's parameterized on the actual language that the contract is in so for example typically you I mean

there are ways around this but typically you write a formal verifier that knows about the semantics of a specific language and then after that you can Eden any particular program within that language you want okay however one thing that people typically do to get around this is you could you know have a language that the formal verifier knows how to reason about and then translate from other languages to that one and as long as that translation process is sound then you will be able to formally verify on whatever can translate down to it okay I feel like this is a total place for bugs or some problem like at the compile are you compiling are you translating you know compiling and translating kind of end up being this a similar thing

because the compiler is just going to compile down to like a byte code right and so here uh let's just call it translating because typically you're going from like a high level representation to another fairly high level representation and so um it's kind of a translation Pro one but for example the move prover is built on top of this verifier that operates on Boogie and so it's fairly common for people to uh rather than Implement their own verifier because that is a lot of work and it can be quite hard they will instead translate down to a verifier that they know well and that is fairly mature because you know there can also be bugs in the verifier I want to just

check so when you say move you mean like the language move the one that was developed by the Facebook group okay or man and the verb you just call it a boogie verifier is that the name of this yeah Boogie is the language that you translate down to and Microsoft has created a verifier that will verify properties that over these Boogie programs that's interesting though and actually maybe for our audience too when we're talking about prove or verify her we're not talking about in the ZK context at all of the code and the verifier of the of the program yeah this is the the struggle of my life his verifier is too overloaded uh context you've got approver and a verifier for formal

verification you've got a verifier wow and then also when it comes to and this is what we've encountered in defy in particular people call the process of validating that source code and byte code matches they call that verification and so oh wow no matter what we always have to clarify because it just gets too confusing I think we've done a pretty nice mapping of formal verification formal verifiers and some of the other tools fuzzers and static analyzers this is the auditing toolkit but all of this so far we're still kind of thinking about it in this solidity context or like smart contracts or even I don't know maybe it goes past that but what I

do want to understand is like where for you did this move to ZK happen and obviously down the line I want to understand if it changes anything but yeah maybe let's start with the story yeah so uh the move to ZK happens when uh we were you know doing stuff at Veritas so basically at the time we talked with the developers of circom lib and they wanted to perform some formal verification over circon lib and so that's where that's where varadise got involved and some of our employees went and they actually now have developed a separate formal verifier specifically for ZK but I'll skip past that for now

basically uh they perform some formal verification over circom lib in order to validate that certain properties held and so they performed some formal verification over if I remember correctly it was specifically the big End Library within cercomlib and ended up being able to identify a couple of bugs there but you know more importantly verified other properties held can you say the name of that Library again yeah so the the big integer Library okay okay the first time I heard about Paradise was I think we mentioned it really briefly on an episode with Uma from succinct and John yeah yeah we were talking a bit about the security of these systems Bridges and all of these

things and they had mentioned that you were doing that so you were first brought in to do this on circum and this is where maybe you could help tease this out like are you when you're doing this still focused on the language so like you're talking about circom but I mean there's a lot of languages in the ZK space there's also like different levels of a stack so I'm wondering like when you deal with circum would you deal with the formal verification of the entire like all levels of circom and libraries it draws upon or would you just focus on that yeah so for uh something like a formal verifier typically you have to assume there's trust somewhere and so when it comes to formally verifying something over a

circum basically you trust that the semantics of the language is implemented correctly and so in this case for ZK that means that you're trusting that the verifier works properly as well and that it's actually performing that verification in a way that's consistent with the semantics of the programming language because otherwise without that trust it it causes the already fairly intensive job that is formal verification to become you know even more intensive and so typically whereas previously when I was talking about performing formal verification over solidity it's a little bit I would say easier in a way because you know you

don't have to worry about what is constraints and what is going to go into your witness generate whereas when it comes to performing formal verification over something like CK you need to make sure that you're only performing formal verification over your constraints because those are ultimately what's going to be checked and so there's a slight difference between how the formal verification is being performed in this ZK space Ah that's interesting I want to understand so like you do the formal verification over circum I'm trying to use your lingo here over circum the language let's kind of figure what this actually looks like so you've

written a program in circum using sarcom yep and now you're going to set the formal verification upon it so you're not really checking the language so much you're just you you know like the formal verifier knows the language and now is looking for what's it actually doing with the constraints what's it looking for Yeah so basically the way that this is going to work is like you said you've got a program that was written by some developer and so the formal verifier at the end of the day has to know the semantics of the language so it is going to reason very concretely about the program itself and what it's going to check is it's going to check to see whether anything that would violate the specification is potentially possible

and so this violation could is not specific to being under constrained or over constrained instead what you have to do at that point is you have to write these properties that you want to check like whether a circuit is under constrained using a logical formula and so for example uh when it comes to expressing whether something is under constrained basically what you say is for every input there exists two outputs such that the circuit will take in the inputs that you provided it and what you'll get out at the end is an output and then you have to check and make sure that it is only possible for those two outputs that you defined to be the same

because if they're different then you have found an under constrained circuit and so that is essentially how the formal verifier goes about checking to see whether there is an under constrained circuit but it's it's not necessarily configured to look for this one problem hmm can you actually I really like you describing this because the under constrained problem has never really been cleared like I don't know what the outcome was so you just said it um but I missed it a little bit so if something is under constrained you're putting in an input you're getting do you say two outputs yeah so so basically at a high level what you're doing when you're checking for an under constrained circuit is if you can provide it with a single input however there can be

multiple assignments to the output and so greater than or equal to two then your circuit is under constrained and so the reason why this would happen is because there might be multiple ways to satisfy your constraints because really what you're doing at a high level when you're working with these EK circuits is you're providing it an input and you're saying I know an assignment to these outputs right and so if you can provide it to conflicting assignments to those outputs for these particular inputs then all of a sudden you now have an under constrained circuit is this similar to like a collision yeah okay like you have you're expecting one input equals some output and here you actually have like multiple inputs that will equal the same output right because the system is under constrained

right so you can say that it is kind of similar to a collision when it comes to a hashing function with a hashing function it can't be um avoided because you know counting but at least when it comes to specifying a proper hashing function you have to make sure that it is fairly well Collision resistant because with a hash function if you have something that commonly hashes to a single value then at least in the space that we're in that would break a whole lot of software and so here basically what you're doing is kind of the same where you need to make sure that for every input there's a single possible output there are reasons why

people wouldn't want to do that I guess but most of the time that we've seen these circuits from people making making sure that circuit is properly constrained or deterministic is another way to consider it is an important property that should hold hmm there's such thing as over constrained yes so that is a good question uh that is something that we kind of debate internally at verdice every once in a while because we used to uh kind of provide or Define an over constrained circuit as well where basically an over constrained circuit would be one where your witness could generate valid valid

outputs that would not be accepted by your circuit and so you can claim that that is an over constrained circuit however in a lot of systems when you add a constraint into or when you add a constraint a similar assertion will be added in your witness generator and so you can kind of say at that point that in some of these languages you can't possibly create over constrained circuits because your witness generator would crash however I at least am on the side that you can create over constrained circuits because sometimes something else is generating your witness and so yeah is there when it comes to sort of the under or or over or perfect constrained systems is there a trade-off

with performance is there a reason like are you kind of looking for the cusp where it works but if you go too far you're actually also like potential I don't know make maybe making the system too slow or too energy inefficient and so often people are trying to find that Razor Edge where it's acceptable but not and not under but also like not too full yeah that's a very good question and so the reason why uh these under constrained circuits actually occur pretty frequently is because exactly what you said people are trying to save constraints the reason why they do that is because proving time often becomes kind of a bottleneck and so they want to make their or they want to have as few constraints as possible so that uh

proving time will become quick and that is where you end up running into problems because they'll remove constraints that they might not think are necessary because it's very easy to make that mistake and when they prune that mistake or that that particular constraint they are now going to have an under constrained circuit and then that's a security risk oh I see yeah are there different levels of security risk do you ever have the result of like it's somewhat under constrained it's very under constrained yeah are there are there different levels or is it sort of binary it's either correct or incorrect so no it it there's definitely a range

that you can have right and so one of the most dangerous things is if you have a completely under constrained signal because that completely under constrained signal can now take on any particular value however we have seen other mistakes that people have made where a signal is partially constrained and so basically you've narrowed down the possibilities that the circuit could take and in terms of whether or not or the severity of the bug that often largely depends on the application itself because for example you might have an under constrained signal but in order to let's say find another value that would be accepted by the circuit uh

you would basically have to break some cryptographic protocol or that is being implemented by the the circuit itself so for example let's say that you have a hashing function and the um kind of making this up on the Fly here so I hope it makes sense so you might have a completely under constrained value but as long as it hashes to the correct value at the very end then everything is okay and so in that case even though maybe the input is completely under constrained because it is being fed into this hash function and that's going to be checked somewhere else technically if you or that's only exploitable if you're able to break that

hash function as well yes I guess because you'd have to be breaking both yeah so is there almost like mitigate like are there techniques that people that maybe I don't know if you've seen this where like people will do a really under constrained system and then have some mitigation on the side so really the only thing that we've seen them do is right now there are people who are trying to combine ZK circuits with um like the apps right and so one thing that they'll do is they might have some mitigation but that might not actually exist in the circuit itself and that's because they will have public inputs and all the outputs to the Circuit are always public and so when the circuit is

actually checked into the blockchain there will be some additional validation logic to make sure things are well formed so for example you can consider the case where there's a miracle Tree in order to validate that something exists in a miracle tree you're ultimately going to end up calculating a root but you know there's no way for the ZK circuit to know what the proper route is unless you've hard-coded it and so one thing that people will commonly do is any root will be accepted but then at least on the blockchain side of things they'll validate that yes this is the root that is stored on the blockchain and it will be rejected otherwise so you might be able to validate the circuit but it will be rejected by other

validation logic in this case are they checking actually at the input itself like is it at that step or is it the output is it like you wouldn't be able to feed in any input that isn't already a block header or something like they're checking something else or they're they're checking it at that beginning part yeah typically what I was describing here would be at the output so basically someone has generated a proof um when you generate a proof you know you have to provide the public signals and so they'll perform some additional validation over those public signals and so in the case that I described specifically uh the additional validation would be performed after uh the proof has been generated and so in that case if someone decided to let's

say try to perform an attack uh they would have to go through the entire process of let's say wasting their computation only for it to be rejected by the smart contract itself could you though do it also at the beginning like could you make sure that like there's only a certain set of inputs like it would be kind of impossible to just randomly pick one out of the air yeah so in that case um really if you're going to do it on the input phase the or at least I believe that you would have to have constraints inside of your ZK circuit itself in order to check things and so the only time that I've seen someone perform something on the input phase it's because they had let's say a trusted service that they would use and

that trusted service would generate a certificate that would then be checked by the circuit itself and so um the the problem that you have with doing things in the input phase at least is you have users who can interact kind of arbitrarily with the the witness generator and stuff like that so there there's no guarantee necessarily that they've been doing things properly and so really if you want to do something on the input side you would have to have some sort of trusted service I see so far we've talked about using formal verification to check for under constraintness but is there anything else that you're checking for yeah so

basically the other thing that you would want to check for is behavioral violations so for example the the reason why formal verification is so powerful is because you can check arbitrary properties under constrainedness is only one of those particular properties and so typically you know under constraintness is one of the I guess interesting properties that we end up getting in this aspect so it gets a lot of uh discussion however people can also just Implement things incorrectly and so uh so this is like checking for bugs in a way this is just like a mistake right and so logical mistakes are one thing that we commonly find during our audits where someone intended to you know write a logic that or writes a program that

did X however it does something slightly different than x and so the other thing that you would do with a formal verifier is you might want to check that someone's logic is actually implementing the computation that they expect and so in that case you would encode the computation that someone wanted to perform as an actual logical formula and validate that yes this logical formula actually holds over the constraints of the CK circuit and so this is something that we do commonly for our clients um and while it probably sounds like you have to write something twice that can be pretty powerful expressing the same thing in two different forms because especially if you find discrepancies

between those forms then you find bugs and that's what the formal verifier does in the case of ZK circuits though are you also running fuzzers and static analyzers yes so at verdice we have developed some custom formal verifiers which help us more efficiently be able to perform the formal verification because at least right now and we didn't really get into this there are ways that you can perform formal verification automatically but uh ZK kind of has some properties that make that difficult and so at this point formal verification is typically a manual process where you have to manually write out the proof and so we have some techniques that we use

in order to automatically prove things most of the time which is another paper that we have published at the same time we have developed tools that use fuzzing in order to help identify problems in ZK circuits by let's say randomly mutating outputs for example in order to try to find this under constrained violation that's something that we've been working on recently because if it can find a counter example that's great and then finally at Paradise we've also developed static analyzers in order to find bugs Within These ZK circuits and recently we're in the process of publishing a paper about the static analyzer that we developed which ended up being able to

to identify bugs and in real circuits that people are using that people are using yes is there an order in which you're usually running these things yeah like okay so what is that definitely for ZK so for ZK typically the first thing that we do is we would run a static analyzer because a static analyzer um at least in terms of the picture that we had it's just going to take in your source code and then it's going to tell you yes this is one rule or no this is a list of problems and so static analyzers are also very fast and so typically we first use a static analyzer then we'll use something like a fuzzer because again a fuzzer is very automated and at least the fuzzers that we use we try to

configure so that they can also do some property checking while they're looking for other bugs and so they can oftentimes also perform or find counter examples that would also be found by a verifier but they don't come with strong guarantees and then the last thing that we normally do is formal verification because with formal verification it requires more manual effort um so I kind of can picture this where you've built tools which are like they're kind of out of the box you might need to run them because you know how they work the best but actually another auditor could also run them but when you get into the formal verification side of things would it need to be the person who wrote it who does the check because they need

to so deeply understand this circuit not necessarily no so basically when it comes to the the formal verification typically that just needs to be done by someone who has expertise with a particular verifier so for example at least in the context of ZK a lot of the actual verification is being performed with what is called an interactive theorem proofer so this is something like or lean if you've heard about them and so essentially the way the formal verification is done there is you translate the constraints down into uh this form that can be understood by or lean and then you manually write a

proof that says that your specification which you also encode in the interactive theorem prover matches the constraints when it comes to an audit so as you're going through this you start with the static analyzer if you find something do you immediately bring that back to the team you're auditing or like the company or whatever like and then see if they can fix from there or do you actually go through the whole process and then give them a report yeah so we try to do as much as we can in parallel and so typically for something like a fuzzer it it's faster to set up but it can take days to run and so uh when we do these things we kind of have this process of how the

order in which we'll start things and at least for a static analyzer we normally get feedback very quickly okay and we we do provide that feedback as soon as possible because at least for something like formal verification if there is a bug that was found by one of the previous uh components the normally the formal verifier is going to find it as well and so really for formal verification you want to verify on the fixed version that everything is proper otherwise you're just going to be rediscovering all of those same bugs with more manual effort is it also good that people do the correction because it's possible they make a mistake in that that the formal verification might find out or would you just run the static and analyzer again on the new version anyway yeah so basically so when

we when we perform our audits what we're going to do is we're first going to perform the audit on one fixed version of the code because when you keep getting new code that makes the auditing process very chaotic and very difficult and so typically what we'll do is we'll perform as much work as we can on the version that we're auditing and then when we get to validating fixes then we'll make sure that we run the same tools that we ran on or that found bugs on the unfixed version of the code the the version that we were given to audit on the fixed version to identify any potential new issues because we have found bugs in the code that people have provided us to that is supposedly fixed

but like different bugs almost yeah but the fixed chain made a new bug appear yeah so sometimes things weren't fixed quite properly other times they introduce new bugs that we then would point out how long does something like this take each of these tools I'm picturing you pressing a button in like 30 seconds later it's like yes but I'm guessing it might be a little longer than this yeah so static analyzers will typically take somewhere in the order of minutes and so in that case your your picture is exactly right for a static analyzer for a fuzzer it can take longer and so with a fuzzer because it's purely random the longer you could run it and it won't

find bugs the better and so with a fuzzer we we typically try to run them for a longer period of time normally about a day or more and then for a formal verifier that can take a lot longer than a couple of minutes because you know typically you'll you'll write a specification and then you'll run it through the formal verifier if with formal verifiers they they might take a little bit longer to verify but in the case where you get counter examples then you might need to refine your specification or introduce new invariants that the the verifier didn't know about in order to push that verification through I I was actually curious about this like when you use the

formal verifier in prep to use it on a particular circuit I'm trying to figure out how abstracted it is or how General it is like do you have to rewrite or like do you have to know this circuit intimately and then like write it into the formal verification yeah so so basically what someone has to do um is if we have uh an automated translator from the circuit language to uh the interactive theorem prover because let's just say that we're using an interactive theorem prover in this case um I'll ignore automated verification if we want to talk about that a little bit later maybe we can but essentially the the auditor

themselves has to perform that translation uh in order to help with that process both in terms of scaling the formal verification and to make it less error prone we also work on automated translations from a particular language to the language used by the interactive they're improver so Cocker lean and then the next thing that you do is after that translation has been performed you then encode your spec in that language as well and then finally you write a proof that that spec holds over the translated program so there's quite a lot of setup work for each one of these things it's not like out of the box and it's going to

understand different circuits in the same language yeah so the hope is that and I mean this is what everyone works on as they start getting more and more uh circuits in a particular language than they work on automated translators too uh Cocker Lane and so we have I think one written for circum that will automatically translate to in our case for uh performing that formal verification but um yeah other languages the the translation has to be manual does it matter I'm curious here like I mean so far you've talked more about circon but not so much about like proving systems does this proving system

have any part of this say you use Planck versus using something like Nova do you have to rewrite these things or can you reuse them yeah so the reason why I say uh circle is just because most of the audits that we've gotten have been forced or come but really a lot of our tooling actually targets r1cs so for different proving systems typically yes you do have to do uh some extra work because you can then with different proving systems obviously have different shaped constraints yeah and then on top of that when it comes to some of these systems like plump now you also have to deal with recursion and so r1cs is typically just the or at least the r1cs chin are hit by circom is typically just

the easiest one for us to deal with because the the constraints are quadratic and then uh while you can I think now have recursion in in those constraints typically they don't yeah I mean I'm I'm just thinking about like r1cs versus something like air or like this sort of Stark structure have there been any auditing tools built for those kinds of systems or is that still like yeah I'm just curious like how much work has to go into building like yeah can you reuse anything if it's a different underlying structure yes so so basically you can always reuse the interactive theorem proverb because that

part is general and so really at that point it comes down to the translation process so when you translate down to that underlying form uh when you move to a different proving system then likely a lot of that is going to have to be re-implemented and so for example if we have a translator that works on cercom for example even if we move to a different language that will generate r1cs we would have to we'd have to create a new translator right and so generally for that reason it makes more sense to Target a proving system like or at least the language for proving systems so something like r1cs or or Planck or something like that that way

you can then support multiple languages are you from familiar with some of the newer languages coming out like there are languages like Noir which are kind of specially designed for some of the more modern plonk uh variations as well as others I know that I think folks from the Noir scene would not say it's just for plunk but like there's some new languages coming out I guess the question here is almost like is it on your radar how would it get on your radar like would you need a project to approach you saying hey we want an audit we're using this other language and then you'd get into it or are you kind of tracking it yourself yeah so a lot of these new languages are on our radar especially because at least my feeling is that in order

some of these new languages will bring greater security and so for some of these languages that are being developed like uh yeah like Leo for example or lurk where people don't have to write the underlying constraints themselves that can bring a much greater security because then you don't have to worry about the individual developer making uh or running into issues and so at least in terms of what we do at Paradise uh we are aware of these different languages and we try to learn as much as we can about them beforehand but we normally can't spend too much time investing and tooling for those particular languages until either one

like we try to approach these uh ecosystems early and try to determine like whether or not we'll get or How likely it is that we'll get audits for them in the future but really a lot of art development at least has been driven by the the projects that we've been getting and so we we are working on a number or expansions to our tools to support other languages so for example some of our tools at Paradise work on source code and so uh typically they were built to support certcom because that was what we got most of our or a lot of the audits that we've gotten have been in sir pump but now we've also

gotten audits in Halo 2 and Arc works and stuff like that so at that point we have started expanding them to work on those languages as well yeah so similarly when it comes to talking with these ecosystems sometimes we expand our tools to those ecosystems but generally it's driven by the audits that we end up getting as you just said that I'm just like Halo 2 to me is a proving system what is I actually don't know this what is the language of Halo 2 is it rust yeah it's rust yeah what happens for something like this then like what happens if rust is the language yeah it gets more difficult let's just say that um so Halo 2 is kind of a unique Beast because basically what you're doing is

you're you're using in order to basically construct the circuit so you've got a circuit Builder that you're interacting with and rest right and so at least for some of these things when it comes to supporting them one of the reasons why we like supporting things at the language level is because then we can reason about at least for a static analyzer we can reason about both the witness and the constraints at the same time because if we can find deviations between them that's likely a bug however for some of these systems where that might be let's say complicated like supporting rest uh sometimes we have to let go of the witness generator side of things that helps us Identify some of

the bugs and instead we reason almost entirely about the constraints in order to find books and so it's always better if we're able to have more information and so that means that some of the at least for the static analyzer some of the detectors that we've developed uh work better in some languages than others but um yeah basically we try to adapt as much as we can to new languages or new proving systems throwing back to that earlier episode I had done on formal verification I know at the time we talked a lot about rust and how rust as a language already has like a form of checking and so there's almost like the spectrum of moments when

your code gets checked and very you know as you're writing it if you're writing in Rust it's getting checked there but then you know you can further check it formal verification potentially being at the end of that where it's like the most checked right does formal verification like rust does it save formal verification like does it find things that normally formal verification or some of these other tools would find so yeah basically one of the nice things that you get with rest and I'm going to say nice from a language perspective rather than sometimes from a developer's perspective is rest has this notion of a borrow Checker and so the borrow Checker essentially is going to perform what maybe you can consider as some sort of

basic form of formal verification it's basically going to validate that when you works right kind of it's basically going to validate that when you have a reference to a program you're you're not using that reference in let's say an improper way because when you have something like C or C plus you can get into problems where like you have a piece of memory allocated and you haven't freed it so with rust the borrow Checker allows you to let's say check something out and then it will validate that it will only compile if you have properly used what you have checked out or if you've like checked it back in for example and so the this borrow Checker basically provides

concrete ownership of a particular reference to an entity so that you're less likely to run into particular issues or yeah I'm going to say less likely because you can still use some unsafe things but at least in rest you can say this is unsafe and so one nice thing and there have been there's at least one paper that I can think of off the top of my head where people have used knowledge of Russ borrow Checker in order to help simplify the process of Performing formal verification interesting but not in ZK so far but not in ZK no this was just a verification using rest

and so in ZK at least um you can still end up with normal bugs that you would otherwise because at least right now what you're doing in rest is your your rust is just the language that you're using to build the circuit itself so you can still make an under constrained circuit because rust is not going to do anything to help when you generate your constraints okay and you sort of mentioned lurk as like a language where it sort of protects developers from making some of these errors but could you build some sort of formal verification into a language for ZK could that ever happen where like almost using that similar technique that you just described in Rust but actually looking at like how a circuit performs yeah so there's a couple of different

things that you can do here so first let me address something like or languages like lurk or uh Mina or something like that so right now there's a couple of different things that you can do so you could one have a high level language and that language is just going to allow people to express the computation that they want to be checked by the ZK circuit and then at that point because developers aren't writing the ZK themselves you can perform formal verification or whatever you want on the underlying infrastructure and validate that yes that infrastructure is correct yeah yes and then you're you're doing it once and so that's one thing that you can do another thing that you can do is and

this is one thing that I'm interested in is you could perform formal verification over the witness generator itself when expressing computation and then as part of the language you could possibly prove that my constraints actually are constraining my program to be exactly this Witness and so that would be another interesting way of doing it where it's kind of like you have a a formal verifier in the loop and so this has been used in other languages so for example there are languages like Daphne and a couple of others where

um you basically perform the formal verification in line with the actual computation and that seems like something that would be interesting in this domain where when someone expresses constraints they there is some integrated tooling that will make sure those constraints and the the computation match the problem is then it places more of a burden on developers because now they basically have to be the ones who perform the formal verification and the feedback that you get from at least interactive theorem proverses not always the best not clearer or not yeah so sometimes it's not quite clear especially to people who aren't very familiar with the

system like what the problem is and so yeah about it I want to talk about Security in the ecosystem okay you are primarily working and exploring I assume projects that you are auditing for so this is a company has been like hey we need external Auditors to look at this code before we go live and they send it to you but do you in the training of these tools do you also look at other circuits other code that isn't your clients yeah and like kind of why I'm kind of curious like is it is it to train up the tools or is it because you're curious or like no so does it help you get deals too it's kind of like hey hire us yeah I mean kind of all of

the above so basically we we use our tools to help with our client code because essentially the more code that we can expose our tools to the more confident that we can be that we have not you know introduced bugs into our own codes so the more confident we are in their results and so there are very good reasons why you would want to let's say check our tools on other people's particularly if we know that code has bugs and this is part of the reason why we like running them on code that we've audited because then we know exactly what bugs should be found but you know for code that has been exploited you oftentimes would want to run your your tools on that to make sure

it can find the exploit if it's supposed to and then in terms of running it on other code let's say code that's just publicly available on GitHub that's also useful because if it can find bugs then you found something new but it also again gives you the opportunity to let's say identify false positives or something like that for a static analyzer that where maybe it identified something that it shouldn't have so that you can trim it out so basically it just allows you to build up your confidence and then when you find a bug then obviously that can be good if you can report it to that particular developer ahead of time and that has led to us finding clients in the past interesting

I am curious about the disclosure process maybe going back to the solidity world are there ways that people expect to happen in solidity and does it change when you move into the ZK world and the reason I'm asking here is like a bug fix in solidity might be quite fast and I'm wondering if you find something in like in a ZK circuit is the fix that much harder yeah just tell me if there's any difference and maybe just how does it work in the solidity world let's start there yeah so in terms of disclosure uh things can get a little bit awkward and so you have to figure out where the appropriate place and this is kind of

the first step in order to post a disclosure so for example four people who want to get paid for their disclosures which a lot of people do they might not want to post something publicly because then someone else might be able to claim it and also they then might not get paid because people can or the developers can take that disclosure and then just kind of go with it and that was one of the issues that people had in the early solidity days that's why some of these bug Bounty platforms like immunify and stuff like that exist because one problem that people had is they would identify a bug they would disclose it privately to the developers and the developers would say okay great and even

though they technically had like a let's say a private Bounty program where if they got a disclosure they would say this isn't actually a bug and then go and fix the bug and people would not get the money that they felt like they would do and so that's where some of these uh bug Bounty programs like immunify came in because they have like a recorded process where developers or hackers can feel more confident that if they disclose a bug they will get a settlement or they will get the actual Bounty that they were promised because now a developer can't necessarily just disappear and say I'm not giving you the money that you know

you expect that I would or that I promised and so that's kind of how it works in the solidity world at least right now and because a lot of people in ZK are kind of building on top of these d-apps some of them also use similar platforms right like immunify but some don't and so when it comes to disclosures at least for us because some of the bugs that we found are in things that may or may not be in production because it's not always clear what's in production um we try to disclose things privately and then we're generally not looking for a bounty unless someone has a bounty

program but it then gets kind of awkward because sometimes we disclose things and then we just don't hear back from the developers and it's unclear if they've fixed things like we'll we'll monitor their their GitHub usually to try to see if they have but uh when we report something and we don't hear back from them it can be a little awkward to know like did you validate this as a bug was was there a reason why maybe this wasn't that we didn't get or something like that so in the case that somebody that a team receives a report like this and they don't react are there ever times where it actually maybe the reason they don't react is it's not breaking it wouldn't

affect their system uh possibly yeah so at least generally when we've done this it's been by discovering uh protocols that are publicly available like on GitHub and so in that case it might not be something that they actually have deployed in production it might be something that they're currently building or something like that and so the the kind of awkward part about you know when people don't respond to this is it it's one where part of the reason why we are reporting this is because we want to make sure it's not a bug or yeah we're there to help and also if it's not a bug we want to learn so for example uh four bugs that we found with tools maybe

there is uh an additional components that we're not aware of that is preventing this from actually being a bug so for example perhaps they're performing some on-chain validation like we talked about earlier that our tools or we weren't aware of and so uh essentially one of the reasons or one of the important reasons why we at least want to report bugs is so that um if the developers disagree with us we can at least learn from them why they built the system this way or why something that we reported maybe isn't a bug so in there's been kind of a conversation brewing in our big Telegram and CK podcast telegram group about

security it's kind of come and gone over the last few weeks and there was one kind of CounterPoint to this which could potentially help explain why some teams aren't reacting which was this idea of and this is this was mentioned by an auditor by a ZK auditor that sometimes there's these like under constrained bugs that wouldn't necessarily be exploitable either because of the way governance is set up or there's only a certain part of the stack in this case like relay relayers that would actually be able to exploit it have you seen any of that could that actually help explain sometimes why there's no reaction it could so for example this is uh where I was kind of describing different parts

of the system that maybe would have allowed um this not to be exploitable so for example in the two cases that you were just talking about basically there's some validation that's being performed on chain that maybe we're not aware of or perhaps a particular proof has to be generated by a trusted entity because maybe the ZK circuit is validating a signature or something like that or for particular inputs and so in that case maybe it's okay that certain values or certain computations are not uh properly constrained and so there could be reasons why an under constrained value might not actually be

exploitable and so for example in one of the disclosures that we made to a team about an under constrained circuit they took it very seriously and particularly because they were hoping to run their trusted setup soon and so they they worked with us in order to try to figure out why this thing was under constrained and while the circuit technically was under constrained the the signals that were actually under constrained were kind of some utility signals that they were using that okay actually were not necessary for the circuit to operate correctly and so uh they were performing some additional computation and it turned out that computation was

unnecessary for the circuit to actually operate correctly and so in that case they were able to remove constraints which is typically great for proving time but the circuit itself more importantly was not constrained or under constrained I'm kind of curious like given you're an auditor it sounds like you're I mean you're doing the disclosures privately responsibly but do you ever bump up against the black hat hackers the other hackers the like or like you you sort of see them around like would you be able to spot because you're kind of in these code bases would you ever like be able to spot other hackers uh no because generally the the black you know the black cat had or hacker is

only going to show up once things have been deployed like they're not okay they're not going to necessarily show up there typically with a black hat they actually want things with baby bugs that they found in the source code to be deployed that way after deployment they can steal funds or something like that and so in the process of auditing I have not bumped up against black hats okay I always find it fascinating sort of the the motivation of the kind of good hacker here like there is the financial gain potentially through bounties I think there can be like epic cred in the community I think if you look at like the Dow hack you look at those stories that are you know Geordie and Griff like

they're written in books like books are written with them as like you know protagonist type characters I mean this is awesome but yeah I wonder are there other things that you think could motivate the appropriate positive disclosure that would like almost encourage the black hats not to wait for that vulnerability to be out in the wild other than what we've talked about it's pretty difficult because one good motivator is obviously money um and at least for motivating a black hat really most of the time what they're doing is they're they're trying to get some sort of financial gain sometimes they'll do something just to spread chaos or something like that because

that can be fun I guess but um really the financial gain aspect is at least in this space pretty significant right and so one thing about disclosing at least bugs early is someone doesn't necessarily know how much money is going to be tied up into a protocol right and so uh if they could report something to a bounty system where they know they will get X funds whereas yeah uh rather than actually exploiting the the thing in production where maybe they can't quite get as many funds and that can be a motivator another one is it can be

difficult to get funds out of these systems like you you might be able to steal funds but then you have to quickly exit and sometimes those exits are not very successful because I feel like people think that they've found a bug and then they try it and then all of a sudden they end up with millions of dollars and they're like oh now what do I do um and so so that's another reason is that I guess these Bounty programs are important to motivators because not only does it allow someone to kind of engage and get that money early it also provides a more guaranteed source of funds if you report a bug because just because you

can exploit the thing doesn't mean that you can successfully exit those funds yeah at least in the context of ZK I think the big question is going to be whether that matters because if everything is private and let's say they can exploit a circuit itself then in some cases it's not obvious that something has actually been exploited or a hack has actually occurred and so at least in this context it's going to be interesting to see how things go forward and I really hope that they do not go forward in a disastrous way okay are you I I'm just now I want to ask sort of a final question on this given the fact that

you're looking at a lot of ZK systems how optimistic are you should we be worried or do you think we're going to have sense well part of what we end up seeing here so the problem is everything is being designed at a really low level people are actually designing these constraints themselves and I would kind of end up you know saying that that's very similar to you know actually programming and assembly it doesn't encourage proper programming practices in some cases and it can be quite dangerous and so we have seen a significant number of bugs during the course of our audits so

I think I calculated this recently on average in ZK audits we found three to four significant bugs per audit on average wow and some of them corresponded to these under constrained circuits during the evaluation that we did on our static analyzer we found even more in publicly available GitHub code which like I said I'm not sure if it's in production but in a lot of these cases it's because people weren't understanding how to properly constrain particular values because there are edge cases that they don't think about so for example and I've talked about this in a couple of conferences if you think about something like division you know that you can't actually divide by zero but you can't

really Express Division and I don't think any of these constraint systems so instead you have to say like rather than a divided by B is equal to n you have to say n times B is equal to a okay however if this is trying to constrain a division you also have to consider the case where uh B can't be zero and that's something that people often miss because it's not really something that you think about very frequently yeah and so that was surprisingly one of the major bugs that we ended up finding in these systems is people not understanding how to properly constrain the semantics of the language that they were trying to or that they were expressing these constraints for

and so for that reason like what I'm hoping going forward is earlier we kind of talked about these high-level languages where maybe you only have to perform the verification once like I think that at least going forward what I'm hoping to see is more people making use out of these languages like Elio Mina lurk risk zero things like that where they can express their computation and then let the language itself deal with the actual constraints because as long as the language team or the people developing that language do their job

properly you only have to check that once yeah yeah or I guess as things upgrade multiple times but really um but just on like like the the person writing it could be like depending on those checks being made right hopefully those uh people developing the languages and I've met with quite a few of them and they're all very intelligent and stuff like that and so you leave the difficult part up to the experts and then uh have them vetted very thoroughly in order to bring broader safety because really the problem that we have right now is in terms of the safety guarantees like they're everywhere you have to

trust everyone you've got to trust the developers you've got to trust the proving system whereas things would be a whole lot better if you were able to kind of design things in a more I guess modular way where only one part has to deal with the constraints and stuff like that the reason why that might not happen or I that people would still design in languages other than that though would likely be in order to improve the the proving times because not every application is going to be amenable to these languages which will likely have a larger overhead um cool well on that note I want to say

a big thank you John for coming on the show and sharing with us sort of how formal verification and ZK can work together a little bit about your journey Fair dice's work and yeah kind of the landscape of ZK security disclosures yeah I really appreciate it yeah no problem thanks for having me I want to say a big thank you to the podcast team Rachel Henrik and Tanya and tour listeners thanks for listening foreign