/
经过验证的机器学习基础设施安全研究报告
随着前沿AI系统的快速发展，保障其运行基础设施的安全变得尤为迫切。恶意攻击者可能窃取模型权重或破坏系统运行，而失控的AI系统也可能利用自身基础设施漏洞绕过安全监控。研究人员于2026年初调查了23位专家，探讨形式化方法能否有效降低AI基础设施风险，并分析了机器学习推理与训练栈中最适合形式化验证的组件、可保障的安全属性及现有落地障碍，为AI实验室、硬件厂商及政府机构提供了初步建议与技术路线图。
Apple在GitHub上发布iPhone与Mac后量子密码学代码
苹果近日在GitHub发布了corecrypto源代码库，并附上详细技术说明，介绍其在iPhone、Mac等设备上推进后量子密码学工作的成果。此次发布包含ML-KEM与ML-DSA两种后量子算法的实现代码、测试工具及形式化验证材料。苹果表示，通过自研形式化验证方法，成功发现了常规测试无法检测到的漏洞，确保加密实现的正确性，旨在推动全球密码学社区的技术进步与安全审查。
Isabelle/HOL：驱动Nitro隔离引擎背后的形式化证明工具
AWS在2025年re:Invent大会上发布了Nitro隔离引擎（NIE），并采用证明辅助工具Isabelle/HOL完成了其正确性与安全性的形式化验证，使NIE成为首个经过形式化验证的云虚拟机监控程序。文章详细介绍了Isabelle/HOL在表达能力、自动化程度、证明可读性和可扩展性方面的优势，以及其在NIE验证中的具体应用，包括分离逻辑实现与25万行证明代码的高效处理。
亚马逊推出高性能后量子密码学实现方案
亚马逊推出mlkem-native高保证、高性能的ML-KEM C语言实现，结合参考实现的简洁性与研究优化及形式化验证。利用CBMC和SLOTHY等自动化工具确保内存安全、类型安全和功能正确性，在数学确定性基础上实现激进的汇编优化。相比ML-KEM参考实现，mlkem-native在不同EC2实例上每秒操作数提升2.0到2.4倍，同时保持安全性和可维护性。
Ironclad OS项目：用Ada语言构建Unix内核
Ironclad OS项目正在开发一个新的类Unix操作系统内核，面向小型嵌入式系统，计划支持实时功能。该项目的独特之处在于采用Ada编程语言及其可形式化验证的SPARK子集进行开发，而非常见的C、C++或Rust语言。项目还包含运行在Ironclad内核上的完整操作系统Gloire，使用GNU工具构建以提供传统Unix兼容性。
京公网安备 11010802021500号
