Audit of Zeko's circuits

Description. Folder.Make(...) implements a recursive proof of a general state machine.

The proof has a public output of the form { source: Stmt; target: Stmt }. Given some function step: Elt -> Stmt -> Stmt, it asserts that there exists some sequence of elements Elt such that step, when applied repeatedly to the elements, transitions from source : Stmt to target : Stmt.

One of the allowed branches of this proof is a merge rule. It accepts a “left” transition left.source -> left.target and a “right” transition right.source -> right.target, and merges them to the combined transition left.source -> right.target, by verifiying two recursive proofs.

The problem is that the merge rule never does the consistency check that left.target == right.source. Which means that, in the proof output, nothing forces source and target to be related in any way.

Impact. Folder is used throughout the rollup contracts for critical components, such as the different variants of Ase (action state extension) which prove that one action state is the result of applying actions to another. Consequently, this issue entirely breaks the bridging protocol and allows users to prove arbitrary actions on either the L1 or the L2.

For example, this could be exploited by anyone to withdraw all available tokens from the L1 bridge contracts, by witnessing an L2 withdrawal action that didn’t actually happen.

Recommendation. Add the missing consistency check to Rule_merge.main:

let%snarkydef_ main (w : Witness.t V.t) =
  let* Witness.{ left; left_proof; right; right_proof } =
    exists ~compute:(V.get w) Witness.typ
  in
+ let* () = assert_equal Stmt.typ left.target right.source in
  let new_stmt : Trans.var =
    { source = left.source; target = right.target }
  in
  Checked.return
    Compile_simple.
      { prevs =
          Two_prevs
            ( { proof_must_verify = Boolean.true_
              ; public_input = left
              ; proof = left_proof
              }
            , { proof_must_verify = Boolean.true_
              ; public_input = right
              ; proof = right_proof
              } )
      ; out = new_stmt
      }

Client Response. The issue was fixed as recommended.

Description. Zeko tracks all accounts in an account set, a Merkle tree. We found a bug which means a prover can update the account set in arbitrary ways. The issue allows sequencers to prove invalid state transitions with far-reaching consequences, like double-spending of L2 deposits.

First, some background. In contrast to the main account ledger, another Merkle tree used by Mina, Zeko’s account set supports non-inclusion proofs, thanks to being an indexed Merkle tree. For more on indexed Merkle trees, see the paper that introduced them and this talk and blog post by Aztec.

The account set construction exists to close a gap in Mina’s “transaction snark”, the circuit(s) that Zeko uses to prove valid state transitions of the L2 ledger. In the original transaction snark, when processing an account update, the prover is free to either prove it belongs to an existing account in the current ledger, or to witness a Merkle path to an “empty” account. In the empty case, no connection to the account id of the account update is proved. The empty account is updated to have the acount id matching the account update, and this update is recorded in the ledger. This is how new accounts are created in the protocol.

In other words, nothing in Mina’s original circuit prevents a prover from creating the same account multiple times, and picking to which of these to apply updates later on. The Mina L1 relies on consensus to prevent duplicated accounts from being accepted. Zeko, on the other hand, is centralized and doesn’t have consensus, and must rely on proofs to guarantee that only valid state transitions are performed on its L2.

This is where the account set comes in. In Zeko, every processed account, along with its “is empty” flag, is passed to a function called update_acc_set. If the flag is true, the function will prove that the account doesn’t exist in the account set yet, and insert it. This is just the piece of circuit logic missing from the original transaction snark.

let update_acc_set accounts init ~witness =
  Checked.List.fold accounts ~init
    ~f:(fun set (account_id, is_empty_and_writeable) ->
      (* ... ZKSECURITY: skipping lines ... *)
      let* y = derive_token_id ~owner:account_id in
      (* ZKSECURITY: `y`, a hash of the `account_id`, is added to the set. *)
      let* `Before_adding_y set', `After_adding_y new_set =
        Account_set.add_key_var ~x ~path_x ~y ~path_y ~z
          (* ZKSECURITY: Via the `check` flag, an insertion is skipped for
             accounts that already existed *)
          ~check:is_empty_and_writeable ()
      in
      let*| () = assert_equal ~label:__LOC__ Account_set.typ set set' in
      new_set )

The problem happens in the case where is_empty_and_writeable is false, and y is in the tree already. Note that in this case, we don’t really want to perform any check here, since elsewhere we already proved inclusion of the account_id in the main ledger. To skip the check, this function passes check:false to Account_set.add_key_var.

