EC2正式验证"隔离引擎"，从数学层面保障虚拟机安全隔离

亚马逊EC2的Nitro隔离引擎是Nitro虚拟机监控程序的核心组件，也是首个在商业云环境中部署的经过正式验证的虚拟机监控程序。该引擎采用Isabelle/HOL证明助手完成验证，生成了33万行机器验证数学代码，规模与s...