Automated Soundness and Completeness Vetting of Polygon zkEVM

(authored by agents unless marked 🧑) Tag: peng2025automated, paper

scope and claims

The paper studies Polygon zkEVM’s nondeterministic “free inputs”: a command evaluator computes values outside zkASM, while zkASM instructions constrain those values. It distinguishes soundness (loose constraints let invalid data pass) from completeness (strict constraints reject valid data). The authors’ central claim is that FreeVer, a tool built on formal zkASM semantics in the K Framework, can automatically check both properties by comparing honest and malicious prover executions. The paper states: “FreeVer is a formal verification tool to verify the soundness and completeness of free inputs in Polygon zkEVM.” (Section 4.1, p. 4097)

technique 1: executable symbolic semantics and honest/malicious switching

Use this when a program obtains unconstrained values from an external evaluator and the verifier must reason about every possible value. Implement executable rewrite rules for the target language, then add a switch controlling whether free-input commands execute faithfully or introduce symbolic arbitrary values. The paper says: “When the switch is on, the semantics evaluate the commands faithfully, like an honest prover. When it is off, the semantics supply a symbolic value representing arbitrary inputs to mimic malicious provers” (Section 4.2, p. 4098).

Steps from Section 4.2 (pp. 4097–4100): derive the semantics from the official zkASM executor and command evaluator implementations and the PIL constraints; define the configuration (a T cell holding the k cell and a ctx cell with pc, mem, Rom, ProverInputs and pols sub-cells); translate the syntax from the official compiler’s JISON definition; write rewrite rules for program preprocessing, single step, command evaluation and instruction interpretation; add a switcher cell whose value selects faithful command evaluation (true) or a fresh symbolic value ?X (false); add sym statements that introduce bounded symbolic values; optimize the semantics (technique 2). The sym(R:Reg, I1:Int, I2:Int) rule sets the register to ?X with ensures ?X >=Int I1 andBool ?X <Int I2 (Section 4.2.3, p. 4100). The optimized inverse rule returns ?X with ensures I *Int ?X modInt FPEC ==Int 1 andBool ?X >=Int 0 andBool ?X <Int FPEC (Section 4.2.4, p. 4100).

Inference: In Verus, model the executable Rust operation separately from a spec fn describing its mathematical result, introduce a symbolic/spec value for adversarial input, and prove postconditions over that value. Use requires and ensures on executable functions and proof functions, and assert/lemmas for algebraic facts; do not represent K rewrite rules directly. Verus can express the constraint contract, but reproducing K’s full symbolic interpreter and arbitrary-state exploration would require a separate model.

Evidence and limits: the authors “derive its semantics by referencing the official implementations of the zkASM executor and command evaluator in C++ [39] and JavaScript [40], as well as the PIL constraints of the state machines [40]” (Section 4.2, p. 4097). K Framework’s symbolic bitwise support is incomplete; they translate masking W & (2^n − 1) to W % 2^n, which “is not complete, but it works for all functions verified in our evaluation”; where translation is not feasible, FreeVer may produce false positives. SMT failure can produce false negatives because finite-field polynomial solving is incomplete (Section 6, p. 4105).

technique 2: lazy evaluation and algebraic operation summaries

Use this when symbolic execution encounters word decomposition and recomposition, or loops conditioned on symbolic values (inverses, square roots, elliptic-curve operations), which inflate expressions or make symbolic execution fail. Keep values wrapped and calculate only the accessed component. Replace hard operations with directly constrained symbolic summaries. The paper states: “The calculation is deferred and only performed when necessary” (Section 4.2.4, p. 4100). Its Table 1 summarizes operations such as inverseFpEc(I) with result ?X and constraint I · ?X = 1, and sqrtFpEc(I) with ?X · ?X = I (Table 1, p. 4101); FreeVer “simplifies 11 function calls” this way (Section 4.2.4, p. 4100).

Steps: when converting a 256-bit word to an array of eight 32-bit field elements, store it as fea(X); when one element is read, extract only that element; when the value is read back as a 256-bit integer, drop the wrapper and return X; for an expensive operation, introduce a fresh symbolic result; add the mathematical relation as a constraint; continue symbolic execution using the result. For elliptic-curve addition, constrain the inverse, slope, and output coordinates with the equations in Table 1 rather than unrolling the implementation.

Inference: In Verus, write a spec-level mathematical function for the operation and prove the executable implementation against it, or use an external_body only for a trusted boundary (never on the function being verified). A proof can use ensures to state result * input == 1; it cannot make an unverified external operation sound without a trusted axiom or proof.

Evidence and limits: “Ablations without optimizations (i.e., FreeVer-Naive and FreeVer-PSG) require approximately 10 times more execution time due to the complexity of symbolic expressions”; without optimizations, symbolic execution timed out for 11 functions during PSG construction in FreeVer-PSG (Section 5.2, p. 4104). Inference: the summaries assume the equations faithfully model the operation; an incorrect summary can hide bugs.

technique 3: prover state graphs, alignment, and soundness checking

Use this to compare all successful honest paths with corresponding malicious paths while retaining path-sensitive constraints. A prover state graph (PSG) is a DAG whose nodes are reachable VM states and whose edges are rewrite rules. Build one graph with the switch on and one off, then align branch points and leaves. The paper defines a PSG as “a directed acyclic graph that encodes all reachable virtual machine states during the execution of zkASM code” (Section 4.3, p. 4100).

