arXiv cs.AI· Chuyue Sun, Su Fong, Zhiyi Kuang, Yizheng Jiao, Nina Narodytska, Haoze Wu, David L. Dill, Clark Barrett·· 11 小时前AI 评分58
CryptoProver：从 API 契约自动合成密码库验证证明
An AI Approach to Verified Production Cryptographic Libraries
AI 导读
研究团队提出 CryptoProver，可从高层 API 契约自动合成内部规格与经 Verus 检查的证明，在不改动可执行代码的前提下为 curve25519-dalek 构建独立证明，并依据 RFC 8439 规格验证 RustCrypto 此前未验证的 chacha20 实现。
正文 · AI 翻译
摘要：密码学代码是必须保证正确性的关键基础设施，然而对生产级库进行形式化验证仍然困难。现有的语言模型证明系统在规范和前提已给定的情况下解决孤立的证明义务，生产级库的验证问题仍未解决。
我们提出 CryptoProver，一个基于 AI 的系统，它从高层 API 契约出发合成内部规范与经 Verus 检查的证明。在不改动可执行代码的前提下，CryptoProver 为 curve25519-dalek 构建了一个新的独立证明，并依据 RFC 8439 规范验证了 RustCrypto 此前未经验证的 chacha20 实现。这些密码学谱系支撑着包括 Signal 和 Shadowsocks 在内的已部署系统；Signal 的全球下载量估计达 2.18 亿次。原开发者报告称，验证 curve25519-dalek 是一项由三人专注投入五个月的工作。在给定 API 契约以及一个固定的可信库（包含域规范、算术事实、公理和 vstd）的情况下，CryptoProver 在 11.4 小时内合成了内部规范与证明，记录的 API 成本为 466.99 美元。CryptoProver 遵循信任优先的设计原则：机械门禁会拒绝规范弱化、凭空捏造的公理以及跨模块破坏，而隔离机制则阻止检索参考证明，包括从 git 历史中检索。
| 学科： | 密码学与安全（cs.CR）；人工智能（cs.AI） |
| 引用为： | arXiv:2608.00965 [cs.CR] |
| （或 arXiv:2608.00965v2 [cs.CR] 为本版本） | |
| https://doi.org/10.48550/arXiv.2608.00965 由 DataCite 颁发 arXiv DOI |
提交历史
来自：Chuyue Sun [查看邮箱]
[v1]
2026年8月2日 周日 03:32:08 UTC（146 KB）
[v2]
2026年10月16日 周五 09:00:33 UTC（154 KB）
来源：arXiv cs.AI · arxiv.org