Mastering o1js on Mina: Four key strategies for secure development

If you’re building on the Mina blockchain, this blog post is a must-read.

After completing an extensive security audit of the o1js v1 library — spanning 39 person-weeks with 4 security analysts — we’ve gained a comprehensive understanding of the framework. We’re eager to share our insights with the community.

To help you develop securely with the o1js TypeScript library, we’ve distilled our findings into four topics. In this post, we highlight common pitfalls, share real-world examples of vulnerabilities, and provide actionable guidance to ensure your projects harness o1js effectively and securely.

Writing ZK Circuits with o1js and TypeScript

o1js brings cutting-edge technology to developers, enabling them to write ZK circuits in TypeScript and seamlessly deploy them to the Mina blockchain. While o1js abstracts much of the complexity of zero-knowledge proofs, it also introduces unique challenges and anti-patterns that developers must carefully navigate.

In this post, we dive into four illustrative examples:

• Example #1: Trust the Types
• Example #2: It’s still ZK under the hood: No conditional data flow!
• Example #3. Account Updates: Mastering on-chain state management
• Example #4: Don’t get DoS’ed: Actions & Reducers

Let’s dive in!

Example #1: Trust the Types

A UInt64 type is a supposed to represent a value in the range [0, 2⁶⁴), i.e. 0, 1, 2, 3, …, up to 18,446,744,073,709,551,615

UInt64.assertLessThan() allows you to assert that a certain value x is less than another value

Provable.runAndCheck(() => {
  // Introduce a UInt64 variable in the program
  let x = Provable.witness(UInt64, () => {return new UInt64(100n);});
  // Prove the variable is at most 2**48
  x.assertLessThan(new UInt64(2n**48n));
})

In the above program, all we prove is that x is some number less than 2⁴⁸. We set x to 100 in our generator, but anyone can change the witness generator. More specifically, anything inside the Provable.witness function is not proven! x can have any value, so long as it satisfies the constraints!

But where are constraints defined?

Provable.witness(UInt64, ...) adds constraints defined in UInt64.check() to ensure that verification won’t succeed unless x is in the range [0, 2⁶⁴)

x.assertLessThan(new UInt64(2n**48n)) then asserts that x is in the range [0, 2⁴⁸)

So far so good….

Now a clever user looks at this and might think: “Why check x is in [0, 2⁶⁴) if we are going to check x is in [0, 2⁴⁸) anyway? We can just do the second check!”

// BUG IN CODE: DO NOT USE
Provable.runAndCheck(() => {
  // Introduce an unconstrained variable in the program
  let xAsField = Provable.exists(1, () => {return new UInt64(100n);});
  // Unsafe cast it to a UInt64. This adds no constraints
  let x = UInt64.Unsafe.from(xAsField);
  // Prove the variable is at most 2**48
  x.assertLessThan(new UInt64(2n**48n));
})

While this looks innocuous, it is actually under-constrained! We can use values for x which are much larger than the input field.

Why?

• UInt64.assertLessThan() assumes that we already know x < 2**64. Under the hood, it then asserts that 2⁴⁸ – x is in the range [0, 2⁶⁴). Remember that x is really a field element, so all arithmetic occurs modulo p for some large p, and we can think of the range [0, p) as all possible values of x!

The implementation has the following cases:

1. If x ∈ [0, 2⁴⁸), then 0 ≤ 2⁴⁸ — x < 2⁴⁸ < 2⁶⁴, so the check passes ✅
2. If x ∈ [2⁴⁸, p + 2⁴⁸ — 2⁶⁴), then 2⁶⁴ ≤ 2⁴⁸ — x, so the check fails p + 2⁴⁸ — 2⁶⁴ ≈ p ≈ 2²⁵⁴ (note p + 2⁴⁸ — 2⁶⁴ ≈ p ≈ 2²⁵⁴ ) ✅ (just like we want)
3. If x ∈ [p + 2⁴⁸ — 2⁶⁴, p) (i.e. the 2⁶⁴ — 2⁴⁸ — 1 largest elements in the field, much larger than 2⁴⁸), then the computation overflows all the way back into the range 0 ≤ 2⁴⁸ — x < 2⁴⁸! ❌ This is bad: the check will pass but x is much larger than 2⁴⁸

This is why we can’t cheat: we need the constraint x ∈ 2⁶⁴ from Provable.witness(UInt64, ...) to eliminate this 3rd “bad case”.

Example #2: It’s still ZK under the hood: No conditional data flow!

