復雜的hypervisor軟件有助于運行云計算機，但驗證其安全性通常被認為幾乎是不可能的。現在哥倫比亞大學的計算機科學家已經開發出他們所說的第一個可以保證安全云計算的管理程序。

每當您在Amazon購買商品時，您的客戶數據都會自動更新并存儲在云中的數千個虛擬機上。對于像Amazon這樣的企業，確保其數百萬客戶數據的安全性是至關重要的。大型和小型組織均是如此。但是到目前為止，還沒有辦法保證軟件系統不受錯誤，黑客和漏洞的影響。

哥倫比亞大學的工程與應用科學學院的計算機科學家、發表這項研究工作的合著者Ronghui Gu表示，希望為系統軟件驗證的未來創新奠定基礎，從而開發出新一代的彈性網絡安全系統軟件。

從理論上講，科學家可以正式驗證軟件，從數學上證明其代碼“在100%的情況下保護數據安全”，顧說。然而，大多數經過驗證的hypervisor通常比商業上的hypervisor簡單得多，因為它們是專門為驗證而設計的，而不是實際應用程序。相比之下，現代的商業hypervisor是一個龐大的軟件，通常包括一個完整的操作系統內核，這使得驗證它們看起來是一項無法克服的任務。

例如，用CertiKOS hypervisor驗證6500行代碼需要3個人年，用seL4 hypervisor驗證9000行代碼需要10個人年，這兩個都是為驗證而設計的。相比之下，廣泛使用的KVM開源hypervisor（與Linux集成的全功能多處理器系統）擁有超過200萬行代碼。

現在哥倫比亞大學的計算機科學家們已經開發出一種驗證商業級虛擬機監控程序的方法。他們使用新技術開發了一個名為SeKVM的KVM安全版本，他們認為這是第一個經過正式驗證的商用級hypervisor。

研究人員將他們的新技術稱為微驗證，它減少了驗證虛擬機監控程序所需的工作量。它將hypervisor分解為一個小的核心和一組不受信任的服務，然后通過單獨驗證核心來證明hypervisor的安全性。該內核沒有可供黑客攻擊的漏洞，并且該內核協調管理程序與虛擬機的所有交互，因此即使黑客攻擊破壞了一個虛擬機，也不會危害其他虛擬機。

基于微驗證，科學家們開發了名為MicroV的軟件來驗證大型商用級多處理器虛擬機監控程序。在MicroV的幫助下，他們為SeKVM開發了一個只有3800行代碼的安全內核，并在兩年的時間里進行了驗證。

當涉及到實際的應用程序工作負載時，SeKVM的性能與未修改的KVM類似，在KVM專門設計用于運行的本機硬件上最多只產生不到10%的性能開銷。同時，SeKVM支持KVM的廣泛特性。

“SeKVM只是一些微小的變化，”研究合著者Jason Nieh說，他是哥倫比亞大學工程與應用科學學院的計算機科學家。它的性能類似于常規KVM，繼承了常規KVM的功能，但除此之外，它還提供了常規KVM所沒有的安全保證。”

未來，“我們將繼續探索這種網絡彈性系統軟件的概念，并在各個領域建立安全保障，從銀行系統和物聯網設備到自動車輛和加密貨幣，”Gu說，“SeKVM將為未來的系統驗證創新奠定基礎，并引領新一代的網絡彈性系統軟件。在一個網絡安全日益受到關注的世界里，這種彈性需求很高。”

科學家們在2021年5月26日舉行的第42屆IEEE安全與隱私研討會上發表的一篇新論文中詳細介紹了他們的發現。

責任編輯：haq