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

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

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

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