本文關(guān)鍵詞：基于模型檢測(cè)的Hyper-V虛擬機(jī)監(jiān)控器的安全性分析　出處：《西安電子科技大學(xué)》2015年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 虛擬機(jī)監(jiān)控器 安全性 模型檢測(cè) 形式化分析

【摘要】：在不久的未來,云計(jì)算很快就會(huì)席卷IT領(lǐng)域,而虛擬機(jī)監(jiān)控器是所有虛擬化技術(shù)活的核心。云計(jì)算本質(zhì)的復(fù)雜性和動(dòng)態(tài)性使得傳統(tǒng)的、以及基于虛擬化的防御技術(shù)很難達(dá)到有效的防御效果。為了保證云計(jì)算的安全,分析虛擬機(jī)監(jiān)控器自身的安全性、找出軟件本身存在漏洞是解決其安全問題的根本辦法。為了盡量多的找出虛擬機(jī)監(jiān)控器存在的安全漏洞,對(duì)系統(tǒng)脆弱性的分析應(yīng)在各個(gè)抽象層次上進(jìn)行。所以,我們可以使用形式化分析方法中的模型檢測(cè)理論進(jìn)行漏洞挖掘。利用現(xiàn)有的形式化代碼分析技術(shù)來分析虛擬機(jī)監(jiān)控器的脆弱性時(shí)主要存在以下問題：1.只證明了代碼的正確性,而不能證明安全性,如在已知Hyper-V源碼的基礎(chǔ)上利用模型檢測(cè)方法驗(yàn)證其正確性的工具VCC。一些針對(duì)代碼層的可信靜態(tài)分析工具可以檢驗(yàn)數(shù)據(jù)結(jié)構(gòu)行為和同步問題等,但是在進(jìn)行檢測(cè)時(shí)沒有考慮軟件的安全性。2.只針對(duì)開源的虛擬機(jī)監(jiān)控器。一些研究方法試圖形式化的捕獲代碼意圖,并將安全性考慮在內(nèi),但是這種方法對(duì)于不開源的軟件比如微軟的虛擬機(jī)監(jiān)控器Hyper-V是不可行的。本文使用模型檢測(cè)的方法來進(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í)和分類,定義不同主體的可執(zhí)行指令,構(gòu)建了CPU簡(jiǎn)單的三個(gè)狀態(tài)的狀態(tài)轉(zhuǎn)移圖。2.構(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í),并為不同的主體定義不同的內(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安全參考模型。對(duì)于DoS攻擊,根據(jù)Hyper-V的架構(gòu)以及調(diào)度機(jī)制的特點(diǎn)構(gòu)建針對(duì)多任務(wù)的CPU安全參考模型。該模型可以用來抽象超級(jí)調(diào)用的相關(guān)代碼,減少代碼分析的工作量。針對(duì)CPU的安全參考模型、內(nèi)存的安全參考模型以及多任務(wù)的CPU的安全參考模型為進(jìn)一步檢測(cè)Hyper-V代碼的安全性奠定了基礎(chǔ)。
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP302;TP309

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 曹曉剛;;Java虛擬機(jī)的10年[J];程序員;2005年07期

2 宋韜;盤細(xì)平;羅元柯;倪國(guó)軍;;Java虛擬機(jī)在嵌入式DSP系統(tǒng)上的實(shí)現(xiàn)[J];計(jì)算機(jī)應(yīng)用與軟件;2007年04期

3 劉黎波;;Java虛擬機(jī)攔截原理研究[J];科技風(fēng);2008年21期

4 劉治波;;Java虛擬機(jī)簡(jiǎn)析[J];濟(jì)南職業(yè)學(xué)院學(xué)報(bào);2008年01期

5 郝帥;;Java虛擬機(jī)中相關(guān)技術(shù)的探討[J];成功(教育);2008年08期

6 李霞;;系統(tǒng)虛擬機(jī)關(guān)鍵技術(shù)研究[J];微型電腦應(yīng)用;2010年03期

7 鄭曉瓏;孔挺;;虛擬機(jī)的安全風(fēng)險(xiǎn)與管理[J];硅谷;2010年16期

8 李學(xué)昌;平淡;;為速度而戰(zhàn),虛擬機(jī)內(nèi)外兼修[J];電腦愛好者;2010年18期

9 王惠萍;張海龍;馮帆;王建華;;Java虛擬機(jī)使用及優(yōu)化[J];計(jì)算機(jī)與網(wǎng)絡(luò);2010年21期

10 鄭婷婷;武延軍;賀也平;;云計(jì)算環(huán)境下的虛擬機(jī)快速克隆技術(shù)[J];計(jì)算機(jī)工程與應(yīng)用;2011年13期

相關(guān)會(huì)議論文 前10條

1 孟廣平;;虛擬機(jī)漂移網(wǎng)絡(luò)連接方法探討[A];中國(guó)計(jì)量協(xié)會(huì)冶金分會(huì)2011年會(huì)論文集[C];2011年

2 段翼真;王曉程;;可信安全虛擬機(jī)平臺(tái)的研究[A];第26次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2011年

3 李明宇;張倩;呂品;;網(wǎng)絡(luò)流量感知的虛擬機(jī)高可用動(dòng)態(tài)部署研究[A];2014第二屆中國(guó)指揮控制大會(huì)論文集（上）[C];2014年

4 林紅;;Java虛擬機(jī)面向數(shù)字媒體的應(yīng)用研究[A];計(jì)算機(jī)技術(shù)與應(yīng)用進(jìn)展——全國(guó)第17屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用（CACIS）學(xué)術(shù)會(huì)議論文集（上冊(cè)）[C];2006年

5 楊旭;彭一明;刑承杰;李若淼;;基于VMware vSphere 5虛擬機(jī)的備份系統(tǒng)實(shí)現(xiàn)[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十二次學(xué)術(shù)年會(huì)論文集[C];2014年

6 沈敏虎;查德平;劉百祥;趙澤宇;;虛擬機(jī)網(wǎng)絡(luò)部署與管理研究[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十次學(xué)術(shù)年會(huì)論文集[C];2010年

7 李英壯;廖培騰;孫夢(mèng);李先毅;;基于云計(jì)算的數(shù)據(jù)中心虛擬機(jī)管理平臺(tái)的設(shè)計(jì)[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十次學(xué)術(shù)年會(huì)論文集[C];2010年

8 朱欣焰;蘇科華;毛繼國(guó);龔健雅;;GIS符號(hào)虛擬機(jī)及實(shí)現(xiàn)方法研究[A];《測(cè)繪通報(bào)》測(cè)繪科學(xué)前沿技術(shù)論壇摘要集[C];2008年

9 于洋;陳曉東;俞承芳;李旦;;基于FPGA平臺(tái)的虛擬機(jī)建模與仿真[A];2007'儀表，，自動(dòng)化及先進(jìn)集成技術(shù)大會(huì)論文集（一）[C];2007年

10 丁濤;郝沁汾;張冰;;內(nèi)核虛擬機(jī)調(diào)度策略的研究與分析[A];'2010系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2010年

相關(guān)重要報(bào)紙文章 前10條

1 ;虛擬機(jī)的生與死[N];網(wǎng)絡(luò)世界;2008年

2 本報(bào)記者 卜娜;高性能Java虛擬機(jī)將在中國(guó)云市場(chǎng)釋能[N];中國(guó)計(jì)算機(jī)報(bào);2012年

3 本報(bào)記者 邱燕娜;如何告別虛擬機(jī)管理煩惱[N];中國(guó)計(jì)算機(jī)報(bào);2012年

4 ;首批通過云計(jì)算產(chǎn)品虛擬機(jī)管理測(cè)評(píng)名單[N];中國(guó)電子報(bào);2014年

5 申琳;虛擬機(jī)泛濫 系統(tǒng)安全怎么辦[N];中國(guó)計(jì)算機(jī)報(bào);2008年

6 Tom Henderson邋沈建苗 編譯;虛擬機(jī)管理的五大問題[N];計(jì)算機(jī)世界;2008年

7 盆盆;真實(shí)的虛擬機(jī)[N];中國(guó)電腦教育報(bào);2004年

8 本版編輯　綜合 編譯整理 田夢(mèng);管理好虛擬機(jī)的全生命周期[N];計(jì)算機(jī)世界;2008年

9 李婷;中國(guó)研制出全球最快反病毒虛擬機(jī)[N];人民郵電;2009年

10 張弛;虛擬機(jī)遷移走向真正自由[N];網(wǎng)絡(luò)世界;2010年

相關(guān)博士學(xué)位論文 前10條

1 宋翔;多核虛擬環(huán)境的性能及可伸縮性研究[D];復(fù)旦大學(xué);2014年

2 王桂平;云環(huán)境下面向可信的虛擬機(jī)異常檢測(cè)關(guān)鍵技術(shù)研究[D];重慶大學(xué);2015年

3 周真;云平臺(tái)下運(yùn)行環(huán)境感知的虛擬機(jī)異常檢測(cè)策略及算法研究[D];重慶大學(xué);2015年

4 郭芬;面向虛擬機(jī)的云平臺(tái)資源部署與調(diào)度研究[D];華南理工大學(xué);2015年

5 周傲;高可靠云服務(wù)供應(yīng)關(guān)鍵技術(shù)研究[D];北京郵電大學(xué);2015年

6 陳彬;分布環(huán)境下虛擬機(jī)按需部署關(guān)鍵技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2010年

7 劉海坤;虛擬機(jī)在線遷移性能優(yōu)化關(guān)鍵技術(shù)研究[D];華中科技大學(xué);2012年

8 劉謙;面向云計(jì)算的虛擬機(jī)系統(tǒng)安全研究[D];上海交通大學(xué);2012年

9 趙佳;虛擬機(jī)動(dòng)態(tài)遷移的關(guān)鍵問題研究[D];吉林大學(xué);2013年

10 鄧?yán)?基于虛擬機(jī)遷移的動(dòng)態(tài)資源配置研究[D];華中科技大學(xué);2013年

相關(guān)碩士學(xué)位論文 前10條

1 潘飛;負(fù)載相關(guān)的虛擬機(jī)放置策略研究[D];杭州電子科技大學(xué);2011年

2 王建一;混合型桌面云高可用性研究與實(shí)現(xiàn)[D];華南理工大學(xué);2015年

3 周衡;云計(jì)算環(huán)境下虛擬機(jī)優(yōu)化調(diào)度策略研究[D];河北大學(xué);2015年

4 羅仲皓;基于OpenStack的私有云計(jì)算平臺(tái)的設(shè)計(jì)與實(shí)現(xiàn)[D];華南理工大學(xué);2015年

5 李子堂;面向負(fù)載均衡的虛擬機(jī)動(dòng)態(tài)遷移優(yōu)化研究[D];遼寧大學(xué);2015年

6 張煜;基于OpenStack的“實(shí)驗(yàn)云”平臺(tái)的研究與開發(fā)[D];西南交通大學(xué);2015年

7 曾文琦;面向應(yīng)用服務(wù)的云規(guī)模虛似機(jī)性能監(jiān)控與負(fù)載分析技術(shù)研究[D];復(fù)旦大學(xué);2013年

8 施繼成;面向多核處理器的虛擬機(jī)性能優(yōu)化[D];復(fù)旦大學(xué);2014年

9 游井輝;基于虛擬機(jī)動(dòng)態(tài)遷移的資源調(diào)度策略研究[D];華南理工大學(xué);2015年

10 方良英;云平臺(tái)的資源優(yōu)化管理研究與實(shí)現(xiàn)[D];南京師范大學(xué);2015年

本文編號(hào)：1324185