零漏洞，零隐患：首款云服务“安保”系统问世_风闻

哥伦比亚大学开发的SeKVM是第一款经数学证明能确保云虚拟机安全性的系统。

云管理程序的微管理。

客户在亚马逊商城购物时，其数据会自动更新并被存储到“云”的虚拟机中。对于亚马逊这种级别的企业来说，确保数百万客户的数据安全至关重要。然而，网络工程师们目前还无法确保软件系统的绝对安全。eurekalert.org网站当地时间5月24日报道，美国哥伦比亚大学的研究人员向着解决这个重大网络安全问题迈出了巨大一步。他们开发的SeKVM是第一款经数学证明能确保云虚拟机安全性的系统。该系统将为新一代网络弹性系统软件的开发奠定基础。相关研究成果将在第42届IEEE安全与隐私研讨会中发布。

形式验证是证明软件数学正确、程序代码能够正常工作的关键步骤。“SeKVM是现实世界中第一种经形式验证证实数学正确性与安全性的多处理器软件系统。”哥大教授Jason Nieh说，“这意味着云端软件对用户数据进行了正确管理，不会受到安全漏洞和黑客的威胁。”

构建安全的系统软件一直是计算机领域面临的重大挑战之一。形式验证专家Ronghui Gu加入了Nieh团队，他们决定合作探索软件系统的形式验证问题。他说：“验证一个多处理器商用系统，一种类似Linux这样被广泛应用的系统，被认为是不切实际的想法。”

云计算的指数级增长促使用户将数据和计算转移到云端虚拟机中。亚马逊等云计算供应商会部署管理程序来支持虚拟机。管理程序的正确性和可信度决定了虚拟机数据的安全性。管理程序非常重要，但又很复杂。代码中出现的任何薄弱环节，都可能受到黑客攻击。亚马逊等云供应商广泛采用了KVM管理程序。Nieh等证实，稍作改动的SeKVM是安全的，并且保证了虚拟计算机之间的隔离性。博士生Xupeng Li说：“我们证实，新系统能够为云端的私人数据和计算提供‘数学保证’。”

SeKVM使用MicroV（一种验证大型系统安全性的新框架）进行验证。这种新的分层技术对现有系统进行改进，并将强制安全性组件提取到一个经过验证的小核心内，从而确保了整个系统的安全性。研究人员表示，如果大型系统的小核心是完整的，那么系统就是安全的。Nieh说：“这就好比测试建筑物的安全性：石膏板出现了裂缝，并不意味着房子的完整性受到了威胁。它的结构仍然稳定，关键的结构体系也状态良好。”博士生Shih-Wei Li补充道：“SeKVM有望成为银行系统、物联网设备、自动驾驶汽车和加密货币的‘安保员’。”

作为第一款经过形式验证的商用管理程序，SeKVM有可能改变云服务的设计、开发、部署和信任方式。在网络安全问题愈演愈烈的背景下，这种弹性特征非常受欢迎。一些云计算公司已经开始探索，如何用SeKVM来满足这些客户需求。

编译：雷鑫宇

审稿：西莫 

责编：陈之涵

来源：IEEE安全与隐私研讨会

原文连接：

https://www.eurekalert.org/pub_releases/2021-05/cuso-cet052421.php

版权声明：本文由科界平台原创编译，中文内容仅供参考，一切内容以英文原版为准。

转载请注明来源科技工作者之家—科界App。

转载本公号内容请联系授权

[email protected]