云管理程序的微管理。
客户在亚马逊商城购物时，其数据会自动更新并被存储到“云”的虚拟机中。对付亚马逊这种级别的企业来说，确保数百万客户的数据安全至关主要。然而，网络工程师们目前还无法确保软件系统的绝对安全。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
中文内容仅供参考，统统内容以英文原版为准。转载请注明来源。