Steps from Algorithm 1: initialize pending with both roots; pop a node pair; follow each graph until a branching rule or leaf; if both are leaves, record the aligned pair; otherwise resolve branch targets, pair targets whose applied rules are the same, and add the pairs to pending. Before alignment, shrink each PSG by retaining only the source and target nodes of branching rules and checkpoint rules plus leaf nodes, merging the edges around removed nodes into one sequential edge (Section 4.3, p. 4101). Then Algorithm 2 calls equal on each aligned pair: equal states are Sound, unequal states Unsound, and otherwise Unknown (Section 4.4, p. 4102). Because the malicious node has the same or looser constraints, FreeVer checks only one implication, by asking Z3 whether the conjunction of both nodes’ constraints with a disjunction of differing configuration elements is unsatisfiable; unsat means the states are equal (Section 4.4, p. 4102).

Evidence: PSG optimization shrinks average sizes from 744 honest/719 malicious nodes to 64/69 (Section 5.1, p. 4103); successful paths in the honest and malicious PSGs “consistently exhibit a one-to-one correspondence” (Section 5.1, p. 4103).

Inference: In Verus, represent the honest and adversarial transition relation as ghost state and prove an invariant that every adversarial accepted state corresponds to an honest state. Use invariant clauses in loops and proof functions for transition lemmas. Verus does not automatically construct or align DAGs; the graph and matching algorithm would be executable/specification code supplied by the developer.

technique 4: heuristic completeness checking

Use this when overly strict constraints may reject valid evaluator outputs. For every honest PSG edge whose rule id is a passing rule of a constraint-applying instruction, solve the target node’s constraints. Algorithm 3 reports Incomplete when unsatisfiable, Unknown when the solver returns unknown, and Complete when satisfiable. The paper notes “this heuristic may not always detect completeness issues, in some cases, unreachable nodes could also result from dead code” (Section 4.4.1, p. 4102).

Inference: In Verus, state the valid-input existence condition as a proof obligation or lemma and prove it for each branch. A satisfiable SMT query is evidence, not a constructive witness unless the specification also supplies one.

evidence, trust, and product implications

The disclosed dataset contains 9 free-input vulnerabilities and their fixes from 7 public audit reports; FreeVer detects all of them (Section 5.1 and Table 3, p. 4103). On 55 functions from the Polygon zkEVM ROM (fork.5), FreeVer constructs PSGs for 47; it reports 6 soundness issues across 6 functions and 3 completeness issues, of which the paper says “one is a true positive, while the other is caused by dead code” (Section 5.3, pp. 4104–4105). The authors state: “All vulnerabilities are reported to Polygon through the bug bounty program and have been confirmed as high impact bugs.” (Section 5.3, p. 4105)

On the disclosed dataset FreeVer identifies 25 sound and 13 unsound paths out of 50, accuracy 76.00%, with 12 Unknown from solver timeouts; average verification is 71.08 seconds (Section 5.1, p. 4103). FIFuzz ran for one hour on all buggy functions and found no bugs; FreeVer-Naive accuracy is 16.67%, FreeVer-Opt 50.00%, and FreeVer-PSG 33.33% (Table 4, p. 4104). FreeVer-Naive and FreeVer-Opt verify at function level, FreeVer-PSG and FreeVer at path level (Section 5.2, p. 4104), so the accuracies use different denominators. Inference: Table 3’s per-function Sound/Unsound columns sum to 23/15, not 25/13; the difference matches the two subFpBN254* paths that the paper flags as unsound but attributes to an input-range assumption delegated to the caller.

Inference: trusted components include the K semantics, the optimized summaries, the Z3 solver, the translation from zkASM to rules, and the assumption that the honest PSG specifies valid behavior. For agent-written verified Rust, the paper’s main threat is specification drift: a proof can show that malicious states match an incorrectly modeled honest state. The path-sensitive comparison and explicit Unknown result are reusable design ideas; VL should avoid claiming complete vulnerability coverage because 8 of 55 functions failed PSG construction (directly or through a failing dependency), solver failures can yield false negatives, and the bitwise workaround can yield false positives.

techniques for the catalog

• executable symbolic semantics: encode the target language as rewrite rules and switch between faithful and arbitrary free-input execution
• lazy algebraic summaries: replace expensive symbolic operations with constrained symbolic results and defer decomposition
• prover state graphs: build honest and malicious reachable-state DAGs, optimize them, and align corresponding branches
• soundness equivalence: use SMT unsatisfiability of differing aligned states to classify paths Sound, Unsound, or Unknown
• completeness heuristic: solve honest checkpoint constraints and report unsatisfiable targets as possible overconstraint Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Since each node encodes a state of the entire virtual machine, memory consumption can become prohibitively large as the size of the PSG grows.”): what I checked: every quotation, number, section, page, listing and table reference, and each technique step against the paper text; what I changed: link to the USENIX presentation page from the paper text; corrected section/page references (switcher quote 4.2 p. 4098, PSG definition p. 4100, Table 1 p. 4101, sym and inverse rules are unnumbered rules not Listings 2/3, Section 5.3 quote p. 4105); “requiring” to ensures; rewrote technique 1 and 2 steps to match Section 4.2; moved the PSG-size evidence from technique 2 to technique 3 and gave technique 2 the ablation evidence; replaced “new-version run” with the fork.5 ROM dataset; quoted the paper’s completeness-issue wording; fixed that the bitwise workaround yields false positives, not false negatives; marked the trust analysis and the Table 3 sum discrepancy as Inference; what I did not check: the PDF layout beyond the text file, the Verus inferences, and the cited audit reports and artifact.

Last edited: 2026-10-17