One common mistake we’ve seen across ecosystems comes from a limitation of ZK itself: the circuit’s control flow is entirely static.

No if/else

How can we do computations then? Conditional data flow.

Instead of

if case1 {
  x = f(y)
}
else {
  x = g(y)
}

We have to compute f(y), compute g(y), and then set

x = case1 ? f(y) : g(y)

Of course, in o1js this would look like

x = Provable.if(
  case1,
  MyProvableType, // tell o1js the type to use
  x,
  y
)

How can this cause issues? We often want to do computations which might succeed. A classical example is division: division-by-zero is undefined.

Suppose we are implementing a simple vault. The vault holds funds. You can deposit funds equaling 1% of the currently managed funds, and the vault will mint you a number of tokens equal to 1% of the currently existing tokens.

For example, imagine the supply of vault Tokens is 1000 Token, and the vault is holding 100 USDC. If I deposit 1 USDC, the vault will mint me 1 USDC * 1000 Token / 100 USDC = 10 Token. If I deposit 10 USDC, the vault will mint 10 USDC * 1000 Token / 100 USDC = 100 Token.

Ignoring decimals, this might be written simply as

amountToMint = totalSupply.mul(depositedAmount).div(managedFunds)

But what about the starting case? Suppose there are no funds and we are the first depositor. Commonly, we will set some fixed ratio: e.g. mint 1 token per initial USDC deposited. A first attempt at implementing this might be the below:

// BUG IN CODE: DO NOT USE
amountToMint = Provable.if(
  managedFunds.equals(new UInt64(0n)),
  UInt64,                               // Output type
  depositedAmount,
  totalSupply.mul(depositedAmount).div(managedFunds)
)

This looks like it will work: if no funds are currently managed, amountToMint is depositedAmount. Otherwise, we compute the ratio of tokens to managed funds.

The problem is simple: we always compute totalSupply.mul(depositedAmount).div(managedFunds), even when managedFunds is equal to zero. To guarantee its correctness, UInt64.div() will cause an assertion failure when the denominator is zero.

This may seem not so bad: we’ll catch it during testing. The problem is, it isn’t always so obvious. For example, what if the above contract starts with a non-zero amount of funds/total supply set up before the vault was opened to the public? Then this issue will only manifest if the managedFunds reaches 0, at which point it can never be deposited into again.

A more serious (but analogous) example could prevent the last user from withdrawing from the vault.

Example #3: Account Updates: Mastering on-chain state management

While o1js looks a lot like other popular smart contract languages, there are some important differences.

Each @method creates an AccountUpdate: A single object representing a change of on-chain state. These AccountUpdates have preconditions on the state to ensure valid access. For example, if I am decreasing a smart contract Mina balance by 10, the node must validate the account has at least 10 Mina—even if I have a proof that I executed the smart contract correctly.

Why? Remember that ZK is “state-less:” it has no hard drive, disk, or memory. All you prove is that, for some inputs which only you know, you did the correct computation.

When dealing with on-chain values, we need to prove that we used the actual on-chain values, and not just some random numbers! How? We output the “private-input” as “public preconditions” of the AccountUpdate. The node can then check the public preconditions

