This post was authored by Kyle Charbonnet.

• Table of Contents:

  • What is the PSE Security Team?

    • L2 Security

    • ZK Security

  • Recent Projects

    • ZK Bug Tracker with 0xPARC

    • BigInt Audit with Veridise

    • ZK Circuit Static Analysis with Veridise

    • Bridge Bug Tracker

  • How can I contribute?

  • Team Members

The PSE Security team has been working on some pretty cool projects lately, so we’d love to share what’s been going on. But first, let’s take a look at what type of security the PSE Security Team focuses on.

What is the PSE Security Team?

The Privacy & Scaling Explorations team at the Ethereum Foundation has its own security division. The main goal has been to help find bugs and strengthen security in the Ethereum L2 and ZK ecosystems. As we have all seen throughout Ethereum’s lifetime, one critical bug can cause major setbacks to the whole space. So it’s very important to get ahead of these bugs, especially in newly developed fields such as the layer 2 and zero-knowledge spaces.

L2 Security

Ethereum’s main scaling solution is now looking very likely to be L2s. If this is the case, security for these solutions becomes critical. Many may think that L2 security is not much different from traditional L1 smart contract security since so many L2s are aiming to be EVM compatible. However, there are a lot more concerns to think about.

The main security threat so far with L2s has been proven to be secure bridging between L1 and L2. There have been many extremely large bridge hacks in recent times. We’ll go over these bridge hacks when explaining project 4 later on.

When assessing the security for an optimistic L2, one must carefully consider what exact transaction data is stored on-chain, what does the fraud proof mechanism look like, who controls the sequencer, etc. These are all new concerns related to the development of L2s, so it’s important to understand what secure answers look like.

Security for ZK L2s has many of the same concerns as those for optimistic L2s. The major difference is that ZK L2s rely on ZK circuits for proving correctness rather than fraud proofs proving incorrectness. As such, ZK security in general plays a significant role and will be explained in the next section.

One of the best resources when it comes to L2 security is L2Beat. They provide an in-depth analysis of the major L2 solutions and bridges out there, properly assessing security risks for different categories.

ZK Security

In recent years, ZK rollups and the zkEVM have been designated as the “holy grail” of scaling. It’s easy to see how important security around ZK technology is for the Ethereum ecosystem. Additionally, implementing secure cryptographic protocols in code is almost never easy.

Cryptography has been around for some time, but ZK cryptography has made rapid progress in the past few years. Many of the codebases that implement and use these ZK protocols are newly developed as well. Just as early smart contracts contained new types of bugs that are now seen as obvious, these early ZK codebases also contain new types of bugs.

The nature of coding ZK circuits and ZK protocols is quite different from coding smart contracts or a REST API. We must look for a whole new class of bugs and attack vectors. Projects 1 through 3 will expand on this in more detail.

Some big players in the ZK security space are Veridise, TrailOfBits, and 0xPARC among others. They all have great resources to learn and enhance ZK security.

Recent Projects

Now, 4 cool projects the PSE security team has been working on:

1. ZK Bug Tracker with 0xPARC

The ZK Bug Tracker github repo is a community-maintained collection of bugs, vulnerabilities, and exploits in apps using ZK crypto. As discussed above, with the advent of ZK applications there are whole new classes of vulnerabilities to be studied.

In the code security world, oftentimes a small category of exploits will be found over and over. By checking for just this small set of exploits, auditors can remove a large majority of the bugs in the code they read. This won’t rule out all bugs, but it will help significantly. This is why documents that outline the most common bugs in a certain field can be very helpful to auditors. This is what the ZK Bug Tracker aims to do.

There are two categories: Bugs in the Wild and Common Vulnerabilities. The Bugs in the Wild section documents actual bugs found in different codebases throughout the ecosystem. The Common Vulnerabilities section lists the common categories of bugs seen in ZK applications. It generalizes the types of bugs previously seen so auditors can get a good idea of what to look for.

2. BigInt Audit with Veridise

The Veridise team led an audit of the Circom BigInt library, along with 0xPARC members and blockdev from PSE Security. The audit led to a few warnings for the BigInt library, and Veridise’s formal verification part led to 8 critical bugs within the CircomLib library (which BigInt relies on). This is a great example of why different fields of security require different solutions.

ZK circuits can naturally be expressed as math equations, so they lend themselves extremely well to formal verification. Formal verification has been around, and used for smart contracts to a degree but never became very popular. It’s not trivial to formally verify random code, so it was only done if the security guarantees were worth it. This may actually be true for ZK circuits due to their mathematical constraint nature.

Formal mathematical specifications that include preconditions and postconditions are required for each program. Thus the mathematical equations of the circuits themselves are compared to this specification to ensure that they are equivalent. This would be much harder if the ZK circuits weren’t readily converted to mathematical equations. For example, it is much more difficult to write formal specs for smart contracts. However, it’s important to note that once the specs are created, automating the verification process is easier for smart contracts than for circuits.

3. ZK Circuit Static Analysis with Veridise

The Veridise team along with researchers from UCSB and UT Austin published a paper on statically analyzing ZK circuit code with a little help from the PSE Security team - “Practical Security Analysis of Zero-Knowledge Proof Circuits”. Static analysis refers to analyzing the code without actually executing it. This is a popular method when analyzing smart contract code, such as using TrailOfBits’ Slither tool.

The research has found that a large number of common vulnerabilities in ZK circuits can be found just by statically analyzing the code. Not only that, but the researchers have developed a framework for detecting these vulnerabilities along with 9 different detectors to implement the framework. The idea was instantiated on Circom code but is language-agnostic and can be adapted to other DSLs with little engineering effort.

While formal verification may provide greater security guarantees, static analysis is much easier and quicker to use. The static analysis tools can be automatically run on random Circom circuits without preparation beforehand. Formal analysis, on the other hand, requires formal specs of the circuits so that the circuits can be verified to work properly. A good security review would include both, as formal verification and static analysis are complementary to each other. Static analysis is good for catching common vulnerabilities with well-known patterns whereas formal verification is good for asserting functional correctness. If the specs are well made and the proving language works as intended, formal verification should be able to find all underconstrained bugs.

4. Bridge Bug Tracker

The Bridge Bug Tracker github repo, created by Yufei Li, is a collection of past Ethereum cross-chain bridge hacks along with resources on bridge security. Since 2021, over $2 billion has been stolen from insecure bridges. This is by far the most critical group of bugs exploited over the past few years in the Ethereum ecosystem. Since L2s rely on bridges to transfer assets, how can they be the future of Ethereum scaling if they are at such big risk of exploitation?

It’s not easy to build a secure bridge, but it’s not impossible. The ecosystem has learned a lot from these past exploits and some early bridges have been operating without a single exploit such as Arbitrum’s bridge. This gives hope to a future where users can safely trust transferring their assets to different L2s, but it requires we learn from the mistakes made by previous bridges.

This repo aims to track past bridge hacks and provide insight into what to look for when assessing a bridge’s security. As L2s progress, many different types of bridges have developed and each requires a different security assessment. Therefore it may be too early to tell which types of bridges are fully secure but this is a good start.

How can I contribute?

Both the ZK Bug Tracker and Bridge Bug Tracker are open to community contributions. If you have a ZK bug or bridge hack that isn’t in the respective repo, feel free to make a pull request or create an issue! Ideally, these repos are used and maintained by the community as we all strive to make bridges and ZK projects more secure.

Team Members

If you’re interested in collaborating or just finding out more about PSE security, you can reach out to any of our 3 team members:

Kyle Charbonnet - Team LeadYufei Li - L2 Security Engineer Blockdev - ZK Security Engineer