Let’s look at add_key_var, the main method on Zeko’s indexed Merkle tree implementation. The function inserts a node y in the tree, using witnesses x and z such that {key: x, next_key: z} exist in the original tree and x < y < z. It turns out that the method is both over- and under-constrained if the check is false and y was already in the tree.

let add_key_var ?check ~x ~path_x ~y ~path_y ~z () =
  let* () =
    with_label __LOC__ (fun () -> assert_x_less_than_y_less_than_z ~x ~y ~z)
  in
  (* ZKSECURITY: after showing that x < y < z, we prove inclusion of `(x, z)` in the input root.
     this alone implies that y did not exist in the tree before! *)
  let* root = implied_root { key = x; next_key = z } path_x in
  let* root_intermediate = implied_root { key = x; next_key = y } path_x in
  (* ZKSECURITY: `root_intermediate'` commits to _some_ tree has an empty entry for `y`.
     But this root is not connected to the input root yet... *)
  let* root_intermediate' =
    implied_root_raw Field.(constant typ zero) path_y
  in
  let* root_intermediate' =
    match check with
    | Some check ->
        if_ check ~typ:F.typ ~then_:root_intermediate'
          ~else_:root_intermediate
    | None ->
        Checked.return root_intermediate'
  in
  (* ZKSECURITY: we check that `path_y` really belongs to the same tree as `path_x`,
     by asserting the roots are equal. But this assertion is SKIPPED if check=false *)
  let* () =
    assert_equal ~label:__LOC__ F.typ root_intermediate root_intermediate'
  in
  (* ZKSECURITY: we update the root with the insertion of y and return it.
     this is a valid insertion if check=true or None, but an unconstrained update if check=false. *)
  let* root_new = implied_root { key = y; next_key = z } path_y in
  Checked.return (`Before_adding_y root, `After_adding_y root_new)

There are two issues:

1. The input root is over-constrained: If y is already in the tree of Before_adding_y root, then the first check assert_x_less_than_y_less_than_z must fail. This is a core property of indexed Merkle trees, maintained by this function by updating x’s next_key to y. It means that update_acc_set fails for accounts already in the set.

2. The output root is under-constrained: Using check: false makes the function skip the check that root_intermediate == root_intermediate'. This means that path_y is not validated to be a path in the same tree, and the updated root After_adding_y root_new could belong to any tree.

In update_acc_set, the returned root is just accepted as the new value. Because of the second issue, the prover could just switch to a different account set whenever an account already existed (i.e. during a majority of transactions).

Impact. The over-constrainedness issue simply means that the implementation would not have worked. Note that the audited code is very new and was not tested prior to the audit.

The more serious issue is the second one, which would not have surfaced on its own: Exploiting it, a prover can add the same account to the L2 ledger multiple times. This is just the problem that the account set was there to address in the first place.

For an example attack enabled by non-unique accounts, consider the bridge method for finalizing an L2 deposit. It prevents double-spending of the deposit by tracking a deposit_index field on a specific receiver account. If that account could be added another time, the same deposit can be withdrawn again.

Such a double-spending attack might only be accessible to the sequencer (depending on the exact operating setup of the rollup). But that seems bad enough, as we want to force sequencers to behave according to the protocol, using zk proofs.

Recommendation. Both issues can be addressed by adjusting add_key_var. To fix the over-constrained input root, the method could accept the root to update as an argument, instead of returning it. If check is false, the input root is replaced (using if-else) with that of an empty Merkle tree, before asserting it to equal the root implied by the (x, z) node. In this case, the witnesses passed in for x and z need to be the default min and max nodes that are in the indexed Merkle tree initially, to make sure the assert_x_less_than_y_less_than_z passes.

To fix the under-constrained output root, we just need another if-else at the end that replaces the output with the original input root, if check is false.

Client Response. The issue was fixed, by swapping out the original root in add_key_var in the check=false case. This addresses both the soundness and the completeness issue, without changing the function signature.

This finding was indicated to us by the Zeko team during the audit. We include it here for completeness and to flesh out its impact.

As explained in the protocol spec, Zeko plans to deploy multiple bridge accounts on the L1 for the same token. This is a conservative measure: Just one of the accounts will be enabled at any given time, which means that even in the case the rollup is hacked, most of the L1 funds are inaccessible to the hacker.

However, using the code base at the time of audit, deploying multiple versions of the same bridge contract would enable double-spending by processing the same withdrawal on each of the accounts.

Double-spending prevention works by checking a certain state field called next_withdrawal on a helper_account. This account has the helper_token_id, which is derived from and owned by the bridge contract itself:

