发表机构
Columbia University（哥伦比亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出ZEBRA框架，通过将zkVM验证转化为解集基数问题并利用约束稀疏性进行并行分支定界搜索，实现高效自动化验证与错误检测，在五个真实zkVM上发现11个零日漏洞。
AI 中文摘要
零知识虚拟机（zkVM）通过将虚拟机语义转化为执行轨迹上的代数约束，实现通用程序的可验证执行。这些约束的正确性至关重要：单个错误约束可能允许伪造证明（约束不足）或拒绝有效执行（约束过度）。现有方法在生产规模下无法提供有意义的保证：模糊测试和单元测试常常遗漏错误，SMT求解器难以应对约束的规模和非线性，而定理证明器则需要大量人工努力。我们提出ZEBRA，一个全自动的验证和错误检测框架：对于给定的程序和输入，约束必须恰好允许一条有效执行轨迹——不多也不少。这将zkVM验证归结为规范轨迹空间上的解集基数问题，其中在计数之前消除了空行填充和非确定性排列等冗余。为了可处理地计算基数，ZEBRA将分析从有限域证据提升到整数区间格，利用zkVM约束的结构稀疏性：在5个真实世界的zkVM中，约束平均仅利用其理论连接容量的14.0%。这种稀疏性使得区间传播紧密且近似误差有限。ZEBRA执行并行分支定界搜索，要么产生具体反例，要么证明在有界区域内不存在违规。我们在五个真实世界的zkVM上评估了ZEBRA。ZEBRA发现了11个零日错误；其中6个已被独立确认，3个已被开发者修复。与基于SMT的验证相比，ZEBRA快51.5倍，验证的实例多16.5个百分点，其范围验证相比重复单输入验证提供高达63倍的效率提升。
英文摘要
Zero-knowledge virtual machines (zkVMs) enable verifiable execution of general-purpose programs by translating virtual machine semantics into algebraic constraints over execution traces. The correctness of these constraints is critical: a single incorrect constraint can admit forged proofs (under-constrained) or reject valid executions (over-constrained). Existing approaches do not provide meaningful guarantees at production scale: fuzzers and unit tests often miss bugs, SMT solvers struggle with the size and nonlinearity of constraints, and theorem provers require substantial manual effort. We present ZEBRA, a fully automated verification and bug-detection framework: for a given program and input, the constraint must admit exactly one valid execution trace - no more and no fewer. This reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting. To compute cardinality tractably, ZEBRA lifts analysis from finite-field witnesses to an integer interval lattice, exploiting a structural sparsity property of zkVM constraints: across 5 real-world zkVMs, constraints utilize only 14.0% of their theoretical connectivity capacity on average. This sparsity enables tight interval propagation with limited approximation error. ZEBRA performs a parallel branch-and-bound search that either produces a concrete counter-example or certifies the absence of violations within a bounded region. We evaluate ZEBRA on five real-world zkVMs. ZEBRA discovers 11 zero-day bugs; 6 have already been independently confirmed and 3 have been fixed by developers. Compared to SMT-based verification, ZEBRA is 51.5x faster, verifies 16.5 percentage point more instances, and its range verification provides up to 63x efficiency gain over repeated single-input verification.
