ZK/SEC Research notes from zkSecurity
All posts
security · consensus · zk

Public report of Aleo's consensus (Bullshark)

Aleo synthesizer

On October 9th, 2023, zkSecurity was tasked to audit Aleo's consensus for use in the Aleo blockchain. Two consultants worked over the next 3 weeks to review Aleo's codebase for security issues.

The code was found to be thoroughly documented and of high quality. In addition, the team acted in a highly cooperative way and was key in helping us find a number of the issues in this report.

You can find the full report here.

The report was well received by the Aleo team:

apruden

victor

What follows is a copy/paste of the overview section of the report


Bullshark in Aleo

In this section we give an overview of the consensus protocol implemented by Aleo, namely Bullshark.

The Bullshark consensus protocol is the evolution of a long lineage of consensus protocol, perhaps starting with the very first practical one (PBFT). The idea remains more or less the same in most (all?) of these protocols: the set of participant is fixed, and they advance together in rounds:

  1. In the first round, a "leader" broadcasts a proposal.

  2. In the second round, participants vote on the proposal.

  3. In the third round, participants vote on votes.

If you see enough participants who have voted on a proposal, and enough participants have seen that (the "vote on votes" part), then we can "commit" to a proposal. In blockchain lingo, committing a proposal would be to finalize and apply the transactions it contains to the blockchain's state.

This basic 3-step committing process was never really improved. Instead, most major optimizations have been obtained by using pipelining techniques. For example, The Hotstuff protocol introduced pipelining of this flow by having a leader propose in every round. More recently, Bullshark introduced another type of pipelining by having every participant propose in every round. (Another recent protocol Shoal introduces both pipelining techniques in a single protocol.)

More concretely, a round of bullshark between $3f+1$ participants (of which only $f$ can be malicious) goes like this:

  1. At the start of a round, every participant broadcasts a new batch of transactions (which can be thought of as a block) to every other participant. (See at the end of the list how the batch was created.)

  2. If you receive a batch from someone, make sure that it's the only batch you've seen from them in this round, store it, and sign it.

  3. Once you collect $2f+1$ signatures on your batch, this produces a certificate for your batch, which you can broadcast to everyone.

  4. Once you observe $2f+1$ certificates in this round, produce a batch of transactions for the next round in which you also include the $2f+1$ observed certificates. This should look like a directed acyclic graph (or DAG) of batches.

  5. Go back to step 1.

To explain concrete examples in the rest of this report, we use the following types of diagrams:

bullshark

This still doesn't let us know how participants agree on what gets committed. The "commit rule" of Bullshark is quite simple: in every even round (e.g. round 2, 4, etc.) a leader is chosen (for example, via a round-robin election), and their DAG (their batch and all the batches they link to transitively) gets committed if there's $f+1$ certificates referring to it.

A leader's batch is called an anchor, and it is possible that an anchor does not get committed in an even round. But if an anchor gets committed by some honest nodes, it will always be committed later on by all other honest nodes. This is because a committed anchor will always be included in the DAG of another anchor.

This property is called the quorum intersection property and can be proven quite easily. If an anchor is committed in an even round $i$, it is because it was referred to by $f+1$ certificates in round $i+1$. Let's call this set $A$. Any block (including anchor block) in round $i+2$ will have to include $2f+1$ certificates from round $i+1$. let's call that set $B$.

We need to show that $A \cap B \neq \emptyset$, or in other words that the intersection contains at least one certificate, or in other words that when a block is committed then there'll always be a path leading to that block in any block from the next even round. This is not too hard to show: the multiset $|A \cup B| = (f+1) + (2f+1) = 3f+2$ which is 1 vertex more than the total number of vertices in a round and thus has some multiplicities.

As leaders and their anchors can be slow to be proposed and certified, timeouts are added to ensure that participants will wait a certain amount of time for the leader to show up before moving to the next round. Concretely, in even rounds, participants will wait to see an anchor to certify, and will wait for a certified anchor to include in their next proposal. In odd rounds, participants will wait to see votes for an anchor to certify, and will wait for certified votes for an anchor to include in their next proposal.

One last (important) subtlety is that as described, the protocol allows for a node's storage to grow ad-infinitum if they do not observe any commit. To prevent this to happen, a garbage collection protocol is added in order to prune older parts of the DAG as it grows. As such, when a commit happens, the DAG will be traversed up to some "garbage collection frontier", and everything on the left of that frontier will be discarded.

Keep reading
Recommended

Exploring Leo: A Primer on Aleo Program Security

In this blog post, we dive into Aleo, a blockchain platform that leverages zero-knowledge cryptography for creating private and scalable decentralized applications. You'll discover how Leo, its Rust-like programming language, simplifies app development by allowing developers to focus on robust privacy features without delving deep into cryptographic complexities. We also explore Leo's unique design, offering practical tips on avoiding common pitfalls and potential vulnerabilities like underflows and unauthorized access. Whether you're a developer curious about building privacy-focused solutions or just intrigued by blockchain innovation, you'll find valuable insights here.

Suneal Gong · August 07, 2024

Public report of Aleo's synthesizer

We were tasked with auditing Aleo's synthesizer for their blockchain, diving deep into its code and uncovering some important findings along the way. The synthesizer is crucial for deploying and executing user programs, utilizing zero-knowledge proofs to maintain privacy and efficiency. Readers will get a glimpse into how Aleo uses their Leo programming language, the intricate process of synthesizing proof circuits, and how function execution and program deployment flows occur on their platform. This post offers insights into Aleo’s unique approach to tackling challenges similar to those faced by Ethereum but with an innovative twist that includes privacy features and reduced costs.

ZK/SEC · January 02, 2024

Optimistic One-Vote-Round Finality in BFT Consensus

An intuition-first walkthrough of why 33% BFT needs two voting rounds, how 20% designs get true one-round finality, and how an optimistic fast path can bridge the gap.

Suneal Gong · February 02, 2026
More to explore

Archetype x zkSecurity - Proof is in the Pudding: The Other Dark Forest (Offchain Public Keys)

In Session 07 of "Proof is in the Pudding," we explore the other dark forest, the realm of offchain public keys. We dive into zkLogin, ZK Email, and ZKPassport, examining how these protocols handle authentication and privacy. We also discuss the issue of unlinkability in privacy protocols and why replacing traditional signature verifications with zero-knowledge proofs could unlock more interesting and powerful ZK products.

ZK/SEC · October 21, 2025

A Year of ZK Security

A year after launching, we've grown and evolved alongside the world of zero-knowledge proofs, uncovering bugs and learning the ins and outs of ZK technology. From circuit audits to developing our own tools like Circomscribe, it’s been a wild ride. We've discovered how easy it is to misstep with ZK code, especially as these systems grow complex and impact financial security. As zkVMs gain popularity, we're excited about the challenges ahead and are expanding our expertise. Want to dive into the world of ZK with us? Check out our latest projects and even take on our zkBank challenge!

David Wong · May 30, 2024

Verifying Cairo proofs on Ethereum

We've been teaming up with StarkWare to create the EVM adapter, and we're thrilled to say that we've recently verified Cairo proofs on the Ethereum mainnet! Building on the work of Andrew Milson and Aditya Bisht, we're making StarkWare’s technology more accessible to everyone. Our blog dives into how Cairo programs are verified on Ethereum and showcases our new library, `stark-evm-adapter`, which helps parse Cairo proofs for Ethereum. Interested in seeing how it works? Check out our demo and learn how to integrate this tech into your system. Plus, stay tuned for future updates as we refine and expand this exciting tool!

Jason Park · August 06, 2024