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

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

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

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

4、構(gòu)建Hyper-V CPU的安全參考模型。形式化的定義了Hyper-V的各個(gè)主體，使用Promela和SPIN得到了CPU狀態(tài)的有限狀態(tài)模型，有限狀態(tài)模型包括的主體有VMM，VMPP以及兩個(gè)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)存劃分為三個(gè)不同的等級(jí)，并為不同的主體

5、定義不同的內(nèi)存訪(fǎng)問(wèn)權(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)存訪(fǎng)問(wèn)的安全參考模型。
　　4.構(gòu)建多任務(wù)的CPU安全參考模型。對(duì)于DoS攻擊，根據(jù)Hyper-V的架構(gòu)以及調(diào)度機(jī)制的特點(diǎn)構(gòu)建針對(duì)多任務(wù)的CPU安全參考模型。該模型可以用來(lái)抽象超級(jí)調(diào)用的相關(guān)代碼，減少代碼分析的工作量。