Polygon zkEVM: Missing constraint in PIL leading to proving fake inclusion in the SMT

From WEB3 Vulnerapedia
Jump to navigation Jump to search

Polygon zkEVM: Missing constraint in PIL leading to proving fake inclusion in the SMT

Identified By: Hexens

Background

The Storage state machine uses SMT (Sparse Merkle Tree) and implements provable CRUD operations in conjunction with Storage ROM.

In order to prove the (Key, Value) inclusion in the SMT, the state machine represents the key as bit string. It traverses the tree from the root down to the leaf using LSBs (least significant bits) of the key: 0/1 values of the bit correspond to the left/right edge traversal.

As the tree is sparse, the leaf level is not necessarily equal to the key bits length, that means that as soon as the leaf is inserted into the tree, the remaining part of the key (rkey) is being encoded into the leaf value.

The inclusion check algorithm consists of two parts (reference link: https://wiki.polygon.technology/docs/zkEVM/zkProver/basic-smt-ops):

  1. Checking The Root - is done as a generic Merkel Tree root check by climbing from the leaf to the root using sibling hashes.
  2. Checking the Key: I. In order to check the key, the state machine prepends every next path bit to the remaining key (rkey), e.g. rkey||b1||b0 (for the leaf level = 2). II. By the end of the operation, which can be distinguished in Storage ROM by the LATCH_GET command, the iLatchGet is set to 1. III. A Permutation constraint is used in the Main SM to ensure that the key passed from the zkEVM ROM matches the one constructed in the step (I):
    sRD {
        SR0 + 2^32*SR1, SR2 + 2^32*SR3, SR4 + 2^32*SR5, SR6 + 2^32*SR7,
        sKey[0], sKey[1], sKey[2], sKey[3],
        op0, op1, op2, op3,
        op4, op5, op6, op7,
        incCounter
    } is
    Storage.iLatchGet {
        Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3,
        Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3,
        Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3,
        Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3,
        Storage.incCounter + 2
    };

Hence, the part (1) is used to prove that the Value exists in the SMT, and the part (2) is used to prove that the Value is actually binded with the correct Key.

The Vulnerability

The issue arise as the next-bit polynomial rkeyBit is missing a binary constraint in the Storage SM, as well as the fact that the Storage ROM, pretty naturally, does not assert that the next bit, that comes from a free input, cannot be of any other value than 0 or 1

storage_sm_get.zkasm: 

<; If next key bit is zero, then the sibling hash must be at the right (sibling's key bit is 1)
${GetNextKeyBit()} => RKEY_BIT
RKEY_BIT                        :JMPZ(Get_SiblingIsRight)

Nonetheless, it can not be abused straightforwardly; a number of limitations must be overcome. Due to the specifics of the key reconstruction algorithm and the fact that the value inclusion check in the part (1) needs to hold true simultaneously.

Limitations overview:

In the Storage SM, The key is broken down into four registers: rkey0,..,rkey3 and the path is constructed by cycling the consecutive bits of that registers: path = [rKey0_0, rKey1_0, rKey2_0, rKey3_0, rKey0_1, ... ] (reference link: https://wiki.polygon.technology/docs/zkEVM/zkProver/construct-key-path)

Thus, in order to reconstruct the key from the bits, the corresponding rkey polynomial needs to be prepended with that bit:

rkey[level % 4] ||= rkeyBit

It is important to mention that the key is actually the POSEIDON hash of the account address, storage slot and the query key.

In order to avoid modulo 4 operation, the Storage SM introduces LEVEL register, which also consists of 4 parts: level0,..level3 and the ROTATE_LEVEL opcode in the Storage ROM.

The LEVEL is firstly set to leaf_level % 4, and then ROTATE_LEVEL is used every time the prover needs to climb the tree:

storage-sm-get.zkasm: 

<; Update remaining key
                                :ROTATE_LEVEL
                                :CLIMB_RKEY

                                :JMP(Get_ClimbTree)

Level rotation(storage.pil): 

pol rotatedLevel0 = iRotateLevel*(level1-level0) + level0;
pol rotatedLevel1 = iRotateLevel*(level2-level1) + level1;
pol rotatedLevel2 = iRotateLevel*(level3-level2) + level2;
pol rotatedLevel3 = iRotateLevel*(level0-level3) + level3;

Finally, the rkey will be modified when using the CLIMB_RKEY opcode

storage.pil: 

pol climbedKey0 = (level0*(rkey0*2 + rkeyBit - rkey0) + rkey0);
pol climbedKey1 = (level1*(rkey1*2 + rkeyBit - rkey1) + rkey1);
pol climbedKey2 = (level2*(rkey2*2 + rkeyBit - rkey2) + rkey2);
pol climbedKey3 = (level3*(rkey3*2 + rkeyBit - rkey3) + rkey3);

In order to hold the above-mentioned permutation constraint all of the rkey0-3 registers must be modified by the end of the operation (when the LATCH_GET opcode is used). As well as the Storage ROM will be rearranging the left/right node hashes by matching the next-bit. Given the fact that one can only abuse the non-zero values of the next-bit, the limitations can be overcome by inserting arbitrary Value into the SMT with a Key that has 1111 as its LSBs.

Key = ***1111, this is needed to have the opportunity to change all 4 rkey registers. This means that the POSEIDON hash that is derived from the account address and the storage slot number (in addition to the storage query key), needs to have the least significant bits of its result registers hash0,..hash3 set as 1: 

hash0 = ***1
hash1 = ***1
hash2 = ***1
hash3 = ***1

As only 1 bit of every POSEIDON hash register is fixed, it is a trivial task to overcome the 4-bit entropy and find a storage slot (for any given account address) to meet the attack prerequisites. Another limitation is that the leaf we are inserting must have a level greater than 4, in the real-world scenario this is guaranteed to be the case (with a negligible negative outcome probability) as there will be millions of leafs inserted into the tree. Even if it's not the case the attacker will only need to precompute two storage slots and insert them both to guarantee the minimal level.

After inserting (KeyPrecomputed, ValueArbitrary) into the SMT using the opSSTORE procedure, and thus fulfilling the prerequisites the attacker can fake the binding of any key KeyToFake with the value ValueArbitrary, by setting the last 4 next-bit values from the free input to: 

rkeyBit[0] =  rkeyToFake[0] - rkey0*2
rkeyBit[1] =  rkeyToFake[1] - rkey1*2
rkeyBit[2] =  rkeyToFake[2] - rkey2*2
rkeyBit[3] =  rkeyToFake[3] - rkey3*2

As the Storage ROM uses JMPZ to distinguish the climb path, despite being greater than 1 the rkeyBit will be treated the same way as if it was set to 1, and the root check (Value inclusion) will successfully be bypassed.

The main impact that will favor the attacker will be to fake the inclusion of (KeyAttackerBalance, ArbitraryAmount) in the SMT.

The Fix

The Fix of this issue is to add the missing binary constraint.

References

Hexens Audit Report

Fix Commit

https://github.com/0xPARC/zk-bug-tracker#hexens-polygonzkevm-1

Related Vulnerabilities

Under-Constrained Circuits vulnerability

Retrieved from "https://wiki.r.security/w/index.php?title=Polygon_zkEVM:_Missing_constraint_in_PIL_leading_to_proving_fake_inclusion_in_the_SMT&oldid=1080"