Polygon zkEVM Hexens审计报告解读
1. 引言
Hexens在2022年12月17日 至 2023年2月27日 期间，对Polygon zkEVM项目进行了审计，并发布了审计报告：
Hexens主要审计的代码库有：
- https://github.com/0xPolygonHermez/zkevm-contracts
- https://github.com/0xPolygonHermez/zkevm-proverjs
- https://github.com/0xPolygonHermez/zkevm-storage-rom
- https://github.com/0xPolygonHermez/zkevm-rom
在审计过程中，Hexens共发现了：
- 9个脆弱点（vulnerabilities）
- 7个（EVM与zkEVM等）不一致点
这16个问题在Polygon zkEVM Audit-Upgraded Testnet 中得到了修复，并于2023年3月初上线。
1.1 Polygon zkEVM
Polygon zkEVM为首个EVM-equivalent零知识L2扩容方案，现有的智能合约、开发者工具和钱包都可无缝迁移使用。
Polygon zkEVM利用零知识证明技术来降低交易手续费，并增加交易突突了，同时集成了以太坊的安全性。
Polygon zkEVM（L2）网络中的交易会被编译为batches，这些batches会sequence到以太坊（L1）智能合约中，当batches对应的state transitions被证明且在以太坊上验证通过之后，相应的状态将变为trusted state。
Polygon zkEVM有多个操作层：
- 1）网络层：为Sequencer和Aggregator所在运行层。
- 2）ROM层：Polygon zkEVM采用新的名为zkASM的语言来实现的EVM，使得EVM state transactions provable。
- 3）硬件层：Polygon zkEVM采用新的名为PIL的语言来创建polynomial identities和polynomial constraints，以确保zkASM ROM执行的完备性和可靠性。
- 4）L1以太坊智能合约：在网络之间进行资产bridge，并实现了PoE（Proof of Efficiency）共识，PoE共识合约可确保batches的正确state transition。
2. bridge合约 严重漏洞
可借助ERC-777 token的扩展特性，对bridge合约发起重入攻击。
/**
* @notice Deposit add a new leaf to the merkle tree
* @param destinationNetwork Network destination
* @param destinationAddress Address destination
* @param amount Amount of tokens
* @param token Token address, 0 address is reserved for ether
* @param forceUpdateGlobalExitRoot Indicates if the new global exit root is updated or not
* @param permitData Raw data of the call `permit` of the token
*/
function bridgeAsset(
uint32 destinationNetwork,
address destinationAddress,
uint256 amount,
address token,
bool forceUpdateGlobalExitRoot,
bytes calldata permitData
) public payable virtual ifNotEmergencyState nonReentrant {
if (
destinationNetwork == networkID ||
destinationNetwork >= _CURRENT_SUPPORTED_NETWORKS
) {
revert DestinationNetworkInvalid();
}
address originTokenAddress;
uint32 originNetwork;
bytes memory metadata;
uint256 leafAmount = amount;
if (token == address(0)) {
// Ether transfer
if (msg.value != amount) {
revert AmountDoesNotMatchMsgValue();
}
// Ether is treated as ether from mainnet
originNetwork = _MAINNET_NETWORK_ID;
} else { //////#####关键点########
//关键点1：Ensure no native asset value is sent in bridging erc20
//等价为： require(msg.value == 0, "PolygonZkEVMBridge::bridgeAsset: Expected zero native asset value when bridging ERC20 tokens");
// Check msg.value is 0 if tokens are bridged
if (msg.value != 0) {
revert MsgValueNotZero();
}
TokenInformation memory tokenInfo = wrappedTokenToTokenInfo[token];
if (tokenInfo.originTokenAddress != address(0)) {
// The token is a wrapped token from another network
// Burn tokens
TokenWrapped(token).burn(msg.sender, amount);
originTokenAddress = tokenInfo.originTokenAddress;
originNetwork = tokenInfo.originNetwork;
} else {//////#####关键点########
// Use permit if any
if (permitData.length != 0) {
_permit(token, amount, permitData);
}
// In order to support fee tokens check the amount received, not the transferred
uint256 balanceBefore = IERC20Upgradeable(token).balanceOf(
address(this)
);
IERC20Upgradeable(token).safeTransferFrom(
msg.sender,
address(this),
amount
);
uint256 balanceAfter = IERC20Upgradeable(token).balanceOf(
address(this)
);
// Override leafAmount with the received amount
leafAmount = balanceAfter - balanceBefore;
originTokenAddress = token;
originNetwork = networkID;
// Encode metadata
metadata = abi.encode(
_safeName(token),
_safeSymbol(token),
_safeDecimals(token)
);
}
}
emit BridgeEvent(
_LEAF_TYPE_ASSET,
originNetwork,
originTokenAddress,
destinationNetwork,
destinationAddress,
leafAmount,
metadata,
uint32(depositCount)
);
_deposit(
getLeafValue(
_LEAF_TYPE_ASSET,
originNetwork,
originTokenAddress,
destinationNetwork,
destinationAddress,
leafAmount,
keccak256(metadata)
)
);
// Update the new root to the global exit root manager if set by the user
if (forceUpdateGlobalExitRoot) {
_updateGlobalExitRoot();
}
}解决方案为：【详细参看https://github.com/0xPolygonHermez/zkevm-contracts/commit/cd69081aa4e827aa85604df4e6c2734dabe61025】
- 1）在
bridgeAsset函数中增加nonReentrantmodifier：
function bridgeAsset(
address token,
uint32 destinationNetwork,
address destinationAddress,
uint256 amount,
bytes calldata permitData
// ) public payable virtual ifNotEmergencyState {
) public payable virtual ifNotEmergencyState nonReentrant {
...........
}
/**
* @dev Prevents a contract from calling itself, directly or indirectly.
* Calling a `nonReentrant` function from another `nonReentrant`
* function is not supported. It is possible to prevent this from happening
* by making the `nonReentrant` function external, and making it call a
* `private` function that does the actual work.
*/
modifier nonReentrant() {
_nonReentrantBefore();
_;
_nonReentrantAfter();
}- 2）
_deposit()函数会调用DepositContrace，设置DepositContract也是防重入的：【为ReentrancyGuardUpgradeable】
//import "@openzeppelin/contracts-upgradeable/proxy/utils/Initializable.sol";
import "@openzeppelin/contracts-upgradeable/security/ReentrancyGuardUpgradeable.sol";
/**
* This contract will be used as a helper for all the sparse merkle tree related functions
* Based on the implementation of the deposit eth2.0 contract https://github.com/ethereum/consensus-specs/blob/dev/solidity_deposit_contract/deposit_contract.sol
*/
//contract DepositContract is Initializable {
contract DepositContract is ReentrancyGuardUpgradeable {- 3）PolygonZkEVMBridge合约的
initialize()函数中增加__ReentrancyGuard_init();：
/**
* @param _networkID networkID
* @param _globalExitRootManager global exit root manager address
* @param _polygonZkEVMaddress polygonZkEVM address
* @notice The value of `_polygonZkEVMaddress` on the L2 deployment of the contract will be address(0), so
* emergency state is not possible for the L2 deployment of the bridge, intentionally
*/
function initialize(
uint32 _networkID,
IBasePolygonZkEVMGlobalExitRoot _globalExitRootManager,
address _polygonZkEVMaddress
) external virtual initializer {
networkID = _networkID;
globalExitRootManager = _globalExitRootManager;
polygonZkEVMaddress = _polygonZkEVMaddress;
// initialize OZ libraries
__ReentrancyGuard_init();
}3. Storage状态机缺少binary约束 严重漏洞
前序博客：
Polygon zkEVM的Storage状态机采用SMT（Sparse Merkle Tree），与Storage ROM一起，实现了可证明的CURD（增删改查）操作。
为证明某(Key, Value)在SMT中（inclusion proof），在Storage状态机中，将Key表示为bit string。其traverse the tree from the root down to the leaf using LSBs（least significant bits）of the key：bit的0/1值对应左/右侧。
由于是稀疏Merkle树，leaf level没必要等于key bits length，这即意味着，一旦leaf插入到树中，该key的剩余部分(rkey)即编码仅了leaf value中——
。
在inclusion proof验证时，需：
- 1）Checking the Root：与常规的Merkle tree root check一样。【用于证明Value存在于SMT中】
- 2）Checking the Key：【用于证明该Value与正确的Key绑定】
- 2.1）为check key，状态机需将next path-bits预追加到remaining key中，如，对于2层leaf level，有：rkey||b1||b0。
- 2.2）操作结束的标签由Storage ROM中的LATCH_GET command标记，iLatchGet selector会被设置为1.
- 2.3）主状态机 会使用Permutation check来检查由zkEVM ROM传来的key 与 2.1）中构建的key 匹配：
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 };
在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)问题就在于，next-bit多项式rkeyBit在Storage SM和Storage ROM中缺少binary约束，即约束其值必须为0或者是1。相应的解决方案为：【详细见：add binary constraint in storage.pil commits。】
- 1）对commit多项式rkeyBit进行binary约束：
rkeyBit' = setRkeyBit*(op0-rkeyBit) + rkeyBit;
rkeyBit * (1 - rkeyBit) = 0; //进行binary约束
level0' = setLevel*(op0-level0) + iRotateLevel*(rotatedLevel0-level0) + level0;
level1' = setLevel*(op1-level1) + iRotateLevel*(rotatedLevel1-level1) + level1;原因在于： Storage状态机中的key被分解为4个寄存器来表示rKey0,,,rKey3，path依次由这4个寄存器的bits组成： path=[rKey0_0, rKey1_0, rKey2_0, rKey3_0, rKey0_1,...]
根据path-bits重构key，如逐level追加bit： rKey[level % 4] ||= rkeyBit
为避免做modulo 4运算（因将key以4个元素来表示），引入了 1个寄存器 和 1个操作：
- 在Storage SM中引入
LEVEL寄存器：由4个bits组成，其中3个bit为0，1个bit为1。LEVEL寄存器的初始值为
- 在Storage ROM中引入
ROTATE_LEVELopcode：每次对LEVEL寄存器进行左移1位的rotation。【当每次Prover需要climb the tree时，会使用ROTATE_LEVELopcode。】
在storage_sm_get.zkasm中有：
; Update remaining key
:ROTATE_LEVEL
:CLIMB_RKEY
:JMP(Get_ClimbTree)对应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;当使用CLIMB_RKEY opcode时，rkey将被修改，对应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);为证明之前提及的Permutation约束成立，在最后（运行LATCH_GET opcode时）需对rkey0-3寄存器进行修改。与此同时，Storage ROM会对左右节点哈希值进行rearrange以匹配the next-bit。因此，仅当next-bit为非零值时，才可能有abuse的情况。因此，可向SMT插入Key以1111结尾的任意Value，可突破该限制：
Key=****1111，有机会可改变所有4个rkey寄存器。
这就意味着，派生自account address、storage slot 以及 storage query key的 POSEIDON哈希结果寄存器hash0,…,hash3的最低有效位均为1：
hash0 = ***1
hash1 = ***1
hash2 = ***1
hash3 = ***1由于每个POSEIDON哈希寄存器仅1个bit是固定的，此为trivial task来克服该4-bit entropy，对于某特定account address，以找到某storage slot使得可满足相应的攻击前提条件。
另一个限制在于：
- 待插入的leaf所具有的level应大于4。在现实场景中，由于有数百万的leaf会插入，突破该限制的情况可忽略。
即使除外情况下，攻击者仅需预计算出2个storage slot，遵循相同的规则，将二者插入以满足最低level。使用opSSTORE流程将(KeyPrecomputed, ValueArbitrary)插入到SMT中之后，满足了攻击前提条件之后，攻击者可伪造任意的key KeyToFake with value ValueArbitrary，只需要求free input的last 4 next-bit满足：
rkeyBit[0] = rkeyToFake[0] - rkey0*2
rkeyBit[1] = rkeyToFake[1] - rkey1*2
rkeyBit[2] = rkeyToFake[2] - rkey2*2
rkeyBit[3] = rkeyToFake[3] - rkey3*2即可。由于Storage ROM中仅需使用JMPZ来区分climb path，即使rkeyBit值大于1，其效果也与 其值为1 等价，且 root check（Value inclusion）将验证通过。
因此，本漏洞的主要影响在于：攻击者可向SMT中伪造插入(KeyAttackerBalance, ArbitraryAmount)。
4. identity预编译合约分配CTX 严重漏洞
zkevm-rom中process-tx.zkasm和precompiled/identity.zkasm中，错误的分配了CTX，使得可向sequencer balance中增加任意数量的Ether。
解决方案为：修改precompiled/identity.zkasm代码，在跳转到handleGas label之前，存下originCTX。【详细参看：https://github.com/0xPolygonHermez/zkevm-rom/commit/d1a2936649d82d912bff51315db397be2f832bc2 commits。】
IDENTITYreturn:
; handle CTX
$ => A :MLOAD(originCTX), JMPZ(handleGas)
; set retDataCTX
$ => B :MLOAD(currentCTX)
A => CTX
B :MSTORE(retDataCTX)
B => CTXPolygon zkEVM ROM架构中使用Contexts（CTX）来划分和模拟一个交易内调用上下文的虚拟地址到物理地址之间的转换。CTX地址空间用于确定在调用上下文之间变化的动态内存空间，以及堆栈和CTX变量（如msg.sender、msg.value、active storage account等）。上下文切换是使用辅助变量完成的，如originalCTX，它指的是创建当前上下文currentCTX的原始CTX。有一个特殊的CTX（0）用于存储全局变量，如tx.origin或旧状态根，batch交易开始的第一个上下文是CTX（1），并且随着新调用、上下文切换或交易的处理而递增。
本漏洞存在与“identity”(0x4)预编译合约中。此时未设置originCTX，即意味着由EOA直接调用预编译合约，而不是在合约内部进行调用。该预编译合约将消耗intrinsic gas并end transaction execution。 尽管在”ecrecover”(0x1)预编译合约中的上下文切换是正确的，但是“identity”(0x4)预编译合约的上下文切换存在问题。
若交易直接调用“identity”(0x4)预编译合约，其使用originCTX变量，并检查其是否为0：
$ => CTX :MLOAD(originCTX), JMPZ(handleGas)尽管其将originCTX立即加载到了CTX寄存器中，所有的内存操作将基于CTX[0]进行。
但是，main.pil中，GLOBAL和CTX上下文之间的切换是通过useCTX来实现的：
/*
ctxBase = CTX * 0x040000 ctxSize = 256K addresses * 32 bytes (256 bits) = 8MiB
Memory Region Size isMem isStack Content
ctxBase + [0x000000 - 0x00FFFF] 2MiB 0 0 Context specific variables
ctxBase + [0x010000 - 0x000000] 2MiB 0 1 EVM Stack
ctxBase + [0x020000 - 0x03FFFF] 4MiB 1 0 EVM Memory
*/
pol addrRel = ind*E0 + indRR*RR + offset;
pol addr = useCTX*CTX*2**18 + isStack*2**16 + isStack*SP + isMem*2**17+ addrRel;当useCTX=0，对应为GLOBAL上下文；当useCTX=1，对应为CTX上下文。当CTX寄存器值为0时，GLOBAL和CTX上下文所计算的最终地址是相同的。 由于这些变量由offset寻址，ROM的全局变量由合适的CTX与相同的offset共同引用。
如果GLOBAL和CTX的offset变量发生了碰撞，则可有如下攻击：
- 1）EOA用户创建一笔目标地址为“identity”(0x4)预编译合约 的交易。
- 2）当执行到
$ => CTX :MLOAD(originCTX), JMPZ(handleGas)时，由于CTX被设置为0，将调整到handleGas label执行。 handleGas 将检查refund（一个重要的细节在于：在当前的VAR配置中，gasRefund变量与当前值为0的nextHashPId发生了碰撞，但是，若与其他具有更大绝对值的VAR变量碰撞的话，则caller有机会为自己“print money out of thin air”），当对sender refund之后，接下来回将所消耗的gas归到sequencer地址中，在process-tx.zkasm中有：
;; Send gas spent to sequencer
sendGasSeq:
$ => A :MLOAD(txGasLimit)
A - GAS => A
$ => B :MLOAD(txGasPrice)
; Mul operation with Arith
A :MSTORE(arithA)
B :MSTORE(arithB), CALL(mulARITH)
$ => D :MLOAD(arithRes1) ; value to pay the sequencer in D由于VAR CTX txGasLimit对应VAR GLOBAL oldStateRoot，oldStateRoot为状态树的哈希值，具有非常大的绝对值，即MLOAD(txGasLimit)将返回oldStateRoot value instead。将gasPrice设置为1(或任意不会引起乘积溢出的小值)，Sequencer可获得非常大的balance。
该攻击要求及概率为：
- 任意用户sequence时，都可给自己credit非常大的ether balance。 攻击的最佳方式为：
- force a batch in L1 PolygonZkEVM contract
因在当前配置下，trusted sequencer会忽略forced batches，会将其存储在独立的数据库表中state.forced_batch。当sequencer调用getSequencesToSend()查询pending batches时，其仅查询state.batch表。这就意味着攻击者将force a batch，并等待超时和sequence该force batch，可设置sequencer为任意地址。当前配置下，任何人都有机会发起该force batch攻击，等待超时然后获得大额的ether balance。若在同一batch中混合一些“dummy”交易并增加bridgeAsset()调用，当该batch被验证通过之后，攻击者可获得具有任意ether amount的deposit leaf，从而可取光bridge中的所有ether。
5. 中间commit多项式isNeg缺少binary约束 严重漏洞
中间commit多项式isNeg取值应仅能为0或者1，缺少binary约束。否则会引起execution flow hijack，可能可跳转到ROM中的任意地址。影响之一是为任意的caller任意增加balance。 相应的解决方案为：【详细见：add missing binary constraints commits。】
- 1）对引入的中间commit多项式isNeg进行binary约束：
/////// isNeg
pol commit lJmpnCondValue;
pol jmpnCondValue = JMPN*(isNeg*2**32 + op0);
isNeg * (1 - isNeg) = 0; //增加binary约束在utils.zkasm的computeGasSendCall中：
; C = [c7, c6, ..., c0]
; JMPN instruction assures c0 is within the range [0, 2**32 - 1]
${GAS >> 6} => C :JMPN(failAssert)
${GAS & 0x3f} => D
; since D is assured to be less than 0x40
; it is enforced that [c7, c6, ..., c1] are 0 since there is no value multiplied by 64
; that equals the field
; Since e0 is assured to be less than 32 bits, c0 * 64 + d0 could not overflow the field
C * 64 + D :ASSERT使用了free input calls来做计算，为保证free input的有效性，使用了JMPN。JMPN将验证寄存器C中的free input是否在
范围内。同时，在后续的断言（C * 64 + D :ASSERT）中有安全假设来确保该寄存器未溢出。 在main.pil中，JMPN约束为：
pol jmpnCondValue = JMPN*(isNeg*2**32 + op0);通过检查jmpnCondValue为32-bit number，即可确保op0在
范围内，从而避免溢出。jump destination以及zkPC约束中，最终都基于了isNeg：
pol doJMP = JMPN*isNeg + JMP + JMPC*carry + JMPZ*op0IsZero + return + call;
pol elseJMP = JMPN*(1-isNeg) + JMPC*(1-carry) + JMPZ*(1-op0IsZero);
.........
// ROM/Zkasm constraint: useJmpAddr * return = 0
pol finalJmpAddr = useJmpAddr * (jmpAddr - addr ) + return * (RR - addr) + addr;
pol nextNoJmpZkPC = zkPC + 1 - ((1-RCXIsZero)*repeat);
pol finalElseAddr = useElseAddr * (elseAddr - nextNoJmpZkPC) + nextNoJmpZkPC;
// if elseAddr wasn't specified on zkasm, compiler put current address + 1
zkPC' = doJMP * (finalJmpAddr - nextNoJmpZkPC) + elseJMP * (finalElseAddr - nextNoJmpZkPC) + nextNoJmpZkPC;若缺少对isNeg为0或1的binary约束，则对应在utils.zkasm的computeGasSendCall流程中，有：
finalElseAddr = nextNoJmpZkPC
doJMP = isNeg
elseJMP = (1-isNeg)相应的zkPC约束也reduce为：
zkPC' = isNeg * (finalJmpAddr - nextNoJmpZkPC) + nextNoJmpZkPC其中finalJmpAddr和nextNoJmpZkPC均为在ROM程序编译阶段的已知值。 为jump到任意zkPC，攻击者需计算相应的isNeg和op0值，具体的计算公式为：
此时攻击者已具有可跳转到任意address的primitive，下一步就是找到合适的gadget来jump to，基本的原则为：
- 不会corrupt或revert zkEVM execution
- 产生对攻击者有利的影响
跳转实现的方式之一是：
- 使用
CALLopcode作为攻击起始操作，调用computeGasSendCall，然后跳转到refundGaslabel中有：
$ => A :MLOAD(txSrcOriginAddr)
0 => B,C ; balance key smt
$ => SR :SSTORE会将D寄存器中的值 作为 txSrcOriginAddr的balance，并完成交易的执行。为滥用SSTORE所存储的值，攻击者需向D寄存器中设置huge value，为此，可使用DELEGATECALL opcode，因实际实现时，DELEGATECALL opcode会在调用computeGasSendCall之前设置D寄存器：
D :MSTORE(storageAddr)
..........
; compute gas send in call
E :MSTORE(retCallLength), CALL(computeGasSendCall); in: [gasCall: gas sent to call] out: [A: min( requested_gas , all_but_one_64th(63/64))]此时，D寄存器中值为storageAddr，具有很大的绝对值。
完成该攻击的额外步骤有：
- 所部署的合约需提供 可发起delegatecall()到任意地址 的函数或fallback。
- 交易应该在gasPrice设置为0的情况下发起，以避免在将其发送到sequencer时gas溢出，而且这将有利于攻击者证明所发起的batch。
- 应预计算出gasLimit，使得交易执行最终的gas为0，原因同上。
6. MAXMEM寄存器 高危漏洞
在zkEVM ROM中，MAXMEM寄存器用于设置memory的最大偏移量，且仅在execution trace的第一步设置为0。 当合约调用MLOAD/MSTORE EVM-opcode时，当referenced memory具有比当前所设置的更高的相对地址时，MAXMEM寄存器值将发生改变：
pol addrRel = ind*E0 + indRR*RR + offset;
pol maxMemRel = isMem * addrRel;
pol maxMemCalculated = isMaxMem*(addrRel - MAXMEM) + MAXMEM;
MAXMEM' = setMAXMEM * (op0 - maxMemCalculated) + maxMemCalculated;MAXMEM当前值与relative address之间的“difference”存在plookup check：
/////// MAXMEM intermediary vals New State
pol diffMem = isMaxMem* ( (maxMemRel - MAXMEM) -
(MAXMEM - maxMemRel) ) +
(MAXMEM - maxMemRel);
isMaxMem * (1 - isMaxMem) = 0;
diffMem in Global.BYTE2;plookup check会高效检查该difference为非负值；isMaxMem设置正确；约束difference为：|maxMemRel — MAXMEM| <
。
另一方面，在utils.zkasm的saveMem流程中，会对relative memory offset进行检查：
$ => B :MLOAD(lastMemOffset)
; If the binary has a carry, means the mem expansion is very big. We can jump to oog directly
; offset + length in B
$ => B :ADD, JMPC(outOfGas)
; check new memory length is lower than 2**22 - 31 - 1 (max supported memory expansion for %TX_GAS_LIMIT of gas)
%MAX_MEM_EXPANSION_BYTES => A
$ :LT,JMPC(outOfGas)尽管CONST %MAX_MEM_EXPANSION_BYTES = 0x3fffe0为
，实际ROM使用的offset为 offset/32，即意味着合约给的最大memory offset为
。 由于diffMem的取值范围为Global.BYTE2（即
），攻击者将需要2次MLOAD或MSTORE操作来让MAXMEM的值超过BYTE2范围，如：
。 由于MAXMEM永远不会reset，且diffMem in Global.BYTE2成立，不存在GLOBAL/CTX或stack变量memory操作的selector，由于isMem将为0，因此maxMemRel也将为0. 即意味着diffMem：
pol diffMem = isMaxMem* ( (maxMemRel - MAXMEM) -
(MAXMEM - maxMemRel) ) +
(MAXMEM - maxMemRel);要么等于maxMemRel-MAXMEM——为一个负数，或者MAXMEM-maxMemRel——值
，因此后续的plookup with BYTE2将无法满足。
这就给了非法用户可乘之机，其可向trusted sequencer发起一笔交易，或者自己force一笔交易，一旦该batch被sequenced，则后续无法证明the next state transition。
补救措施为：将diffMem plookup改为BITS17，或者将MAX_MEM_EXPANSION_BYTES压缩为
，使得MAXMEM的最大值为
详细解决方案见：
- remove MAXMEM register commits
7. ecrecover zkasm中不正确的limit check 中危漏洞
zkEVM中以zkASM语言实现了ecrecover函数，其必须可检查出ECDSA签名的延展性。当在验证交易签名，以及在调用ecrecover预编译合约时，均需要做ECDSA签名延展性检查。
为让ECDSA签名不可延展，S值应不大于Fp/2，即满足S<=Fp/2，而Fp/2的实际值为57896044618658097711785492504343953926418782139537452191302581570759080747168。
在Go-ethereum中也有相应的check实现：https://github.com/ethereum/go-ethereum/blob/f53ff0ff4a68ffc56004ab1d5cc244bcb64d3277/crypto/crypto.go#L268-L270。而当前ecrecover中实现的check为基于Fp/2+1而不是Fp/2，这意味着S的合法取值包含了Fp/2+1，这种差异可能被滥用来为 与EVM不一致的交易 生成proof。
ecrecover_tx:
%FNEC_DIV_TWO :MSTORE(ecrecover_s_upperlimit)
..........
; s in [1, ecrecover_s_upperlimit]
$ => A :MLOAD(ecrecover_s_upperlimit)
$ => B :MLOAD(ecrecover_s)
$ :LT,JMPC(ecrecover_s_is_too_big)详细解决方案见：
//CONSTL %FNEC_DIV_TWO = 57896044618658097711785492504343953926418782139537452191302581570759080747169n //错误的值，应为57896044618658097711785492504343953926418782139537452191302581570759080747168
CONSTL %FNEC_DIV_TWO = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF5D576E7357A4501DDFE92F46681B20A0n8. zkEVM与EVM交易RLP解码不一致 低危漏洞
在https://ethereum.org/en/developers/docs/data-structures-and-encoding/rlp/#definition中指出，当将把交易中的data字段编译为RLP string时，具有short size（0–55 bytes）和long size（55+ bytes） 2种情况：
在zkEVM中，对应的交易RLP解码见load-tx-rlp.zkasm中，其中的dataREAD label负责解码交易中的DATA字段。
问题在于，在构建RLP交易时，可将（小于55字节的）short data字段 编码为 long string格式（如0xb801AA = [“AA“]，明明为1 byte string，但将其编码为long string格式），在EVM中做了相应的检查，以避免类似的情况：
case b < 0xC0:
// If a string is more than 55 bytes long, the RLP encoding consists of a
// single byte with value 0xB7 plus the length of the length of the
// string in binary form, followed by the length of the string, followed
// by the string. For example, a length-1024 string would be encoded as
// 0xB90400 followed by the string. The range of the first byte is thus
// [0xB8, 0xBF].
size, err = s.readUint(b - 0xB7)
if err == nil && size < 56 {
err = ErrCanonSize
}
return String, size, err与此同时zkEVM-node也集成了该lib，也做了相应的价差。但是，在zkEVM的ROM RLP解码过程中，并没有做相应的检查（包括short/long strings和short/long lists这2种情况）。
造成的影响为：
- 编码不匹配的“poison”交易会阻塞和破坏batch sequencing机制。
具体的攻击步骤为：
- 1）攻击者force一个错误RLP编码的batch
- 2）trusted sequencer要么sequence该batch，要么忽略该batch，当超时之后
- 3）trusted sequencer 或 攻击者 可sequence该forced batch
- 4）攻击者验证该batch，由于其对zkEVM ROM是fully provable的，并借助该poison交易来从bridge中claim或use assets。
- 5）zkEVM网络会halt，因为其无法同步该force batch，且网络将保持desynced状态。
- 6）对该情况的可能应对策略为：
- 6.1）修复zkEVM ROM中RLP解码，并通过以更老的state root重新部署PoE合约 来 回滚L1状态。
- 6.2）修改zkEVM-node中的RLP解码以匹配这种错误的情况，对整个L2网络升级以应对错误RLP交易情况。
最可行的解决方案为6.1，而不是像6.2那样为解决一个bug而引入新bug。不过，回滚操作可能对攻击者有利，其可能会实现双花。
详细解决方案见：
- no leading zeros and it is encoded in its shortest form commits中的checkNonLeadingZeros
- RLP checks & clean code commits 中的 checkShortRLP 和 checkLongRLP
9. EVM与zkEVM中的gasLimit和ChainID max size不一致 低危漏洞
Go-ethereum中有：
- https://github.com/ethereum/go-ethereum/blob/79a478bb6176425c2400e949890e668a3d9a3d05/core/types/tx_legacy.go#L29 设置的gas limit为64bit，而Polygon zkEVM中在RLP解析时，设置的gas limit为256bit，二者不一致：
// LegacyTx is the transaction data of regular Ethereum transactions.
type LegacyTx struct {
Nonce uint64 // nonce of sender account
GasPrice *big.Int // wei per gas
Gas uint64 // gas limit 为64bit
To *common.Address `rlp:"nil"` // nil means contract creation
Value *big.Int // wei amount
Data []byte // contract invocation input data
V, R, S *big.Int // signature values
}- 2）https://github.com/ethereum/go-ethereum/blob/01808421e20ba9d19c029b64fcda841df77c9aff/core/types/transaction.go#L75中chainID为big.Int类型，为256bit，但Polygon zkEVM中在RLP解析时，设置的chainID为64bit，二者不一致：
type TxData interface {
txType() byte // returns the type ID
copy() TxData // creates a deep copy and initializes all fields
chainID() *big.Int //为256bit
accessList() AccessList
........
}相应解决方案见： * 1）RLP checks & clean code commits：
;; Read RLP 'gas limit'
// ; 256 bits max
; 64 bits max //与EVM匹配，为64 bit
gasLimitREAD:
1 => D :CALL(addHashTx)
:CALL(addBatchHashData)
A - 0x80 :JMPN(endGasLimit)
A - 0x81 :JMPN(gasLimit0)
// A - 0xa1 :JMPN(shortGasLimit, invalidTxRLP) //32 bytes对应为256 bits
A - 0x89 :JMPN(shortGasLimit, invalidTxRLP) //8 bytes对应64 bits- 2）Polygon zkEVM中的chainID仍保持为64bit，讨论见：https://github.com/0xPolygonHermez/zkevm-rom/issues/274：
;; Read RLP 'chainId'
; 64 bits max
chainREAD:
1 => D :CALL(addHashTx)
:CALL(addBatchHashData)
A - 0x80 :JMPN(endChainId)
A - 0x81 :JMPN(chainId0)
A - 0x89 :JMPN(shortChainId, invalidTxRLP) // chainID保持为64bit不变原因在于：
- 2.1）Polygon zkEVM
chainID的设置源自PolygonZkEVM.sol合约，在该合约内，chainID为uint64类型，为64bit，ROM中的设置应与合约中的一致：
constructor(
IPolygonZkEVMGlobalExitRoot _globalExitRootManager,
IERC20Upgradeable _matic,
IVerifierRollup _rollupVerifier,
IPolygonZkEVMBridge _bridgeAddress,
uint64 _chainID, //为 64 bit chainID
uint64 _forkID
)- 2.2）
chainID为SNARK input的一部分，更短的input byte size，意味着电路中更少的约束。 - 2.3）在ROM刚刚开始执行时，
chainID被映射到了GAS寄存器中，每个GAS寄存器对应一个field element，对应约64bit。main.pil中有：
public chainId = GAS(0);
Global.L1 * (GAS - :chainId) = 0;- 2.4）
chainIDmaximum size不匹配，可能的影响是：以正确的chainID来创建交易，当将该chainID编码为更大的unit，使得zkEVM节点和EVM（RLP lib）均认可该交易，但无法证明包含了该交易的batch。因为zkASM EVM将在load-rlp阶段就失败，从而会忽略该batch，借此可向sequencer发送这样的免费垃圾交易，从而影响网络可用性。对此的解决方案为，约束chainID仅能以最短有效RLP方式表示，即增加了checkShortRLP和checkNonLeadingZeros检查：
shortChainId:
A - 0x80 => D :CALL(addHashTx)
:CALL(addBatchHashData)
:CALL(checkShortRLP) //增加检查
:CALL(checkNonLeadingZeros) //增加检查
;; Check short value is over 127. Error RLP: single byte < 0x80 are not prefixed
checkShortRLP:
D - 1 :JMPNZ(skipCheckShort)
A - %MIN_VALUE_SHORT :JMPN(invalidTxRLP)
skipCheckShort:
:RETURN
;; Check non-negative integer RLP representation has no leading zeros and it is encoded in its shortest form
VAR GLOBAL tmpVarAcheckNonLeadingZeros
VAR GLOBAL tmpVarZkPCcheckNonLeadingZeros
checkNonLeadingZeros:
RR :MSTORE(tmpVarZkPCcheckNonLeadingZeros)
A :MSTORE(tmpVarAcheckNonLeadingZeros)
; set value to B and get its
A => B :CALL(getLenBytes) ; in: [B: number] out: [A: byte length of B]
; check (bytes length - encoded length) are not equal
D - A :JMPNZ(invalidTxRLP)
$ => RR :MLOAD(tmpVarZkPCcheckNonLeadingZeros)
$ => A :MLOAD(tmpVarAcheckNonLeadingZeros), RETURN10. opcodes/block.zkasm中的有条件跳转 低危漏洞
在分析zkEVM ROM opcodes 与 状态机中相应PIL表示时，否限某些条件跳转的operational register size存在差异：
- JMPN（如为负数即跳转）：
main.pil中有：
pol jmpnCondValue = JMPN*(isNeg*2**32 + op0);- JMPZ（如为零值即跳转）和JMPNZ（如为非零值即跳转）：
main.pil中有：
/// op0 check zero
pol commit op0Inv;
pol op0IsZero = 1 - op0*op0Inv;
op0IsZero*op0 = 0;
...........
pol doJMP = JMPN*isNeg + JMP + JMPC*carry + JMPZ*op0IsZero + return + call;由此可知，JMPN/Z/NZ opcodes仅考虑op0寄存器。而JMPC/JMPNC等条件跳转，需使用binary状态机的carry latch，基于256-bit values进行操作。 这些类型的跳转仅针对具有8-slot（如A,B,C,…）寄存器的lower part。如，若
，即使其它7个slot均为非零值，因
，也会发生相应的调整。因为，这对应为
，在跳转时，仅需对
进行判断。
而在整个zkEVM ROM中调用JMPN/JMPZ/JMPNZ时，使用的为8-slot寄存器，但未对其它7个slot中的值做任何约束（如要求寄存器值小于
）。
如在opcodes/block.zkasm的opBLOCKHASH中，有：
opBLOCKHASH:
.....
; Get last tx count
$ => B :MLOAD(txCount) ; 此时B寄存器的值可能会大于$2^{32}$
B + 1 => B
$ => A :MLOAD(SP) ; [blockNumber => A]
; Check batch block is lt current block number, else return 0
B - A - 1 :JMPN(opBLOCKHASHzero) ;即要求A<B-1，BLOCKHASH(oldBlockNumber)，其中oldBlockNumber小于当前区块号。当txCount值大于
时，可能会存在对JMPN的不正确触发。这种情况是可能发生的，因为zkEVM网络中的blocks实际上表示的是transactions（这也是为何使用txCount），若平均TPS为75，则在未来1年半到2年，交易总数将超过
。若超过
，当发生误触发时，对old blockNumber的BLOCKHASH指令返回的将为0，而不是实际的区块哈希值。 长远来看这是一个严重的问题。
详细解决方案参看：
具体为：
- 移除对old blockNumber的判断，直接从smt storage中去查询，若不存在，则查询返回的结果为0：
opBLOCKHASH:
; checks zk-counters
%MAX_CNT_POSEIDON_G - CNT_POSEIDON_G - %MAX_CNT_POSEIDON_SLOAD_SSTORE :JMPN(outOfCountersPoseidon)
$ => A :MLOAD(cntKeccakPreProcess)
%MAX_CNT_KECCAK_F - CNT_KECCAK_F - A - 1 :JMPN(outOfCountersKeccak)
%MAX_CNT_STEPS - STEP - 100 :JMPN(outOfCountersStep)
; check stack underflow
SP - 1 => SP :JMPN(stackUnderflow)
; check out-of-gas
GAS - %GAS_EXT_STEP => GAS :JMPN(outOfGas)
$ => B :MLOAD(SP) ; [blockNumber => B]
; If block number does not exist in the smart conract system, it will return 0
; 不判断BLOCKHASH(oldBlockNumber) 中的oldBlockNumber是否小于当前区块号，都直接从smt storage中取查询。
; Create key for the batch hash mapping key
; set bytes length to D
32 => D
; A new hash with position 0 is started
0 => HASHPOS
$ => E :MLOAD(lastHashKIdUsed)
E+1 => E :MSTORE(lastHashKIdUsed)
B :HASHK(E)
%STATE_ROOT_STORAGE_POS :HASHK(E)
HASHPOS :HASHKLEN(E)
; blockhash key = hash(blockNumber, STATE_ROOT_STORAGE_POS)
$ => C :HASHKDIGEST(E)
%ADDRESS_SYSTEM => A
; set key for smt storage query
%SMT_KEY_SC_STORAGE => B
; storage value in E
$ => E :SLOAD
; store result value in the stack
E :MSTORE(SP++), JMP(readCode); [hash(E) => SP]11. PolygonZkEVM合约中的loop优化 信息类
在PolygonZkEVM合约的_updateBatchFee函数中，会计算在verification time target之前和之后所验证的区块数。更新的fee取决于二者的ratio。 _updateBatchFee函数中的while loop，为找到高于target time的batch数，采用的是后向循环，由最新验证的batch倒推到最早验证的batch，直到找到横跨该target time的last verified batch。
function _updateBatchFee(uint64 newLastVerifiedBatch) internal {
uint64 currentLastVerifiedBatch = getLastVerifiedBatch();
uint64 currentBatch = newLastVerifiedBatch;
uint256 totalBatchesAboveTarget;
uint256 newBatchesVerified = newLastVerifiedBatch - currentLastVerifiedBatch;
while (currentBatch != currentLastVerifiedBatch) { // Load sequenced batchdata SequencedBatchData
storage currentSequencedBatchData = sequencedBatches[
currentBatch
];
// Check if timestamp is above or below the VERIFY_BATCH_TIME_TARGET
if (
block.timestamp - currentSequencedBatchData.sequencedTimestamp > veryBatchTimeTarget
){
totalBatchesAboveTarget += currentBatch - currentSequencedBatchData.previousLastBatchSequenced;
}
// update currentLastVerifiedBatch
currentBatch = currentSequencedBatchData.previousLastBatchSequenced; }
.......
}可将该while loop优化为：
- 因为sequencedTimestamp是严格递增的，第一个找到的sequence time大于target time，则后续的batches直到last verified batch都可认为是高于该target time的。（因为每个next sequencedTimestamp都要小于当前的sequencedTimestamp）。 因此，相应的优化为，计算直到last verified batch的所有batches总数，然后若找到某符合要求的sequence，即可直接跳出循环。
详细解决方案见：
- loop优化 commits
相应的修改为：
/**
* @notice Function to update the batch fee based on the new verified batches
* The batch fee will not be updated when the trusted aggregator verifies batches
* @param newLastVerifiedBatch New last verified batch
*/
function _updateBatchFee(uint64 newLastVerifiedBatch) internal {
uint64 currentLastVerifiedBatch = getLastVerifiedBatch();
uint64 currentBatch = newLastVerifiedBatch;
uint256 totalBatchesAboveTarget;
uint256 newBatchesVerified = newLastVerifiedBatch -
currentLastVerifiedBatch;
uint256 targetTimestamp = block.timestamp - verifyBatchTimeTarget;
while (currentBatch != currentLastVerifiedBatch) {
// Load sequenced batchdata
SequencedBatchData
storage currentSequencedBatchData = sequencedBatches[
currentBatch
];
// Check if timestamp is below the verifyBatchTimeTarget
if (
targetTimestamp < currentSequencedBatchData.sequencedTimestamp
) {
// update currentBatch
currentBatch = currentSequencedBatchData
.previousLastBatchSequenced;
} else {
// The rest of batches will be above
totalBatchesAboveTarget =
currentBatch -
currentLastVerifiedBatch; //设置totalBatchesAboveTarget值
break; //跳出while循环
}
}
..........
}12. verifyMerkleProof函数index size不正确 信息类
DepositContract合约中verifyMerkleProof函数index size不正确：
- index size设置为uint64，而merkle tree level为32，因此，可操控该index的最高有效位，对相同的index进行双花。调用
verifyMerkleProof上下文，index的正确size应为uint32。
function verifyMerkleProof(
bytes32 leafHash,
bytes32[] memory smtProof,
// uint64 index,
uint32 index, //index应为uint32
bytes32 root
) public pure returns (bool) {
bytes32 node = leafHash;
.......详细解决方案见：
- 修改index size commits。
13. PolygonZkEVM合约内重复引用 信息类
合约内应避免重复引用，或引用未被使用的情况。 在PolygonZkEVM合约内，对ERC20BurnableUpgradeable.sol和Initializable.sol存在重复应用问题，应注释掉：
import "@openzeppelin/contracts-upgradeable/token/ERC20/utils/SafeERC20Upgradeable.sol";
//import "@openzeppelin/contracts-upgradeable/token/ERC20/extensions/ERC20BurnableUpgradeable. sol"; // redundant import
import "./interfaces/IVerifierRollup.sol";
import "./interfaces/IPolygonZkEVMGlobalExitRoot.sol";
//import "@openzeppelin/contracts-upgradeable/proxy/utils/Initializable.sol"; // redundant import
import "@openzeppelin/contracts-upgradeable/access/OwnableUpgradeable.sol";
import "./interfaces/IPolygonZkEVMBridge.sol";
import "./lib/EmergencyManager.sol";14. verifyPil与stark generation工具中 plookup与permutation selector多项式不一致 信息类
本质就是，在pil-stark的permutation和plookup中，约束了selector的具体值会参与约束，而pilcom的verifyPil中国，仅对selector做了binary（0/1）判断，事实上selector可为非0非1的其它取值，二者会存在不一致问题，如以permutation为例：
//针对 selC {c, c} is selD {d, d};约束
const N = pols.c.length;
for (let i=0; i<N; i++) {
pols.a[i] = BigInt(i*i+i+1);
pols.b[N-i-1] = pols.a[i];
if (i%2 == 0) {
pols.selC[i] = 1n;
pols.c[i] = pols.a[i];
pols.selD[i/2] = 5n; //为1n才是正确的值。而该不正确的值，verifyPil验证通过，应像stark_gen一样验证不通过
pols.d[i/2] = pols.a[i];
} else {
pols.selC[i] = 0n;
pols.c[i] = 44n;
pols.selD[(N/2) + (i-1)/2] = 0n;
pols.d[(N/2) + (i-1)/2] = 55n;
}
}详细解决方案见：
15. verifyPil与stark generation工具中 permutation约束不一致 信息类
permutation约束中，2个序列必须具有相同的长度。 本质就是，当2个序列的selector选中的长度不一致时，pil-stark中的permutation约束能发现并验证不通过，而pilcom的verifyPil会验证通过，如：
//针对 selC {c, c} is selD {d, d};约束
const N = pols.c.length;
for (let i=0; i<N; i++) {
pols.a[i] = BigInt(i*i+i+1);
pols.b[N-i-1] = pols.a[i];
if (i%2 == 0) {
pols.selC[i] = 1n;
pols.c[i] = pols.a[i];
pols.selD[i/2] = 1n;
pols.d[i/2] = pols.a[i];
} else {
pols.selC[i] = 0n;
pols.c[i] = 44n;
pols.selD[(N/2) + (i-1)/2] = 0n;
pols.d[(N/2) + (i-1)/2] = 55n;
}
}
pols.selC[0] = 0n;//selC和selD选中的序列长度不一致，permutation约束应不通过。而该不正确的值，verifyPil验证通过，应像stark_gen一样验证不通过。详细解决方案见：
16. opcodes/create-terminate-context.zkasm中缺少call depth检查 信息类
opcodes/create-terminate-context.zkasm中的opcode对应为创建新的call context的指令，如opCALL/opDELEGATECALL/opSTATICCALL等等。根据EVM说明书，这些指令的call depth具有上限值 — — 1024。具体参考以太坊黄皮书第37页：
在创建context的opcode中，应增加call depth检查。 不过，当前Polygon zkEVM未增加call depth 1024检查。原因在于：
- 当前事实情况为：call forwards at max 64/64th of the remaining Gas，使得实际上不可能达到1024的深度。因此，本问题可暂不修复。
17. utils.zkasm中重复的JUMP 信息类
在utils.zkasm的readPush中，有3处多余的无条件跳转指令（正常执行即为目标位置），可删除：
// 0 => B :JMP(readPushBlock) //多余的JMP指令
0 => B
readPushBlock:
%MAX_CNT_STEPS - STEP - 20 :JMPN(outOfCountersStep)
@@ -1066,10 +1072,10 @@ readPushBlock:
$ => A :HASHP1(E)
HASHPOS - 2 => HASHPOS
// A*16777216 + C => C :JMP(doRotate) //多余的JMP指令
A*16777216 + C => C
doRotate:
// B - 1 => A :JMP(doRotateLoop) //多余的JMP指令
B - 1 => A详细解决方案见：
参考资料
[1] Polygon zkEVM: Results of Hexens’ Security Audit
附录：Polygon Hermez 2.0 zkEVM系列博客
- ZK-Rollups工作原理
- Polygon zkEVM — — Hermez 2.0简介
- Polygon zkEVM网络节点
- Polygon zkEVM 基本概念
- Polygon zkEVM Prover
- Polygon zkEVM工具 — — PIL和CIRCOM
- Polygon zkEVM节点代码解析
- Polygon zkEVM的pil-stark Fibonacci状态机初体验
- Polygon zkEVM的pil-stark Fibonacci状态机代码解析
- Polygon zkEVM PIL编译器 — — pilcom 代码解析
- Polygon zkEVM Arithmetic状态机
- Polygon zkEVM中的常量多项式
- Polygon zkEVM Binary状态机
- Polygon zkEVM Memory状态机
- Polygon zkEVM Memory Align状态机
- Polygon zkEVM zkASM编译器 — — zkasmcom
- Polygon zkEVM哈希状态机 — — Keccak-256和Poseidon
- Polygon zkEVM zkASM语法
- Polygon zkEVM可验证计算简单状态机示例
- Polygon zkEVM zkASM 与 以太坊虚拟机opcode 对应集合
- Polygon zkEVM zkROM代码解析（1）
- Polygon zkEVM zkASM中的函数集合
- Polygon zkEVM zkROM代码解析（2）
- Polygon zkEVM zkROM代码解析（3）
- Polygon zkEVM公式梳理
- Polygon zkEVM中的Merkle tree
- Polygon zkEVM中Goldilocks域元素circom约束
- Polygon zkEVM Merkle tree的circom约束
- Polygon zkEVM FFT和多项式evaluate计算的circom约束
- Polygon zkEVM R1CS与Plonk电路转换
- Polygon zkEVM中的子约束系统
- Polygon zkEVM交易解析
- Polygon zkEVM 审计及递归证明
- Polygon zkEVM发布公开测试网2.0
- Polygon zkEVM测试集 — — 创建合约交易
- Polygon zkEVM中的Recursive STARKs
- Polygon zkEVM的gas定价
- Polygon zkEVM zkProver基本设计原则 以及 Storage状态机