What don't we know? Understanding Security Vulnerabilities in SNARKs

Hello, thanks for the introduction. So today I'm going to talk about vulnerabilities, mainly in the implementation of Snarks or ZK-Snarks, and also on what can go wrong when we deploy SNARKs in production. This is joint work with collaborators from TUM, the Ethereum Foundation, ZK Security, the Scroll Foundation and also Imperial College London. Okay, so let's start. Okay, what is the state of ZK-AP applications today?

We have ZK-K rollups that have become very popular in the last two years. They have more than 5 billion USD in TVL in them. We have Zcash, which is a payment system. It was deployed, I think, the first version around 2015, 2016. We have many ZK applications both for infrastructure such as ZK bridges but also for private payments, for using wallets without having to use seed phrases like ZK login.

We have private programmable L1s and L2s like Mina, Aleo, Azdec, and also we have some off-chain applications. And although all of those systems have been deployed, we haven't seen any major exploits like the DAO exploit we had in smart contracts. And although we haven't seen any exploit, there have been bugs in the systems deployed in production. So Zcash had a vulnerability. Sorry for the pictures, might be a bit small, but I will go through them.

So Zcash had a vulnerability for, I think, more than a year in it. People from within the Zcash, found it, and patched it. Then one of the most popular mixers had a vulnerability that if someone exploited, it could have basically drained the smart contracts of that protocol. One of the most popular ZK rollups had a major vulnerability that someone could again potentially could have exploited and get everything out of that roll-up. And also I would say that in audits in ZKE protocols, even in top-notch protocols, if you compare it with top-notch smart contract protocols, the ratio of critical vulnerabilities, it's even higher.

So there are many vulnerabilities. And people for many years suggested that ZKPs are very difficult and very hard, and not many people actually understand them. And also they have suggested that to exploit a ZK protocol, it's much more difficult to exploit, for example, a smart contract vulnerability. I would say the first one is not true anymore, right? Because if you see the number of presentations in ZK in DEF CON this year and compared with three years ago, we have an exponential increase.

And also, although it might be true that some ZK vulnerabilities is difficult to exploit, I would say that some of them are pretty simple. And for example, here we have a circumcircuit. It's a very old circuit, but anyone who has written a circumcircuit could probably understand what's going on here. And still there are such vulnerabilities in ZK protocols that I think are pretty easy to exploit. So there is a huge risk if there are still vulnerabilities in deployed protocols to be able to exploit them at some point.

Okay, so let's start with explaining what are the properties of a ZKE protocol. We have knowledge tenderness, which basically means that a dishonest prover cannot convince a verifier of an invalid statement except with a negligible probability. We have perfect completeness, which means that if you have a valid statement, a prover will always be able to convince an honest verifier of the correctness of that statement. And also we have zero knowledge, which means that the proof pi that we produce with the zero knowledge proof does not reveal anything about the witness we are proving. So what is our threat model in a ZK world, right?

We have three adversaries. So what is our threat model in the ZK world, right? We have three adversaries. We have the network adversary who observes the system and its public values but cannot interact with the system. We have the adversarial user, which basically is able to submit some inputs for proof generation in an honest and non-malicious prover.

And finally, we have the adversarial prover, which is the most common thread model, and it's our thread model when we actually need the ZK property, right? But I would argue that even if we don't need it, if we want to have a fully permissionless system, then that's the adversary we have. And it has the ability to produce proofs and has the ability basically to do everything to try to trick the verifier. To give you an example of what I mean with the second category, because it might be a bit confusing, consider ZK rollups at the moment, right? Where we have a single centralized trusted L2 node that is both the sequencer and the prover so users can only submit the transactions there and then that centralized node will produce a proof so in that case we have an adversarial user basically and what can be the impact of ZK vulnerabilities.

So, we might be able to try to break sadness, which means that a prover can convince a verifier of a false statement, and that could result in basically, for example, in ZK roll-up, to get all the funds out of it. We can break completeness, which means that a verifier cannot verify proofs, or basically that the prover might generate verify proofs, or basically that the prover might generate invalid proofs, right? And for example, such a vulnerability could basically have a high impact in the liveness of ZQ rollups. And we might also break zero knowledge, which means we have some information leakage. Okay, so what we did is we analyzed 141 bugs and vulnerabilities from audit reports, from vulnerability disclosures, and from bug trackers.

And our goal was to split those vulnerabilities in layers and understand what can go wrong in each layer and also create a taxonomy of vulnerabilities. So let's start with that figure. So in the real work, non-SNARK work, we'll have a relation, a specification, some idea that we want to actually create a ZKP about. And we might have some public and private inputs. So the first step is to manually encode that specification, that idea, in a circuit and get the circuit implementation.

So we figure out that in that level, it's where most of the vulnerabilities happen. And the main reason, in our understanding, is because it's confusing for most developers to write circuits because they have to think both about computation and also about constraints and they might do very aggressive optimizations there and they might try to apply some tricks and that typically leads to vulnerabilities. So we identified three main vulnerabilities. Other constraint vulnerabilities which means that you forgot some constraints or some of your variables are partially constrained. And that typically leads to sadness vulnerabilities, which is the worst vulnerability that can happen in a ZK system.

