微软用AI Agent验证Rust密码学代码
Microsoft Research · rss · 2026-07-14
微软研究院发文介绍如何利用 Rust、Lean、Aeneas 和 AI agents 来扩展生产级密码学算法的形式化验证。
- 背景：密码学代码对安全性要求极高，传统测试不足。微软在 SymCrypt（Windows 和 Azure 使用的加密库）中用安全 Rust 重写算法，并用 Lean 框架进行形式化验证。
- 方法：使用 Aeneas 工具将 Rust 代码翻译为纯 Lean 模型，证明其符合标准规范。AI agents 被引入来编写可独立验证的证明，从而扩展自动化规模。
- 进展：已开源包含 SHA-3 和 ML-KEM（后量子密码）完整证明的代码分支，正扩展至 AES-GCM 等更多算法。
- 优势：软件工程师可继续编写高性能 Rust 代码，验证工程师则在生成的 Lean 模型上工作，互不干扰。
「编程与Agent」频道最新
- 让 Hermes Agent 当 QA：浏览器实测揪出 8 个网站问题 — techlatest_net · 2026-10-27
- 开源 FableCut 用远程 MCP 让 AI Agent 直接剪辑浏览器时间线 — FastPresence9799 · 2026-10-27
- 网友给 Hermes Agent 配专属 Ubuntu 虚拟机实测真实任务表现 — techlatest_net · 2026-10-27
- 开发者晒弃用清单：VS Code、Office 全卸载，只用 Claude — One_Improvement_6470 · 2026-10-27
- Grok bot 首次自主网购：识破页面隐藏提示，1 美元开通 Spotify 后秒取消 — msg · 2026-10-27
- Swarmatory 开源：为团队编码 Agent 提供共享聊天室与信息流 — qhoxie · 2026-10-27