Amazon Science·· 2026-06-10精选AI 评分76
AWS EC2 M9g 实例推出经形式化验证的隔离引擎
EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
AI 导读
AWS 宣布 EC2 M9g 和 M9gd 实例正式可用，首次搭载 Graviton5 处理器并配备 Nitro Isolation Engine。该组件是首个部署在商用云环境的形式化验证 Hypervisor，使用 Isabelle/HOL 完成 33 万行机器检查数学证明，涵盖保密性、完整性、功能正确性、无运行时错误和内存安全。
推荐理由
给出了可量化的验证规模和语言选择，读者可以据此评估云虚拟机隔离的形式化保障程度。
来源：Amazon Science · amazon.science