Then we have over-constrained vulnerabilities, which is the exact opposite. That most typically will lead to completeness issues. And we also have computation or hint errors, which is just on the computation part. And accordingly, you might have messed up constraints, but the root cause was in the computation part. So we did a complete root cause analysis and I will share with you a QR code for our paper to look into examples and to look on how you can fix some of those vulnerabilities, etc.

But very briefly here, we have categorized them in three main root cause classes. First is that when developing circuits circuits we have a different programming model and that could lead to many vulnerabilities. Secondly we observed that the root cause of vulnerabilities were optimizations and also having cryptography at the outer layer and in very low level DSLs that could introduce many vulnerabilities and also common errors like in any software, like specification issues or API misuses, etc. So, the next layer is the front-end, which is basically composed from two components, a compiler and a witness generator. The compiler will take the circuit and will try to produce an intermediate representation that it's on what our proof system works on top, for example R1CS, and then the witness generator will take the circuit, will take the public and the private variables we have, and it will produce a witness.

And the next one is a backend. The backend is composed of three main functions, setup, proving, and verification, and things can go wrong in all those functions. So the vulnerabilities we identified here in the frontend is incorrect constraint compilation and errors in witness generation and in the previous presentation we saw how things can go bad there and it's very critical to actually trust and to be able to have correct implementations of front-ends and in the back-end the situation is quite similar. From our data we found out that unsafe verifier is a very common issue and can lead to major vulnerabilities. Let's go to the next one.

The next one and the last one is the integration layer, which is basically you can think of one and the last one is the integration layer, which is basically, you can think of it in the blockchain space as the JavaScript that is responsible to run your prover client side and create the proof, and also the smart contract that consumes that proof and calls the verifier you have implemented or it was produced automatically and try to do some things. And we had some very interesting vulnerabilities in that layer. I want to focus in the first one, which is passing unchecked data. And what does that mean? Sometimes, as already said, we might try to do some optimizations in the circuits.

And for example, one thing that is pretty common is for people to say, OK, in that circuit, let's have some implicit assumptions that our inputs are in a specific range. And then delegate that check to the actual code that will call the verifier. So in that example, we forgot to do such a check, and that could lead to major vulnerabilities then in our infrastructure. And in the last year or so, there has been a major change in some architectures, where instead of circuits, we have ZKVM circuits right so the developers now only care about writing some program typical in the high-level language like Rust and then compile that program and giving it as an input to ZKVM. Still, circuit bugs can happen in the ZKVM itself, and I would say a subtle new threat here is traditional compilation errors that might happen to the Rust compiler, for example.

That could lead to have invalid proofs. So that's something that people should take into consideration when using ZKVM cells. So another way to see what we currently described is in a hierarchical way. And here I have an example of all the stack when we use the circum-programming languages and SNAC-JS with GROT16 Azure-proof system. I have two new layers here.

One is full arithmetic elliptic curves, which have nothing to do with ZK, but when we construct and implement a proof system, we have to have such a very efficient library and things can go wrong there. And also things can go wrong in the hardware, in the operating system, in the blockchain we are using, right? So you should always be very, basically think about what you are going to use and apply all traditional best security practices we know from other fields. And one last thing is that in the proof system, there could be errors there, there could be errors in the initial description, in the papers of proof systems. So if something goes wrong there, it doesn't matter if you have formally verified the circumcircuits, if you have the best backend or frontend, it could be exploitable.

And that basically it's true for any layer. So if your frontend or the backend it's vulnerable, then even if you have formally verify your circuits, they could be exploitable. Okay, so we did that analysis and now I want to present some of the results. So we categorize the bugs in all those layers and also based on their impacts. And we can see that circuits was the number one threat in the whole infrastructure of using ZKPs.

And also most of the vulnerabilities can result in soundness issues. So what can we do? Fortunately, there has been a lot of development and a lot of research of creating security tools for ZK circuits, specifically for ZK EVMs or ZK EVMs and also in the last month two new papers were published and tools, Circus which was presented in the previous talk and also MTZK which is great because such novel tools can detect infrastructure bugs in circuits in ZPs, but I would say there are still a lot of work that needs to be done. For example, most of the circuit tools, they target a specific DSL, and also they typically target a specific vulnerability class. And then we have some tools like static analysis tools like circumspect, which might have tons of false positives.

And then we have some really nice tools and very novel tools like PyCos that try to formally verify and find any under-constrained issues in the circuits but unfortunately those tools do not scale that well. So there's a lot of space to do to have innovation and try to build better tools and here I have a list of security tools. You can scan that QR code and it's basically GitHub repository. If I don't have any of the tools that you are know of, please add them. And yeah, we need to do a better job here.

And one also major issue I see in this space is that we don't have good tools for writing tests. And most of the code base that user knowledge proves is that we don't have good tools for writing tests. And most of the code base that user knowledge proves are unfortunately not that good in having complete test suites and try to understand in the testing part both soundness and completeness issues. Okay, so in conclusion, why do we have bugs? One of the reasons is that because ZKPs are not just mods.

