Coral：连接语法分析与零知识证明
语法分析是计算中那些基础却常被忽视的操作之一。当浏览器渲染网页、防火墙检查流量或编译器转换代码时，总有某个解析器在默默地将原始字节流转换为结构化对象。我们往往认为这一步理所当然，假设输入一旦被解析，系统的其余部分就能安全地对其进行推理。我们也通常期望浏览器或编译器能够“开箱即用”地完成这项工作，并即时修复任何解析错误。
在日常计算中，这种期望并非不合理。浏览器能够优雅地从格式错误的HTML中恢复，编译器会标记语法错误以便开发者修复。但在隐私保护验证场景中，特别是在零知识证明系统中，这种假设和宽容会带来问题。证明者可能承诺某个字节流表示有效的JSON文档、令牌或源文件，却从未证明解析过程是否正确执行。验证者无法访问底层数据，无法判断证明者是否诚实。
ZK应用中的缺失环节：Coral
过去十年间，密码学社区在零知识的大旗下探索了许多雄心勃勃的想法：证明TLS会话的陈述、验证数字凭证的属性、检查编译链、在不暴露底层流量的情况下执行网络策略。然而所有这些都共享着一种无声的脆弱性。
以zk-TLS为例。用户可能想向智能合约证明其银行API报告了特定余额。当今的方法通常假设API响应已经是格式良好的JSON对象（或HTML）。如果银行的服务器配置错误或遇到故障导致输出格式错误的响应（非有效JSON或HTML），恶意证明者可能滥用这种格式错误的响应来说服验证者相信错误的事实。类似的缺口也出现在处理JWT的zk-Authorization系统中，或是在检查流量却无法保证数据流符合其形式文法（无论是JSON、HTML还是HTTPS）的zk-Middleboxes中。
Coral的方法
Coral的方法始于一个简单观察：在许多场景中，验证计算结果远比执行计算本身容易，特别是当验证者获得适当提示时。一个经典例子是排序：生成排序列表需要O(n log n)时间，但验证列表是否正确排序（且对应于给定原始列表）只需单次遍历，或O(n)时间，如果证明者提供排序输出及原始列表中每个元素的映射。
语法分析展现出相同的结构。语法分析是确定输入字节串是否符合给定文法的过程，如果符合，则生成证明这一符合性的解析树。执行完整的语法分析算法是一个复杂、有状态的过程，但验证语法分析结果（通常表示为解析树）则容易得多。Coral不是将解析器功能本身编码到电路中或在zkVM内模拟它，而是假设不可信的解析器已生成候选解析树，并专注于检查该输出相对于私有原始字节流和公共文法是否正确。
然而这带来了表示挑战：标准上下文无关文法（CFG）的解析树自然包含具有任意数量子节点的节点。这种可变度节点难以映射到基于电路的证明系统中，后者更喜欢统一、固定元数的结构。Coral通过应用经典的编译器技术转换来克服这一点。解析树被转换为左孩子右兄弟（LCRS）二叉树，这种表示编码相同的结构但确保每个节点最多有两个出边：一个指向其第一个孩子，一个指向其下一个兄弟。这种二进制、统一的布局保留了原始文法的完整语义，同时与R1CS约束的固定元数布线对齐。
实现与性能
该实现用Rust编写，证明了现实输入（如JSON API响应、TOML配置文件和C源代码子集）的语法分析。证明简洁（小于20 kB）、生成快速（数秒）且验证廉价（小于70毫秒）。重要的是，它们仅需要几千兆字节内存且无需特殊硬件，使得在普通笔记本电脑上即可实现。
迈向更广泛的应用
随着零知识语法分析成为可能，新的途径正在打开。例如，证明者可以承诺TLS记录，不仅证明某些字段存在，而且证明记录本身在相关文法下正确解析。用户可以证明凭证的属性而不暴露令牌或其结构，知道格式错误的输入无法欺骗验证者。通常不透明且难以审计的编译链可以被端到端证明：从源代码到二进制文件，包含语法分析步骤。甚至中间盒也可以在尊重隐私的同时执行策略，因为它们可以依赖关于流量语法结构的证明，而不是信任不透明的字节流。
Coral不是完整的解决方案。许多现实世界的格式，如HTML、PDF和Python，不是上下文无关的。实践中，许多常用文法依赖优先级和复杂的否定谓词，这些我们尚未支持。将Coral扩展到处理上下文相关特征仍然是一个开放且重要的挑战。但通过解决字节承诺与结构化对象证明之间的基本缺口，Coral为新一代ZK系统奠定了基础。
与密码学协议的复杂性相比，语法分析可能显得平凡，但在许多方面它是基石。没有输入被正确解析的保证，高层证明风险建立在沙子上。Coral从沙子中生长：通过证明将其夯实。Coral证明这一基石可以被带入零知识领域：快速、简洁且实用。通过使语法分析可证明，我们希望Coral帮助解锁那些可验证性和隐私不是权衡而是伙伴的应用，以及我们依赖的结构化对象可以与密码学证明本身同样严谨地进行推理的应用。
了解更多
Coral已被IEEE S&P 2026接收，如想了解更多请参会！或者你可以试用我们的代码：https://github.com/eniac/coral
脚注
- zkVM是一种虚拟机，其执行可以在零知识证明系统内被证明。与为每个计算编写自定义电路不同，zkVM让开发者运行任意程序（通常使用固定指令集如RISC-V或WASM），然后生成简洁证明证明程序在某个输入上正确执行，可选地隐藏输入和中间状态。