/
数学证明保障隔离 关键字列表
EC2正式验证"隔离引擎"，从数学层面保障虚拟机安全隔离
亚马逊EC2的Nitro隔离引擎是Nitro虚拟机监控程序的核心组件，也是首个在商业云环境中部署的经过正式验证的虚拟机监控程序。该引擎采用Isabelle/HOL证明助手完成验证，生成了33万行机器验证数学代码，规模与seL4项目相当。验证过程涵盖机密性与完整性、功能正确性、运行时错误缺失及内存安全四类属性，并已作为Graviton5用户的默认功能上线。
白皮书
京公网安备 11010802021500号
