基于模型檢測的HypeR-V虛擬機監(jiān)控器的安全性分析.pdf

1、在不久的未來，云計算很快就會席卷IT領(lǐng)域，而虛擬機監(jiān)控器是所有虛擬化技術(shù)活的核心。云計算本質(zhì)的復雜性和動態(tài)性使得傳統(tǒng)的、以及基于虛擬化的防御技術(shù)很難達到有效的防御效果。為了保證云計算的安全，分析虛擬機監(jiān)控器自身的安全性、找出軟件本身存在漏洞是解決其安全問題的根本辦法。
　　為了盡量多的找出虛擬機監(jiān)控器存在的安全漏洞，對系統(tǒng)脆弱性的分析應(yīng)在各個抽象層次上進行。所以，我們可以使用形式化分析方法中的模型檢測理論進行漏洞挖掘。利用現(xiàn)有的形

2、式化代碼分析技術(shù)來分析虛擬機監(jiān)控器的脆弱性時主要存在以下問題:
　　1.只證明了代碼的正確性，而不能證明安全性，如在己知Hyper-V源碼的基礎(chǔ)上利用模型檢測方法驗證其正確性的工具VCC。一些針對代碼層的可信靜態(tài)分析工具可以檢驗數(shù)據(jù)結(jié)構(gòu)行為和同步問題等，但是在進行檢測時沒有考慮軟件的安全性。
　　2.只針對開源的虛擬機監(jiān)控器。一些研究方法試圖形式化的捕獲代碼意圖，并將安全性考慮在內(nèi)，但是這種方法對于不開源的軟件比如微軟的虛擬

3、機監(jiān)控器Hyper-V是不可行的。
　　本文使用模型檢測的方法來進行基于Hyper-V的虛擬機監(jiān)控器的漏洞分析。本研究遵循的流程是:抽象-建模-描述-驗證。主要工作如下:
　　1.分析了Hyper-V的基本架構(gòu)。本文詳細研究了微軟的虛擬化技術(shù)及其架構(gòu)，分析了Hyper-V的安全特性。將敏感指令、特權(quán)指令、CPU的狀態(tài)及狀態(tài)轉(zhuǎn)移進行了分級和分類，定義不同主體的可執(zhí)行指令，構(gòu)建了CPU簡單的三個狀態(tài)的狀態(tài)轉(zhuǎn)移圖。
　　2.

4、構(gòu)建Hyper-V CPU的安全參考模型。形式化的定義了Hyper-V的各個主體，使用Promela和SPIN得到了CPU狀態(tài)的有限狀態(tài)模型，有限狀態(tài)模型包括的主體有VMM，VMPP以及兩個VMCP等。在有限狀態(tài)模型的基礎(chǔ)上，結(jié)合用LTL所定義的安全斷言，構(gòu)建了Hyper-V CPU的安全參考模型。
　　3.構(gòu)建Hyper-V內(nèi)存的安全參考模型。描述了虛擬內(nèi)存到物理內(nèi)存的映射及其關(guān)系，將物理內(nèi)存劃分為三個不同的等級，并為不同的主體

5、定義不同的內(nèi)存訪問權(quán)限。根據(jù)主體的形式化定義以及有限狀態(tài)模型，從主體中抽象出相關(guān)內(nèi)存的屬性。形式化的描述主體，并建造內(nèi)存的有限狀態(tài)模型。最終根據(jù)內(nèi)存的轉(zhuǎn)移規(guī)則以及內(nèi)存狀態(tài)的有限狀態(tài)模型，利用SPIN得到內(nèi)存訪問的安全參考模型。
　　4.構(gòu)建多任務(wù)的CPU安全參考模型。對于DoS攻擊，根據(jù)Hyper-V的架構(gòu)以及調(diào)度機制的特點構(gòu)建針對多任務(wù)的CPU安全參考模型。該模型可以用來抽象超級調(diào)用的相關(guān)代碼，減少代碼分析的工作量。