微软用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」频道最新
- 拆解两款真实「公司大脑」：Slite 与 Gorgias 同台对比构建之道 — femke_plantinga · 2026-09-11
- 浏览器主线程很贵:动画卡顿的真正成本与前端优化实践 — jh3yy · 2026-09-11
- 开源工具 Claude Unlimited：多账号轮换让 Claude Code 会话不断线 — Similar_Injury_6739 · 2026-09-11
- 受 OpenAI 万机群启发，开发者开源 agent 众包解题平台 — Benjaminsen · 2026-09-11
- 开源 Mac 应用 Lucid：只在跑 AI 时阻止笔记本休眠 — Pitiful_Hedgehog_600 · 2026-09-11
- 20kb 函数匹配达成,banteg 召集 AI 逆向 Snail Mail 剩余 20 个挑战 — banteg · 2026-09-11