There are implementations and many things can go wrong in those implementations. Why else? This is a quote from Ron Rivest in a completely different context, but I really like it. And I would say that in the ZK space, unfortunately, we have given to the poor developer enough rope with which to hunt himself. Circuit languages are typically very low level, so they don't have good abstractions for developers to write safe code.

We expose a lot of cryptography to the outer layers, and also there is a lot of complexity and a different threat model than what developers are used to. And there is a lack of specification throughout the whole infrastructure and the whole stack for using GKPs, so we need to write more specifications. So what can we do? Basically, we have to negate everything from the previous slide. We need more layering resources, which I think we are doing a great job in that as a community.

We need to write specifications and get used to write specifications because if you have complete specification, then we know exactly what text we should put in each layer and what vulnerabilities can happen in each layer and that's how we can help developers but also auditors into doing a better and what vulnerabilities can happen in its layer. And that's how we can help developers, but also auditors into doing a better job in trying to find vulnerabilities in those systems. We need easier and more secure programming languages, which I think it's kind of where we are heading to. For example, Noir is a great language that it's much more safer than writing circuits in Siricom or Hello2. But in some cases, people will still need to write circuits in Hello2 or Siricom because they need to do some specific optimizations or they need to deploy to specific blockchains, for example.

And then we need better testing and security tooling from simple frameworks to write unit tests, to do property-based testing, to formal verification. And not just formal verification. So that's it. I have there a link with our paper where you can find many examples and how to try to avoid some of those pitfalls. And we also have a blog post that we publish many blogs about ZK security in general.

So, thanks a lot. Thank you, Stefanos. This was enlightening. All right, people. As usual, you can ask your questions here.

We're going to go through them in order. And let's take the first one. Several times in your slides, you referred to witnesses. What are witnesses? Are those private inputs?

So a witness, I would say, it's composed from both the private inputs, the public inputs, and all the intermediate steps and the outputs for our circuit. So I will say it's a trace that then we create a proof about that trace. Thank you. All right, next question. I've put a bunch of those, so do ask serious questions, please.

We have a bit of time. What is your favorite bug ever? What is the most interesting bug you've ever found? That's a very good question. I think I can't pick one, but I would say typically the simple bugs, right?

For example, the bug I have in one of the first slides, that could have led to basically draining one of the major mixers we have in the space. But also bugs that have to do with using cryptography in the circuits. And typically due to some optimizations or some logic errors in those circuits, there could be like pretty interesting exploits that someone can do. Pretty cool, thank you. Alright, the next one.

You're doing research, looking for bugs, you're paying your bills and buying your foods by finding bugs. Can we consider you have a bug-based diet? We can consider that, yeah. I hope that in some future world there won't be that many bugs and maybe I will have a better diet. But unfortunately at the moment we have tons of bugs.

Fantastic, thank you. What are your thoughts on TEE? Okay, that's the question of DevCon, I feel. Everyone asking that question. I would say you have different security assumptions when you use TEs, right?

I think it can work along with ZKEs, but they can't replace ZKEs. You have a much weaker threat model when you are working with TEs. So, yeah, people should use them when they have to use them, but also don't trust them like a black box that will do everything for you and you are secure if you use a TE. Wonderful, thank you. What can we do to make more secure languages like Noir faster compared to Sercom, particularly with respect to gas cost?

How do we make it more efficient? So gas cost, I will say that it's independent kind of what programming language you're using. It's more about like what proof system you are using, right? And if that proof system has very efficient verification, that's the main factor. But also more general in the circuit layer.

I would say that indeed someone, if you don't like really use unsafe in Noir, which then breaks the whole purpose of using Noir, you can write more optimized circuits at that point in Siricom. But I would hope that we will have major advances in compilers for ZKPs, and then we can have compiler optimizations that are very strong, like in any other field, and rely on those optimizations to get pretty optimized circuits. But if we do that, then we need very, very solid testing for our compilers to detect any issues in those optimizations. Thank you. You mentioned in your slide that, you know, sometimes we give too much rope to the users to hang themselves with.

I think the design in ZK circuits is difficult, but also using them is not very commonplace, right? A lot of users are not used to using this kind of systems and what goes in, what goes out, what you can do with them, what is safe behavior to do that. You mentioned learning resources. Do you think there's something to do with users also to explain to them what are the benefits and what should be done? Or is it entirely on the app developer?

Yeah, yeah. That's a great question. I think as researchers, it's our responsibility to create learning resources that are easy to follow by almost everyone. So I think we are doing kind of a good job there. For example, at ZK Security, we published a book on Hello2.

And basically, many teams in that space develop pretty nice learning resources. And what I really like is that they also have a section about security vulnerabilities and what you should look at when you use a specific DSL. So, yeah, I think we are doing a great job on that. And in a few years, it will be even better. Fantastic.

Stefanos, thank you. We're over time. So thank you for your talk. Thank you. Thanks a lot.