基于模型檢測的Hypervisor脆弱性分析方法研究.pdf

1、著云計(jì)算技術(shù)的廣泛應(yīng)用,作為底層的Hypervisor(虛擬機(jī)監(jiān)控器)的安全性也越來越重要。Hypervisor通過對硬件資源的抽象,為客戶機(jī)操作系統(tǒng)呈現(xiàn)和物理硬件相同或相近的硬件抽象層,使多個(gè)操作系統(tǒng)能共享硬件資源,但又擁有獨(dú)立的運(yùn)行環(huán)境。由于Hypervisor的基礎(chǔ)性作用,使得 Hypervisor 自身存在的脆弱性可能會(huì)被攻擊者利用對整個(gè)虛擬化平臺(tái)造成更嚴(yán)重的危害,如何對Hypervisor進(jìn)行脆弱性分析,確保虛擬化的安全性也成

2、為一個(gè)研究熱點(diǎn)。
　　由于Hypervisor的關(guān)鍵性以及高可靠性和高安全性的需求,一般采取更嚴(yán)謹(jǐn)?shù)男问交治龇椒ā，F(xiàn)有的對Hypervisor的分析方法主要分為以下兩類:對Hypervisor 源代碼的正確性分析,如檢驗(yàn)是否存在內(nèi)存溢出、數(shù)據(jù)結(jié)構(gòu)操作是否規(guī)范等。 重點(diǎn)分析 Hypervisor 中某部分功能的安全性,如影子頁表算法、Hypercall機(jī)制等。 這些分析都只是涉及Hypervisor某些功能模塊低層次的安全屬性分析

3、,然而針對一些高層次的安全屬性分析如虛擬機(jī)的隔離性、虛擬機(jī)運(yùn)行權(quán)限等,不僅涉及Hypervisor中多個(gè)模塊的功能組合,同時(shí)也涉及Hypervisor,特權(quán)虛擬機(jī)和普通虛擬機(jī)三者之間的交互。
　　本文以對Hypervisor進(jìn)行脆弱性分析為目的,以模型檢測方法為基礎(chǔ),首先提出了一種適用于Hypervisor的脆弱性分析框架,框架融合了高低兩個(gè)層次的安全屬性分析,闡述了如何利用模型檢測方法在對安全屬性的驗(yàn)證中發(fā)現(xiàn)系統(tǒng)的脆弱性;然后針