云虚拟机管理程序的微验证。信用:Jason Nieh和Gu/ Columbia Engineering每当你在亚马逊上买东西时，你的客户数据会自动更新并存储在云中的数千台虚拟机上。对于亚马逊这样的企业来说，确保其数百万客户的数据安全至关重要。无论是大公司还是小公司都是如此。但是到目前为止，还没有办法保证软件系统不受bug、黑客和漏洞的攻击。哥伦比亚工程研究人员可能已经解决了这个安全问题。他们开发了SeKVM，这是第一个通过数学证明来保证云中虚拟机安全性的系统。在将于2021年5月26日在第42届IEEE安全与隐私研讨会上发表的一篇新论文中，研究人员希望为系统软件验证的未来创新奠定基础，从而产生新一代具有网络弹性的系统软件。
SeKVM是第一个经过正式验证的云计算系统。形式验证是关键的一步，因为它是证明软件在数学上是正确的，程序代码正常工作，并且没有隐藏的安全漏洞需要担心的过程。
计算机科学教授、软件系统实验室联合主任Jason Nieh说:“这是第一次证明现实世界的多处理器软件系统在数学上是正确和安全的。“这意味着用户的数据由在云端运行的软件正确管理，并且不会受到安全漏洞和黑客的攻击。"
构建正确、安全的系统软件一直是计算面临的重大挑战之一。| Nieh自1999年加入哥伦比亚工程公司以来，一直致力于软件系统的不同方面。当计算机科学唐家助理教授、形式验证专家谷于2018年加入计算机科学系时，他和聂决定合作探索软件系统的形式验证。
他们的研究引起了极大的兴趣:两位研究人员都获得了亚马逊研究奖、美国国家科学基金会的多项资助，以及国防高级研究计划局(DARPA)价值数百万美元的合同，以进一步开发SeKVM项目。此外，聂赫留朵夫还因此获得了古根海姆奖学金。
在过去的十几年里，形式验证受到了很大的关注，包括验证多处理器操作系统的工作。“但所有这些研究都是在现实生活中无人使用的类似玩具的小系统上进行的，”顾说。“验证一个多处理器商品系统，一个像Linux这样广泛使用的系统，被认为或多或少是不可能的。”
云计算的指数级增长使公司和用户能够将其数据和计算从异地转移到运行在云中主机上的虚拟机中。像亚马逊这样的云计算提供商部署虚拟机管理程序来支持这些虚拟机。
云虚拟机管理程序的微验证。功劳:杰森·涅和·古/哥伦比亚工程公司虚拟机管理程序是使云计算成为可能的关键软件。虚拟机数据的安全性取决于虚拟机管理程序的正确性和可信度。尽管虚拟机管理程序很重要，但也很复杂——它们可以包含整个Linux操作系统。仅仅是代码中的一个薄弱环节——通过传统测试几乎不可能检测到的环节——就可能使系统容易受到黑客攻击。即使虚拟机管理程序写得99%正确，黑客仍然可以潜入特定的1%设置并控制系统。
Nieh和Gu的工作是第一次验证一个商品系统，特别是广泛使用的KVM虚拟机管理程序，它被亚马逊等云提供商用来运行虚拟机。他们证明了SeKVM是安全的，并保证虚拟计算机相互隔离，SeKVM是带有一些小变化的KVM。
“我们已经表明，我们的系统可以保护和保障上传到云中的私有数据和计算，并提供数学保证，”顾的博士生、该论文的共同第一作者李说。“这是以前从未有过的。”
使用验证大型系统安全属性的新框架MicroV对SeKVM进行了验证。它是基于这样一种假设，即对系统的微小改变可以使其更容易验证，这种新技术被研究人员称为微验证。这种新颖的分层技术对现有系统进行了改造，并将强制安全的组件提取到一个经过验证并保证整个系统安全的小核心中。
改造一个大型系统所需的改变相当有限——研究人员证明，如果大型系统的小核心完好无损，那么该系统是安全的，不会有私人数据泄露。这就是他们如何能够验证像KVM这样的大型系统，这在以前被认为是不可能的。
“想象一所房子——干墙的裂缝并不意味着房子的完整性有风险，”涅解释道。“结构上还是比较健全的，关键的结构体系还是不错的。”
Nieh的博士生、该研究的合著者施-李玮补充道，“SeKVM将在从银行系统和物联网设备到自动驾驶汽车和加密货币的各个领域发挥保障作用。”
作为第一款经过验证的商用虚拟机管理程序，SeKVM可以改变云服务的设计、开发、部署和信任方式。在一个网络安全日益受到关注的世界里，这种弹性是非常需要的。主要的云公司已经在探索如何利用SeKVM来满足这一需求。
这项研究的标题是“一个安全且经过正式验证的Linux KVM虚拟机管理程序。”
该研究将于2021年5月26日在第42届IEEE安全与隐私研讨会上发表。
来源：由phyica.com整理转载自PH，转载请保留出处和链接！
