利用零知识证明重塑漏洞披露机制
背景与目标
我们与约翰霍普金斯大学的合作伙伴Matthew Green共同致力于利用零知识证明（ZK）技术构建可信环境，使科技公司与漏洞研究人员能够安全沟通，避免破坏或轻视。这项为期四年的研究将推动ZK证明从理论走向实践，为漏洞研究人员提供生成可利用性ZK证明的软件工具。该研究隶属于DARPA“加密验证与评估信息保护（SIEVE）”项目。
当前ZK技术多聚焦于区块链应用（如验证交易合规性），而我们的工作将显著扩展ZK可证明陈述的类型。项目完成后，用户将能证明关于x86处理器上运行程序的陈述。
为何需要可利用性ZK证明？
软件厂商与漏洞研究者在漏洞报告过程中常存在对立关系：过早披露漏洞会损害厂商声誉，而过度披露细节会削弱研究者收益。沟通破裂导致技术行业受损，且企业常忽视安全团队警告，使研究者陷入两难——保持沉默或公开披露（后者可能告知攻击者利用路径）。
ZK证明能彻底改变漏洞披露模式：企业可精确定义漏洞赏金范围，研究者能明确证明拥有有效利用代码且无需公开披露风险。
ZK证明设计原理
ZK证明允许证明者向验证者证实拥有某信息而不泄露信息本身（例如证明知道SHA256原像而不透露密码）。其核心效率指标包括：
- 证明者时间：生成证明所需时间
- 验证者时间：验证证明所需时间
- 带宽：协议中双方传输的数据量（非交互式证明仅含证明大小）
关键挑战在于将待证明陈述转换为无循环的布尔或算术电路（布尔电路使用AND/NOT/XOR门，算术电路使用ADD/MULT门）。循环程序需先展开，但数据依赖型循环往往无法处理。此外，电路规模直接影响协议效率——证明者时间通常与电路规模呈线性关系（每门操作存在较大常数开销）。
证明可利用性的技术实现
由于ZK证明接受布尔电路表述的陈述，核心挑战是将漏洞利用转化为仅当利用成功时返回"true"的布尔电路。该电路需满足：
- 架构精确建模：因二进制利用通常依赖特定处理器架构，电路需精确模拟目标程序的编译架构
- 执行验证：电路需接受程序成功运行且在执行过程中触发漏洞的条件
初始方案及缺陷
基础方案是构建模拟处理器"单步执行"的电路：初始化内存（含待执行程序）、设置程序计数器，让证明者基于恶意输入运行程序——重复处理器电路直至程序结束，并每步检查是否满足漏洞条件（如程序计数器设为已知恶意值、特权内存地址被写入）。但此方案需每步运行完整处理器电路（避免泄露执行轨迹信息），导致电路规模过大：即使仅50MB内存的机器，100条指令的跟踪也会产生至少5GB电路，效率不可行。
高效解决方案：SNARKs for C方法
采用SNARKs for C的分割证明策略：
- 逻辑有效性证明：处理器电路应用于程序跟踪中每对连续指令，验证寄存器状态转换合法性（假设内存操作正确）
- 内存验证：证明者提供按内存地址排序的执行跟踪，通过线性扫描确保内存访问一致性（避免电路规模与RAM大小成正比）
- 排列检查器电路：验证内存排序跟踪与原始跟踪对应，防止伪造证明
x86架构建模实践
为实现真实场景中的ZK证明，需将实际处理器架构建模为布尔电路。现有工作基于RISC架构TinyRAM（专为ZK场景设计），但商业应用需支持x86等复杂架构。
实施路线
- 从MSP430起步：先为广泛使用的嵌入式微处理器MSP430建模（Microcorruption CTF平台基础），完成Microcorruption挑战的ZK证明作为可行性验证
- 攻克x86复杂性：x86作为复杂CISC机器，单周期电路需10万门级。若直接建模，万条指令的利用将产生48GB证明，显然不现实
关键技术突破
- 动态子集生成：通过程序分析确定二进制文件所需的最小x86指令子集，动态生成处理器验证模型（实际程序通常仅使用数百条指令）
- 静态二进制转换器：处理不支持指令（如数据依赖循环指令
repz），将其转换为程序特定x86子集，避免硬编码到处理器电路中
漏洞披露新范式
我们与约翰霍普金斯大学及DARPA SIEVE项目同事共同推动此项工作，旨在：
- 工具开发：提供彻底改变漏洞披露方式的工具，使企业能精确界定漏洞赏金范围，研究者能安全提交漏洞存在证明
- 消费者保护：ZK漏洞披露可作为保护机制——研究者可警告用户设备风险而不公开漏洞细节，迫使企业修复原本可能忽视的问题
- 技术普及：推动ZK证明从学术界走向工业界，提升其在现代软件中的可用性与实用性
欢迎具有未提及应用场景的机构与我们联系，我们在ZK证明方案和电路编译器复杂生态中积累了丰富经验，可提供协助！
分享至: Twitter | LinkedIn | GitHub | Mastodon | Hacker News