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

Bringing Aleo and Leo into zkao

We recently brought Leo and Aleo support to zkao, our AI-powered bug-detection tool, and put it to work on a real engagement with HumanityLink. Getting an LLM to audit a young ecosystem like Aleo turned out to be less about the model and more about what we fed it - custom prompts or skills so it actually recognizes Aleo bug patterns, a harness called cheatVM that turns findings into real end-to-end proofs of concept instead of code that just looks right, and a clear threat model that significantly cut down our false positives.

zk/sec, False Witness team · July 20, 2026

Cryptography challenges @KalmarCTF 2026

Minsun shares a high-level overview of the hard cryptography challenges he authored for KalmarCTF 2026, focusing on the broader ideas behind their design and solutions. The post reflects on how subtle randomness failures and algebraic structure can lead to deep vulnerabilities.

Minsun Kim · April 28, 2026

noname 3.0: Native Hints, Standard Library, Compiler Visualizer, And More!

We're super excited to introduce noname 3.0, our zk programming language inspired by Rust and Golang, now achieving full feature parity with Circom. This update brings native hints, a standard library, debugging features, and a lot more to enhance developer experience. Dive into how hint functions work with an 'unsafe' keyword to balance innovation and security, explore our new stdlib modules, and see how the compiler pipeline visualizer can help you understand the compiling process. Plus, check out our next steps and how you can contribute to shaping noname's future.

ZK/SEC · November 13, 2024