With state, we do this via the getAndRequireEquals() function. o1js will cause an error if you call get() without getAndRequireEquals(). It will now also call an error if you getAndRequireEquals() with two different values, due to an issue reported by Veridise (see #1712 Assert Preconditions are not already set when trying to set their values)

Let’s take a simple example.

// BUG IN CODE: DO NOT USE
export class Pool extends SmartContract {
  @state(Boolean) paused = State<Boolean>();

  @method function mint(amount: UInt64): UInt64 {
    this.paused.get().assertFalse("Pool paused!");
    // Minting logic
  }
}

The above snippet is intended to prevent minting when the protocol is paused. In actuality, it just proves that the prover set paused to False in their local environment when generating the proof. To ensure that the network validates this assumption, the code should instead use getAndRequireEquals(). This way, the assumption paused = False is included in the AccountUpdate as part of the proof, forcing the network node to validate that the on-chain protocol is not paused.

export class Pool extends SmartContract {
  @state(Boolean) paused = State<Boolean>();

  @method function mint(amount: UInt64): UInt64 {
    this.paused.getAndRequireEquals().assertFalse("Pool paused!");
    // Minting logic
  }
}

Example #4: Don’t get DoS’ed: Actions & Reducers

Preconditions can cause problems when concurrent accesses are occurring. Say you and I are both incrementing a counter. Our AccountUpdate will have two important parts:

• A precondition that the current counter value is the old value x
• A new value for the counter: x+1

If you and I both call this function when x = 3, we both have a precondition x=3! That means whichever one of us is executed second will have our AccountUpdate fail, since after the first person goes, x = 4 != 3

How can we fix this? We queue up actions.

Mina has a feature called actions & reducers. You can submit an “Action”, which gets put in a queue. Later, users can call a “reducer” which calls a function on those actions

Let’s look at an example taken from reducer-composite.ts:

class MaybeIncrement extends Struct({
  isIncrement: Bool,
  otherData: Field,
}) {}
const INCREMENT = { isIncrement: Bool(true), otherData: Field(0) };

class Counter extends SmartContract {
  // the "reducer" field describes a type of action that we can dispatch, and reduce later
  reducer = Reducer({ actionType: MaybeIncrement });

  // on-chain version of our state. it will typically lag behind the
  // version that's implicitly represented by the list of actions
  @state(Field) counter = State<Field>();
  // helper field to store the point in the action history that our on-chain state is at
  @state(Field) actionState = State<Field>();

  @method async incrementCounter() {
    this.reducer.dispatch(INCREMENT);
  }
  @method async dispatchData(data: Field) {
    this.reducer.dispatch({ isIncrement: Bool(false), otherData: data });
  }

  @method async rollupIncrements() {
    // get previous counter & actions hash, assert that they're the same as on-chain values
    let counter = this.counter.getAndRequireEquals();
    let actionState = this.actionState.getAndRequireEquals();

    // compute the new counter and hash from pending actions
    let pendingActions = this.reducer.getActions({
      fromActionState: actionState,
    });

    let newCounter = this.reducer.reduce(
      pendingActions,
      // state type
      Field,
      // function that says how to apply an action
      (state: Field, action: MaybeIncrement) => {
        return Provable.if(action.isIncrement, state.add(1), state);
      },
      counter,
      { maxUpdatesWithActions: 10 }
    );

    // update on-chain state
    this.counter.set(newCounter);
    this.actionState.set(pendingActions.hash);
  }
}

In this code, incrementCounter() dispatches an action to the queue requesting an increment. dispatchData() adds a queue with some other unrelated data.

Anyone can process the entire queue by calling rollupIncrements(). This will go through the whole queue, incrementing once for each submitted (but unprocessed) request to increment.

Note:

• The contract is responsible for managing the actionState field, which tracks “where we are in the queue.” In particular, this.actionState tracks what parts of the queue have been processed, while the Mina node automatically tracks what actions have been submitted via dispatch

Suppose that, instead of just incrementing by one, the user provided a number to add (e.g. an account balance change).

class MaybeIncrement extends Struct({
  isIncrement: Bool,
  otherData: Field,
  amount: UInt64
}) {}

// function that says how to apply an action
(state: Field, action: MaybeIncrement) => {
  return Provable.if(action.isIncrement, state.add(action.amount), state);
},

A malicious user could submit several large amounts, e.g.

{
  isIncrement: new Bool(0),
  otherData: new Field(0),
  amount: new UInt64(UInt64.MAX),
}

Action submission will work smoothly, but this single action can permanently prevent all other actions from being processed!

Using this simplified example, the only way to process actions is in a single, large batch. Using more complex constructions like the batch reducer, or a custom rollup proof can get around this issue, but at the time of audit, only simple examples were made available for us to review.

If you decide to use the actions and reducer pattern, the reducer must be guaranteed to succeed once an action is submitted. This means that any arithmetic must be inspected carefully, actions must be strictly validated at submission, and must be canonicalized (see this PR #1759 Canonical representation of provable types, which was developed as a solution to an issue raised during the Veridise audit).

To see what other solutions the O(1) community is working on, check out this article from zkNoid.

Closing thoughts

o1js empowers developers to build cutting-edge zero-knowledge applications on the Mina blockchain, leveraging the simplicity of TypeScript to create and deploy ZK circuits.

However, this power comes with responsibilities. Developers must be vigilant about potential vulnerabilities, from respecting type constraints and avoiding under-constrained circuits to managing state updates effectively and mitigating concurrency risks.

We hope the examples and strategies shared in this blog provide a solid foundation for developing securely on Mina. The challenges and pitfalls of working with zero-knowledge circuits can be intricate, but with careful attention to detail and adherence to best practices, they can be navigated successfully.