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

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

哥倫比亞大學的工程與應(yīng)用科學學院的計算機科學家、發(fā)表這項研究工作的合著者Ronghui Gu表示，希望為系統(tǒng)軟件驗證的未來創(chuàng)新奠定基礎(chǔ)，從而開發(fā)出新一代的彈性網(wǎng)絡(luò)安全系統(tǒng)軟件。

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

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

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

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

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

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

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

未來，“我們將繼續(xù)探索這種網(wǎng)絡(luò)彈性系統(tǒng)軟件的概念，并在各個領(lǐng)域建立安全保障，從銀行系統(tǒng)和物聯(lián)網(wǎng)設(shè)備到自動車輛和加密貨幣，”Gu說，“SeKVM將為未來的系統(tǒng)驗證創(chuàng)新奠定基礎(chǔ)，并引領(lǐng)新一代的網(wǎng)絡(luò)彈性系統(tǒng)軟件。在一個網(wǎng)絡(luò)安全日益受到關(guān)注的世界里，這種彈性需求很高。”

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

責任編輯：haq