Theorem 用形式化验证构建 AI 沙箱,机器码级证明访客代码无法改动宿主文件
ChrSzegedy · x · 2026-11-04
Theorem 团队发布「验证沙箱」系列第一部分：基于 MIT 的 xv6iris（约 150 万行 Rocq 证明，在编译后机器码层面验证内核正确性）构建了一个原型 hypervisor，可运行 Linux，并从机器码层面证明了任意访客代码无法修改宿主文件。
- 团队在 xv6 内核内加入类似 KVM 的 hypervisor，并编写了类似 Firecracker 角色的 vmm 程序，在虚拟机中加载不受信代码
- 核心主张：沙箱必须像密码学原语一样可信，唯一可行路径是把形式化验证扩展到计算机系统领域，以保护互联网基础设施免受 agent 与恶意行为者威胁
- 团队称这是验证生产级沙箱的第一步，更多成果即将发布
「编程与Agent」频道最新
- Device MCP 发布：让 Claude/Codex 直接操控真实 iPhone 做 UI 测试 — rudrank · 2026-11-04
- 开发者用 Gemini 4 Argon 加 Antigravity 制作融化三明治 WebGPU 动画 — AI_Andrew · 2026-11-04
- 团队想从 IDE 补全转向云端异步后台编码 Agent，求选型建议 — Extension_Lake4065 · 2026-11-04
- ≤4B 小模型 Agent 实测:Qwen3.5-4B 得 51.4%,思考模式最多提升 20 分 — KienShen · 2026-11-04
- 用外部确定性状态层治 AI 编码失忆:三篇论文给出会话管理新思路 — ApprehensiveSkin7975 · 2026-11-04
- 字节跳动等开源 Axion 1.0：三阶段训练的 Agent 基础模型 — Yuqi Jia · 2026-11-04