(* ZKSECURITY: helper token id is derived from bridge account *)
let helper_token_id =
  let account_id =
    Account_id.Checked.create public_key
      (constant Token_id.typ token_id_l1)
  in
  Account_id.Checked.derive_token_id ~owner:account_id

(* ... ZKSECURITY: skipping lines ... *)

let helper_account =
  { default_account_update with
    public_key = base_params.recipient
  (* ZKSECURITY: this account is only unique if `helper_token_id` is *)
  ; token_id = helper_token_id
  ; authorization_kind = authorization_signed ()
  ; use_full_commitment = Boolean.true_
  ; may_use_token = constant May_use_token.typ Parents_own_token
  (* ZKSECURITY: if this account is not unique, we can do the state update
     multiple times with the same `next_withdrawal` index,
     which means we can double-spend a withdrawal *)
  ; update =
      { default_account_update.update with
        app_state =
          Outer_user_state.fine
            { next_withdrawal = Some next_withdrawal
            ; next_cancelled_deposit = None
            }
          |> var_to_app_state_fine

The problem with multiple L1 bridge contracts is that we also get multiple different helper accounts, and so the fact that next_withdrawal is incremented on one of them doesn’t prevent us to repeat the withdrawal using another of them.

The same issue is present in the method for cancelling a deposit, which also must only be allowed once since it involves paying back the deposit.

The solution to this issue is already outlined in the bridge-spec.md: There is a single zkapp called helper_token_owner_l1, which owns the helper_account token id, and sits between the bridge and helper account updates in a transaction similar to the one above.

Recommendation. Implement the helper_token_owner_l1 and add it to the withdrawal and cancel-deposit rules. This zkapp needs two methods, one for withdrawal and one for cancel-deposit, which produces the account update layout needed by the bridge rules without further restrictions on when the method can be called.

Note that there’s currently no way to assert the helper_token_owner_l1 is only called in the context of a bridge call, but this is fine since, thanks to signature authorization_kind on the helper_account, only the recipient of the withdrawal could ever call this method. So, this allows voiding a withdrawal by user error, but not maliciously for a different user.

Client Response. The issue was fixed in commit cf78d9.

Description. For its indexed Merkle tree, Zeko implements an $x>y$ assertion where x and y can range over the full field. This is achieved by representing x and y as bigints.

The conversion of field elements to bigints works by asserting that

Here, $x$ is the field element, $(x_0,x_1,x_2)$ its representation as bigint, $\ell =88$ is the limb size, and $fp$ is the native field size.

Because $3\ell =264$ is more bits than the field size, the split of x into limbs is underconstrained: It allows to convert x into a bigint that represents x plus a small multiple of $fp$, like $x+fp$ for example.

In order to assert that $x>y$, we need to confirm two conditions:

1. The bigint version of $x$ is larger than that of $y$
2. The bigint version of $x$ is less than $fp$

To see why the second condition is necessary, imagine we chose a bigint representation of $x+fp$. In that case, the first point would just prove that $x+fp>y$, which is trivially true and doesn’t tell us that $x>y$.

The second check can be performed using sub_then_dec which calculates $fp-x-1$ and range-checks the result. However, in assert_greater_than_full, this step is done with y instead of x as input, and therefore only checks that $y<fp$.

let* () =
sub_then_dec
    ~dec:Field.(constant typ one)
    ~x0:(constant Field.typ fp0) ~x1:(constant Field.typ fp1)
    ~x2:(constant Field.typ fp2) ~y0 ~y1 ~y2
(* ZKSECURITY: we range-checked fp - y - 1, which doesn't help *)

With the $x<fp$ check missing, the gadget is unsound, and can be trivially exploited to “prove” $x>y$ even if $x\le y$ by adding a multiple of the modulus to the bigint $x$.

Impact. Faking a less-than assertion allows you to break the indexed Merkle tree and add duplicate entries. Due to its use for the account set, the finding lets the prover make old accounts appear as if they are new. As explained in the intro, this implies attacks like double-spending L2 deposits, by any entity that is able to call the commit rule on the L1.

Recommendation. Update the code to ensure that x0, x1, and x2 are passed to sub_then_dec as the y0, y1, and y2 parameters.

Client Response. The issue was fixed as recommended.

Description. The sub_then_dec function performs subtraction between two big integers $x$ and $y$ (represented as three limbs) and then decremented by a constant $dec$ which can be 0 or 1. There are also two big integers $z$ and $w$ which represent the result of $x-y$ and $z-dec$, respectively.

The current implementation of sub_then_dec applies the multi-range check constraint to the intermediate result $z$ instead of the final result $w$, as seen in the following lines of code:

let sub_then_dec ~dec ~x0 ~x1 ~x2 ~y0 ~y1 ~y2 =
    let* (z0, z1), z2 =
    exists
        Typ.(F.typ * F.typ * F.typ)
        ~compute:
        (let- x0 in
            let- x1 in
            let- x2 in
            let- y0 in
            let- y1 in
            let- y2 in
            Zeko_as_prover.sub ~x0 ~x1 ~x2 ~y0 ~y1 ~y2 |> As_prover.return )
    in
    let* (w0, w1), w2 =
    exists
        Typ.(F.typ * F.typ * F.typ)
        ~compute:
        (let- z0 in
            let- z1 in
            let- z2 in
            Zeko_as_prover.sub ~x0:z0 ~x1:z1 ~x2:z2 ~y0:Field.one
            ~y1:Field.zero ~y2:Field.zero
            |> As_prover.return )

    (* ... ZKSECURITY: skipping lines ... *)

    in
    (* ZKSECURITY: this should have been w0 w1 w2 *)
    multi_range_check z0 z1 z2

The idea of the check is that by proving $w=x-y-1\ge 0$, you guarantee that $x>y$. Because the function only performs a range-check on the intermediate value $z=x-y$, it only shows that $x\ge y$.

Consequently, when sub_then_dec is used within assert_greater_than_full, it allows x and y to be equal.

Impact. This “off-by-one” error is enough to break the indexed Merkle tree: You can insert an existing entry y by providing itself as low node witness $x:=y$ and then “prove” that $x<y$. Thus, this finding breaks the account set.

Recommendation. Update the multi_range_check statement to apply it to (w0, w1, w2).

Client Response. The issue was fixed as recommended.

Description. Kimchi, the proof system underlying Zeko, supports “multi-range checks”: using a combination of 3 gates (2x range_check0 and 1x range_check1) to perform an 88-bit range check on all three limbs of a 264-bit bigint. These range checks were originally added to Kimchi to support foreign field arithmetic, and were later reused for bigint arithmetic on the native field, to enable relatively cheap full-field comparisons.

However, circuits using multi-range checks were only added to o1js, Kimchi’s TS “frontend”, and not to the OCaml frontend snarky that Zeko uses. Therefore, Zeko had to reimplement some gadgets down to the most low-level parts, like multi_range_check and wrappers around the range_check0 and range_check1 gates.

In multi_range_check, two calls to range_check0 serve to range-check the lower 64-bits of each of the lower two limbs. The remaining 24 bits of each of those limbs are left to be range-checked by range_check1 (which uses up two PLONK rows, with 4 12-bit lookups each). To enable this, range_check0 returns two 12-bit slices of the limb, and passes them to range_check1.

let multi_range_check x y z =
    let* v0p0, v0p1 = range_check0 x in
    let* v1p0, v1p1 = range_check0 y in
    range_check1 ~v2:z ~v0p0 ~v0p1 ~v1p0 ~v1p1

Unfortunately, range_check0 returns the wrong 12-bit slices: (v0p4, v0p5) instead of (v0p0, v0p1). As a result, some slices are range-checked twice while v0p0, v0p1 and v1p0, v1p1 (the most significant slices of their respective limb) are not range-checked at all.

Due to the mistake, the entire multi-range check is ineffective, since an arithmetically valid decomposition of each limb can move an arbitrarily large value into the unchecked slices. With its multi-range check turned off, the higher-level assert_greater_than_full x y gadget can successfully be called with any x and y.

Impact. As in the two previous findings, the indexed Merkle tree is broken and the prover is free to insert entries that already existed.

Recommendation. Change the return values of range_check0 to be (v0p0, v0p1).

Client Response. The issue was fixed as recommended.

Description. On Zeko, withdrawals to the L1 are subject to a withdrawal_delay: a minimum time that must pass before the withdrawal can be finalized, counted in number of slots since the first L1 commit which includes the L2 withdrawal transaction.

We found that the method to finalize a withdrawal does not actually check that the withdrawal is contained in the mentioned commit. Consequently, a caller of the method could witness an unrelated, much older commit. In that case, the check that withdrawal_delay slots passed since the commit tells us nothing about the withdrawal itself. In other words, the withdrawal delay is not enforced.

In contrast to the implementation, the pseudo-code in bridge-spec.md does include an assertion that enforces the withdrawal delay:

(* ZKSECURITY: this is pseudo-code taken from the spec *)
let do_finalize_withdrawal
  (* ... ZKSECURITY: skipping lines ... *)
  let inner_action_state =
    List.append actions_after_withdrawal withdraw_action withdrawal_params :: action_state_before_withdrawal
  in
  let outer_action_state =
    List.append actions_after_commit @@ Commit commit :: action_state_before_commit
  in
  (* ZKSECURITY: the following assertion is MISSING from the implementation! *)
  assert commit.inner_action_state = inner_action_state ;
  let inner_action_state_length = List.length actions_after_withdrawal + 1 + withdrawal_index in
  { account_id = holder_account_l1
  ; balance_change = -withdrawal.amount
  ; may_use_token
  ; authorization_kind = Proof
  ; children =
    [ { public_key = helper_token_owner_l1
      (* ... ZKSECURITY: skipping lines ... *)
      }
    ; { public_key = zeko_pk
      ; authorization_kind = outer_authorization_kind
      ; preconditions =
        { action_state = outer_action_state
        ; app_state = { inner_action_state ; inner_action_state_length ; paused = false }
        ; valid_while =
          { lower = commit.valid_while.upper + withdrawal_delay
          ; upper = infinity }
        }
      }
    ]
  }

However, in our view, that spec design is also not ideal because it imposes tight bounds on when it is possible to withdraw at all. To understand this point, note that in the pseudo-code, the inner_action_state has to precisely match the rollup’s current app state:

      ; preconditions =
        (* ... *)
        ; app_state = { inner_action_state ; inner_action_state_length ; paused = false }

Because of this, the assertion commit.inner_action_state = inner_action_state implies that this is in fact the most recent commit; since any later commit would overwrite the app state with a different inner action state.

But the transaction is only allowed at least withdrawal_delay slots after the commit:

      ; preconditions =
        (* ... *)
        ; valid_while =
          { lower = commit.valid_while.upper + withdrawal_delay

That means, for your withdrawal to succeed, you have to know the latest commit, wait for the withdrawal delay, and only then squeeze in your transaction before the next commit comes along.

Depending on how long the withdrawal delay is and how frequently commits happen, this might only leave a small time window in which withdrawal is even possible. Also, it makes it easy for rollup sequencers to prevent any withdrawals just by committing too often.

Impact. Turning back to the issue that withdrawal delays are not enforced: This will not be a problem as long as the rollup operates normally.

The withdrawal delay is a defense-in-depth mechanism. The idea is that, when the rollup gets hacked or is known to be vulnerable, it can be paused, which makes withdrawals impossible. The delay simply makes sure that there is enough time for honest operators to pause the rollup in such a scenario, before funds are lost to the attacker.

Because of the issue we found, the pausing mechanism is unlikely to help, since an attack can commit (potentially invalid state) and withdraw in a single transaction.

Recommendation. The issue should obviously be fixed, but we advise against following the current spec. The witnessed commit should not be required to exactly have commit.inner_action_state = inner_action_state.

Instead, a third ASE should be used to show that there is a line of actions starting from the withdraw_action and ending at commit.inner_action_state. This would let you use any commit which includes the withdrawal, not necessarily the latest one.

Client response. The issue was fixed in commit c291d4d by connecting the commit’s inner action state to the end of the withdrawal ASE. It turns out no third ASE was needed: the withdrawal ASE was freed up to be used for this purpose, by no longer tying its target to the rollup’s Outer_state. In fact, the method doesn’t need any precondition on the Outer_state.inner_action_state: the fact that the withdrawal is contained in the commit, and the commit is contained in the outer action state, is enough to show that the withdrawal happened on a valid L2.

This finding was pointed out to us by the Zeko team during the audit. We include it here for completeness and to flesh out its impact.

Description. To withdraw tokens from the L2, users need to first send them to the “inner” bridge account. Later, they finalize the withdrawal on the L1 by witnessing the L2 transaction.

The same L2 account is also used to send out funds for finalizing deposits, and in that method it functions as a “token contract”: It controls a child account that stores the deposit index in its state.

To make the deposit design secure, the inner bridge account needs to have its “access” permission set to “proof”. Otherwise the deposit index on child token accounts could be manipulated with unproved transactions.

However, “access = proof” implies that it’s not possible to simply send tokens to the inner bridge contract, without a dedicated method on that contract to support receiving. Currently, this method is missing.

In other words, in the current design, it’s possible to deposit tokens into the L2 but impossible to withdraw them.

Impact. It seems likely that this issue would have been noticed quickly after deploying or testing the rollup. It might have necessitated a redeployment, manual repayment of funds and other damage control.

Recommendation. Add the missing “receive” rule on the inner bridge contract.

Client response. The issue was fixed, and the receive rule added in commit ea5b251.

Description.

In Zeko, slot ranges define time windows during which specific operations are valid. When multiple operations are batched together, their slot ranges need to be merged to find a valid intersection.

let merge_slot_ranges (x : Slot_range.var) (y : Slot_range.var) :
    Slot_range.var Checked.t =
  let* lower =
    Slot.Checked.(x.lower < y.lower)
    >>= if_ ~typ:Slot.typ ~then_:y.lower ~else_:x.lower
  in
  let*| upper =
    Slot.Checked.(x.upper < y.upper)
    >>= if_ ~typ:Slot.typ ~then_:x.lower ~else_:y.lower
  in
  ({ lower; upper } : Slot_range.var)

We found a bug where when determining the upper bound of the merged range, it incorrectly uses the lower bounds (x.lower or y.lower) instead of the upper bounds (x.upper or y.upper). This could lead to deposits being incorrectly marked as timed out and users might lose the ability to reclaim funds when they should be able to. The sequencer might fail to create valid transaction batches and valid transactions could be rejected due to invalid time windows.

Impact. It seems likely that this issue would have been noticed quickly after deploying or testing the rollup. It might have necessitated a redeployment, manual repayment of funds and other damage control.

Recommendation. Use the upper bounds to get the merged upper bound.

  let*| upper =
    Slot.Checked.(x.upper < y.upper)
-    >>= if_ ~typ:Slot.typ ~then_:x.lower ~else_:y.lower
+    >>= if_ ~typ:Slot.typ ~then_:x.upper ~else_:y.upper

Client Response. The issue has been fixed.

Description. In Mina’s original transaction snark, invalid transactions are processed without error, but have no effect except that their fee payments are applied. In other words, if your transaction fails, you don’t get your transaction fee back.

Zeko chose to change this behaviour: It doesn’t apply fees for invalid transactions. To ensure this, constraints are added to the transaction snark designed to make it impossible to prove the state transition that belongs to a failed transaction.

We believe the change, as currently made to the Mina code base, is ineffective.

The following line is added in Zkapp_command_snark.main:

(* ZEKO NOTE: We do not accept failure. *)
with_label __LOC__ (fun () -> Boolean.Assert.is_true local.success) ;

However, before this line is called, the account update in question was fully processed, with the following logic at the very end (in zkapp_command_logic.ml, Make(...).apply):

let local_state =
  (* Make sure to reset the local_state at the end of a transaction.
      The following fields are already reset
      - zkapp_command
      - transaction_commitment
      - full_transaction_commitment
      - excess
      so we need to reset
      - token_id = Token_id.default
      - ledger = Frozen_ledger_hash.empty_hash
      - success = true
      - account_update_index = Index.zero
      - supply_increase = Amount.Signed.zero
  *)
  { local_state with
    ledger =
      Inputs.Ledger.if_ is_last_account_update
        ~then_:(Inputs.Ledger.empty ~depth:0 ())
        ~else_:local_state.ledger
  ; success =
      Bool.if_ is_last_account_update ~then_:Bool.true_
        ~else_:local_state.success

In words: if this was the last account update in the transaction, local_state.success is reset to true, no matter its value up until then.

Therefore, in the is_last_account_update case, the assertion that requires .success to be true has no effect: It happens too late in the logical flow.

Impact. Assessing the impact with 100% certainty is infeasible as it relies on the details of a large amount of out-of-scope code (the entire transaction snark). But from reviewing the diff to Mina, and the way Zeko uses the transaction snark, it seems likely to us that failing transactions are not ruled out, and are allowed to behave the same as in Mina’s original code, with fees applied.

Recommendation. We recommend to add the assertion Boolean.Assert.is_true local_state.success inside apply, right before local state is reset in the code section quoted above. This is the appropriate location for such an assertion, and comes for free even if added in addition to the assertion that already exists.

Client Response. The issue was fixed, by modifying the definition of add_check, the method used to set local_state.success to false. Instead of doing that, it now asserts that the input check passes, so that success can never become false. In addition, the recommended assertion was also added.

Description. We found instances where Zeko’s outer contract only guarantees correct behavior under additional assumptions on the initial rollup state.

• The initial account set acc_set must contain the same accounts as the initial ledger ledger_hash
  • It it contains fewer, accounts can be added twice; if it contains more, some accounts can never be processed. Both can have serious security implications.
• The initial nodes in the account set must form a linked list ordered by key, and there has to be a minimum and maximum node such that hashes outside the min-max range can not be efficiently computed.
  • Again, if this is not the case it could allow duplicated accounts or forbidden accounts.
• Genesis ledger accounts must not contain positive token balances, unless they either legitimately correspond to initial funds in the L1 bridge contracts; or serve as liquidity for L2 bridge contracts that cannot be withdrawn in any way except by finalizing L2 deposits.
  • Note: Details depend on the permissions configuration on these accounts, which is not part of the codebase yet.

Finally, the commit rule assumes that the inner rollup account is stored at the left-most node in the ledger Merkle tree. It does check the public key of that account matches the expected one, but does not check the token id:

(* We check that we're dealing with the correct account. *)
let* () =
  with_label __LOC__ (fun () ->
      PC.Checked.Assert.equal old_inner_acc.public_key
        (constant PC.typ inner_public_key) )
(* ZKSECURITY: we didn't check the token id, so it could still be an incorrect account *)

If the left-most tree node would contain a different account (with the same public key), the sequencer can potentially commit L2 actions that don’t correspond to L2 transactions. This could be exploited to, for example, withdraw tokens the sequencer doesn’t own.

In summary, security critically relies on the correctness of initial state on the outer rollup account.

Zeko’s contracts don’t contain any provable initialization logic, which means that initial state must be set in a signed transaction by the controller of Zeko’s private key, before (potentially) changing account permissions and yielding control over state to the zkapp code.

Impact. On Mina, it’s hard to transparently ensure that an account was initialized correctly. The proved_state state flag shows whether the entire account state was last updated by a proof, but this is not reliable information if the account allows verification key upgrades: the entire state can be swapped out by switching to a different verification key and back, in a single transaction, and proved_state would still be true.

Therefore, any way of verifying correct initialization has to involve looking at the transaction history. However, the assumptions on Zeko’s rollup account are sufficiently complex that even that seems hard to achieve for a motivated user. It’s unlikely that state initialization, on which security of the rollup relies, will be independently verified.

Recommendation. We recommend to add a provable init method to the outer contract, which sets the entire state and is called after deploying the rollup. The method should have a way of ensuring it can only be called once.

Adding an init method would make it easier to verify validity of the rollup’s state, with a script that loops through all transactions and checks that the verification key was not changed since initialization.

Furthermore, designing the init method would force the team to precisely nail down the requirements on initial state, making the init process easier to audit and better documented.

Regarding Rule_commit and its reliance on having the inner account in the left-most Merkle node: we recommend to simply add a check for the token id. This would eliminate one more complex assumption at no cost.

Client response. The Zeko team opted for a different way of documenting the intended initial state: They added an official spec for the initial state, that rollup implementations can be checked against. This avoids the overhead of adding an entire zkapp method that can only be used once, and mostly addresses the concern we raised regarding auditability.

Description. For its indexed Merkle tree, Zeko implements an $x>y$ assertion where x and y can range over the full field. This is achieved by representing x and y as bigints, and leveraging snarky’s custom foreign field gates. We found that the circuit is overconstrained and will not work for about half the (x, y) input pairs.

If x and y are bigints, we can check that $x>y$ by performing a bigint subtraction $w=x-y-1$ followed by a range-check on $w$. This is implemented in suc_then_dec by calling the ForeignFieldAdd gate twice: For $z=x-y$ and $w=z-1$.

In general, ForeignFieldAdd allows for overflow around a field, but here, the gate is instantiated with a modulus of 0 and a field_overflow of 0. For the sign, -1 is used to instantiate a subtraction. In this simplified form, the gate asserts two equations:

Here $x_2$ is the highest 88-bit limb (of three), $x_{01}=x_0+2^{88}{x}_1$ is a concatenation of the lower two limbs, and same for y and z. The carry $c$ is constrained by the gate to be either 0, 1 or -1.

In sub_then_dec, two addition gates are chained where the second subtracts the hard-coded bigint $1=(1,0,0)$. This implies the constraints

for some carries $c_0$ and $c_1$, where w is the final output.

Since the limbs of x, y and w are range-checked, these equations must hold over the integers and not just modulo the circuit field. Summing them as $e{q}_{01}+2^{176}e{q}_2$ cancels out the carries and proves that $x-y-1=w$, as desired. This way of using the gates is sound.

The only remaining challenge is witnessing the correct carries and outputs to make the constraints hold. This is where the implementation takes a short-cut and hard-codes both carries to 0. So the first equation simplifies to

This forces $x_{01}>y_{01}$ since $w_{01}\in [0,2^{176})$. However, even if $x>y$ we can not deduce any relationship between the lower two limbs, and in fact we expect $x_{01}\le y_{01}$ in about half of all cases. In other words, this circuit is overconstrained.

Impact. When properly tested before deployment, this bug would have surfaced quickly. If the rollup would be deployed as is, it would soon come to a halt because of a transaction that can’t be applied in-circuit. This is because sub_then_dec is called with hashes of account ids as input, which are essentially random field elements.

Recommendation. Implement the computation of at least one carry instead of hard-coding both to zero.

To see that one carry is enough, consider the extreme case where $x>y$, but $x_{01}=0$ and $y_{01}=2^{176}-1$. The first equation becomes

This is satisfiable with $c_0=-1$, so it’s fine to hard-code $c_1=0$.

In fact, this also means that the subtraction and decrement could be done in a single ForeignFieldAdd gate:

let* () =
  add_plonk_constraint
    (ForeignFieldAdd
        { left_input_lo = x0
        ; left_input_mi = x1
        ; left_input_hi = x2
        ; right_input_lo = Field.Var.add y0 dec
        ; right_input_mi = y1
        ; right_input_hi = y2
        ; sign = Field.of_int (-1)
        ; carry = carry
        ; field_overflow = Field.(constant typ zero)
        ; foreign_field_modulus0 = Field.zero
        ; foreign_field_modulus1 = Field.zero
        ; foreign_field_modulus2 = Field.zero
        } )

Client Response. The issue was fixed by computing and witnessing the carry, and collapsing the two foreign field gates into one as recommended.

Description. Zeko’s design features two bridge contracts: An “outer” bridge contract on the L1, and an “inner” bridge contract on the L2.

Furthermore, the outer contract can be in two different “states”: Enabled and disabled. When disabled, the contract should have a different verification key, with only a single method: the method to enable it.

In total, we end up with three separate sets of contract methods / verification keys:

• Outer contract, when enabled:
  • Rule_bridge_finalize_withdrawal
  • Rule_bridge_finalize_cancelled_deposit
  • Rule_bridge_disable
• Outer contract, when disabled:
  • Rule_bridge_enable
• Inner contract:
  • Rule_bridge_finalize_deposit
  • A currently missing rule to receive tokens, see finding

In the current bridge_rules.ml implementation, instead of compiling three separate rule sets, all rules are mixed together in a single verification key.

Impact. When deploying the mixed rule set both to the L1 and the L2, contract interactions outside the actual protocol design would be available to users.

In particular, a “disabled” outer contract with all the other rules still present would not actually be disabled.

Recommendation. Split up compilation into three different rule sets.

Client response. The issue was fixed in commit c291d4d.

Description. The function sub_then_dec performs subtraction $w=x-y-dec$ where $x$, $y$, and $w$ are big integers represented as three limbs and $dec$ is a small constant value.

But in the implementation, to compute the witness of $w$, a hard-coded constant value of $1$ is used instead of deriving it from the dec parameter, as seen in the following snippet.

let* (w0, w1), w2 =
    exists
        Typ.(F.typ * F.typ * F.typ)
        ~compute:
        (let- z0 in
            let- z1 in
            let- z2 in
            Zeko_as_prover.sub ~x0:z0 ~x1:z1 ~x2:z2 ~y0:Field.one
            ~y1:Field.zero ~y2:Field.zero
            |> As_prover.return )
    in

Impact. The circuit is incomplete if the value of $dec$ is not equal to one. In practice, an issue might not occur because in the audited code base, the function is always used with $dec=1$.

Recommendation. Update the parameters of (y0, y1, y2) to use the value from the dec for computing the witness of (w0, w1, w2).

The bridge contracts are designed to work for bridging either MINA or custom tokens. However, due to differences in how the zkapp protocol handles those kinds of tokens, the logic sometimes has to disambiguate between the two cases.

This is why the bridge rules depend on abstract configuration modules called Deposit_params and Withdrawal_params which have two instantiations, one for MINA and one for custom tokens: Deposit_params_base vs Deposit_params_custom, and same for withdrawals.

In bridge_rules.ml, two different functors called Make_mina and Make_custom are defined for the two cases. However, both functors accidentally use Deposit_params_base and Withdrawal_params_base, i.e. the native MINA configuration.

The Zeko team was already aware of this bug when we notified them.