【文獻心得】Hypervisor 技術、安全

[1]肖偉民,鄧浩江,孫鵬.嵌入式虛拟化技術研究綜述[J].網絡新媒體技術,2019,8(02):9-18.

​​https://www.jianshu.com/p/d808b8e6c917​​

計算機系統包括五個抽象層：硬體抽象層，指令集架構層，作業系統層，庫函數層和應用程式層。虛拟化可以在每個抽象層來實作。

在系統虛拟化中，虛拟機（VM）是在一個硬體平台上模拟一個或者多個獨立的和實際底層硬體相同的執行環境。

虛拟化技術是将計算機的各種實體資源，予以抽象、轉換後建立某種特定虛拟對象的做法，包括虛拟的計算機硬體平台、儲存設備和計算機網絡資源等，該技術通過在軟體和硬體中間引進一個新的虛拟化層，将主控端的各種資源進行邏輯的抽象轉換，實作了軟硬體分離。使用者無需關注硬體的具體實作即可在虛拟化的作業系統環境中運作應用程式，提高了資源的使用率和安全性。

虛拟化技術的發展階段：

1. 硬體仿真技術。在主控端作業系統上建立一個硬體VM來仿真所想要的硬體。采用該技術，甚至可以運作多個虛拟機，每個虛拟器仿真一個不同架構的處理器。WindRiver Simics、QEMU、Bochs。
2. 完全虛拟化技術。不對底層硬體資源進行劃分分區，通過 Host 系統進行虛拟化，通過VMM來管控虛拟機。典型代表有 VirtualBox，Virtual Iron，IBM z/VM，Virtual PC，Hyper-V，VMware Workstation，VMware Server (formerly GSX Server)，Adeos，Mac-on-Linux以及Egenera vBlade technology等。為使用者提供了完整的互相獨立的虛拟化硬體資源，缺點是：VMM 需要消耗大量資源，實體主機開銷大。
3. 半虛拟化技術。是指通過暴露給Guest OS一個修改過的硬體抽象，将硬體接口以軟體的形式提供給客戶機作業系統。這可以通過Hypercall（VMM提供給GuestOS的直接調用，與系統調用類似）的方式來提供。能夠改善虛拟化的性能，通過定制的虛拟機作業系統使得其可以與 VMM 通信，協同工作，并對指令進行了優化，典型代表為早期的 XEN。并且半虛拟化技術修改了Guest OS與虛拟機監控器協同工作，使得虛拟機監控器可以得知Guest OS内部的一些狀态，消除了黑盒排程帶來的一些問題。優點是：提高了虛拟化的性能和系統效率，缺點是：由于其需要對虛拟機作業系統進行修改，增加了系統設計複雜性。
4. 硬體輔助虛拟化技術。硬體輔助虛拟化技術是指借助硬體（CPU、晶片組以及I/O裝置等）的虛拟化支援來實作高效的全虛拟化。原有的硬體體系結構在虛拟化方面存在虛拟化漏洞等缺陷，導緻單純的軟體虛拟化方法存在一些問題；還有就是由于硬體架構的限制，某些功能即使可以通過軟體的方式來實作，但是實作過程卻異常複雜，甚至帶來性能的大幅下降，這主要展現在以軟體方式實作的記憶體虛拟化和I/O裝置虛拟化。通過在硬體中加入專門針對虛拟化的支援，系統虛拟化的實作變得更加容易和高效。例如，在Intel VT技術的支援下，Guest OS和VMM的執行環境可以自動地完全隔離開來，Guest OS有自己的“全套寄存器”，可以直接運作在最進階别。采用該技術的虛拟化平台有Linux KVM， VMware Workstation， VMware Fusion， Microsoft Virtual PC， Xen， Parallels Desktop for Mac，VirtualBox and Parallels Workstation。

5. 不在硬體平台，而是在作業系統層進行虛拟化 —— 作業系統虛拟化。所有虛拟機共享同一個作業系統執行個體，涉及輕量級虛拟化技術和容器化技術，OpenVZ、Sun Solaris Container 和 Linux 核心容器（LXC，通過控制組實作基于程序組的資源隔離，采用命名空間就為每個容器提供特定的命名空間，實作程序級别的隔離）等。

   1、所有容器共享同一作業系統核心，資源浪費和性能損耗較小；

   2、容器可根據需要擷取資源，不會造成資源浪費；

   3、不需要作業系統和硬體資源間的指令集模拟和轉換，提高系統性能；

   4、LXC 的特性由 Linux 核心提供，帶來更小的虛拟化開銷；

   5、LXC 提供管理工具，可以快速部署；

嵌入式虛拟化技術。是指通過在嵌入式系統部署虛拟機或容器監控程式，使得嵌入式系統硬體上能夠支援多種類型的、互相隔離的客戶作業系統。方案：開源社群 Open Kernel Lab 提出的 OKL4 Microvisor（半虛拟化）、NOVA（全面虛拟化）、Codezero、XEN on ARM（全虛拟化、半虛拟化）、KVM for ARM（全虛拟化、半虛拟化）、Xvisor（全虛拟化、半虛拟化）。

嵌入式Docker容器技術

Docker 擴充了 LXC 和應用層的接口，使程序隔離運作，隔離的程序資源包括 CPU、記憶體、I/O、網絡等；通過采用命名空間實作底層操作環境的徹底隔離，包括程序樹、網絡、使用者ID 和檔案系統；具備鏡像的自動化建構與便捷快速部署元件複用、容器共享、類似 git 的版本控制。

嵌入式 Docker 容器技術作為嵌入式虛拟化技術的典型代表，解決方案：RancherOS、HypriotOS、ResinOS。

以 Docker 容器技術為代表的輕量級虛拟化技術能夠有效緩解嵌入式虛拟化給系統帶來的性能下降、資源使用率低、額外開銷大等問題。Docker 容器技術在應用的快速部署、容器數量及并發性方面更具有優勢。通過鏡像複用，Docker 容器可以共用作業系統和應用程式元件，極大的減輕系統負載，提高資源使用率。是以，基于 Docker 容器技術的輕量級虛拟化技術更适合嵌入式系統虛拟化。

Hypervisor types

Hypervisor types

• VMM 直接運作在沒有作業系統的裸機上，具有最高特權級，管理底層所有的硬體資源。所有的Guest OS都運作在較低的特權級中，所有Guest OS對底層資源的通路都被虛拟機監控器攔截，由虛拟機監控器代為操作并傳回操作結果，進而實作系統的隔離性，達到對系統資源絕對控制。
• 虛拟機監控器作為一個應用程式運作在主控端作業系統（Host OS）上，而Guest OS運作于虛拟機監控器之上。Guest OS對底層硬體資源的通路要被虛拟機監控器攔截，虛拟機監控器再轉交給Host OS進行處理。

• Type 1: Hyper-V，VMware ESX Server，Citrix XenServer，Oracle OVM for SPARC，KVM；
• Type 2: VMware Server，VMware Fusion，Microsoft Virtual Server，Oracle VM Virtual Box，Oracle VM for x86， Solaris Zones，Parallels，Microsoft Virtual PC。

[1]祝現威. Xen安全模型設計與形式化驗證方法研究[D].解放軍資訊工程大學,2017.

Xen 虛拟化技術将關鍵性硬體的控制權，從原有運作在硬體上的作業系統轉移到了虛拟機螢幕層，Xen 中的安全機制大多是通過在 VMM 中添加安全子產品來實作對平台和資料的安全保護。

Xen 的安全架構 XSM 參考了 Linux 作業系統中的安全架構 LSM，為實作 Xen 上虛拟機及其資源的排程和通路控制提供的一個安全架構，目前 XSM 支援的安全架構有 Dummy、ACM 和 Flask 三種。Dummy 是強隔離機制，使虛拟機間不産生資訊流動，ACM 和 Flask 是通過安全政策限制具有沖突關系的虛拟機間的資訊流動。

XSM 是通過在 Xen 中加入鈎子實作的，XSM 在 Xen 中定義了幾組函數指針，每組函數指針的集合稱為 Hook，實作原理是 XSM 将所要執行的鈎子函數放在其對應的敏感操作之前，實作 XSM 的安全政策。

1. ACM 安全架構

   又稱為 sHype，是一個為解決 Xen 虛拟機多使用者間的沖突而設計的一個沖突模型，其實作原理類似于容器，将互相沖突的虛拟機劃分為同一集合。解決了不同虛拟機間的通路沖突問題，并且部分實作了虛拟機間的機密性，但是其安全政策的靈活性較低無法适應多種安全通路方式，并且通路方式限制的過為嚴格，甚至會影響系統的正常運作。

1. STE 模型（Simple Type Enforcement）

   主要對象為虛拟機及虛拟機所對應的資源。

2. CW 模型（Chinese Wall）

   制定了一組安全政策來定義和限制主體對客體的通路，要求主體不能通路同一沖突集中的客體。CW 通過定義的沖突集判斷不同虛拟機是否能夠在同一主機上運作。當建立一個新的虛拟機時，首先查找其所在的沖突集，在該沖突集中判斷是否有虛拟機在運作，如果在同一沖突集中存在運作的虛拟機則該虛拟機不允許建立，否則

   允許建立。

1. Flask 安全架構

   Xen 将 Flask 體系結構從 SELinux 移植到了 XSM 中，它将政策執行和政策判斷分開，具有很強的靈活性和擴充性。Flask 由客體管理器和安全伺服器組成，客體管理器主要有安全政策執行和主客體标簽配置設定兩個功能，安全伺服器對主體通路行為進行判斷并給出通路政策。主體通路客體時客體管理器将主客體的安全辨別發送給安全伺服器，安全伺服器查找到安全政策，并傳回給客體管理器執行。

2. Xen 的增強安全架構 Xenon

   核心隔離實作虛拟機間隔離。MLS 安全模型。

3. 基于 Xen 的 BLP 模型

   當一個虛拟機通路另一個虛拟機時，通過在 VMM 的路徑代碼處插入鈎子函數，鈎子函數通路 Police Manager 判斷該通路行為能否執行。

傳統作業系統安全标準，使用經過形式化證明的可信的開發環境和流程，并提供可證明安全模型來達到其标準所聲稱的安全等級：

• 形式化評估标準：（TCSEC）《可信計算機系統評價标準》。提出安全功能和安全确信度兩個概念。
• 面向标準開發的安全标準：計算機安全評價标準聯邦标準。
• 面向工程實踐的安全标準：資訊安全評價國際通用标準。
• 作業系統安全評估标準 GB-17859、GB/T18336。

形式化驗證：

形式化方法是指基于數理邏輯和邏輯語言來描述和驗證軟體和硬體的方法。利用形式化方法對目标系統及其模型進行驗證，主要通過數學模組化來描述目标系統的行為和語義，建立形式化模型，驗證其實作特定的功能和滿足安全要求。提供了一種數學評估的手段，是他們能夠嚴格的刻畫系統，被廣泛的應用于系統安全評價标準中。

對于安全模型來說，主要的形式化驗證手段是模型檢測和演繹證明。

• 模型檢測是利用系統問題建立數學模型，對系統的狀态空間進行周遊，以判定規範的真假，其證明過程可以自動化證明。但是由于是對系統的狀态空間進行周遊，要防止狀态空間膨脹，模型檢測隻能應用于有限狀态的并行系統中。
• 演繹證明一般采用互動式的定理輔助證明器對系統進行抽象描述，依賴系統的定理和公理來表達系統功能和安全性。

1. 提出系統模組化架構，對目标模型進行描述；
2. 選擇對驗證安全模型的性質進行描述的規範語言；
3. 對系統性質的描述是否滿足規範驗證進行确認；

存在問題：

1. 傳統作業系統的安全标準在結構和内容上與雲計算安全标準有許多共通點，但由于雲計算多使用者、可遷移等特性使其與傳統安全标準有許多不同，如何面對這種既有一緻性又有差別的兩種系統安全标準，也是開發人員要面對的重要問題。
2. 現階段安全模型都是以虛拟機作為元機關，沒有實作虛拟機的細粒度管理，違反最小特權原則。對安全模型的形式化是保證安全模型一緻性的基礎工作，安全模型形式化不僅要求開發人員具有深刻的模型設計理論，還要擁有堅實的數理邏輯功底。在形式化方面安全模型的形式化工作還是一個較為艱巨的工作。
3. 形式化方法可以最大程度的保證安全架構的正确性和一緻性。由于子產品化形式化模組化方法的缺乏和開發效率的考慮，開發人員往往對安全模型和安全架構實行一體化證明，但是在實際應用中由于抽象層次、複雜性和規模上以及程式設計邏輯和應用邏輯的不同而導緻安全模型和安全架構無法進行統一的模組化。

[1]陳劍鋒,王強,王劍鋒.雲計算虛拟環境的形式化安全驗證[J].資訊安全與通信保密,2012(04):64-66.

==目前針對雲計算虛拟環境多采用傳統的覆寫使驗證方法，無法徹底解決正确性問題。==形式化方法的基本含義是借助數學的方法來研究計算機與數學科學問題，在系統建構、實作的全過程中，凡是采用嚴格的數學語音，具有精确的數學語義的方法，都可以稱之為形式化方法。

模型檢測技術：

• 1、配置采集。元素集合、謂詞邏輯的執行個體化過程。
• 2、需求分析。得到形式化語言刻畫的安全性質語句，一般也用邏輯命題的形式表述。
• 3、性質檢測。檢測器将算法選項參數初始化，并輸入待檢測的語句作為未知命題進行演算，窮舉模型空間裡的謂詞和給定事實，尋找能夠比對的規則，将命題進一步分解，直到能夠成功求值并傳回演算結果，整個計算過程在周遊了整棵演算樹後結束，根據獲得的中間結果組合成最終傳回值，給出是、否、系統異常三個結論。

[1]錢漢偉,王承毅.作業系統形式化驗證綜述[J/OL].河海大學學報(自然科學版):1-10[2021-07-28].http://kns.cnki.net/kcms/detail/32.1117.TV.20201218.1650.012.html.

支撐理論和架構：目前作業系統的形式化驗證是用定理證明的方法對作業系統的性質規約進行驗證。性質規約描述的邏輯基礎是霍爾邏輯，并以此為基礎進行擴充的分離邏輯、并發分離邏輯和并發精化程式邏輯。

• 霍爾邏輯。證明規約用形如​

  ​{Pre}P{Post}​

  ​ 的霍爾三元組表示，通過前置後置條件，比如某些不變量，放入程式要證明的性質，實作了用一組公理和一組規則描述程式代碼應有的性質。
• 分離邏輯。對霍爾邏輯進行擴充，增加了分離合取和分離蘊含謂詞及相應的推導規則，能夠以自然的方式來描述計算過程中記憶體的屬性和相關操作，驗證指針程式也更加友善。
• 并發精化程式邏輯。将并發分離邏輯的斷言語言擴充為關系型斷言，更适合證明與多級中斷有關的并發程式的上下文精化關系。作業系統驗證問題也是精化驗證問題，作業系統從底層模型到高層規約之間的一緻性驗證等問題都是以精化理論為基礎。

形式化驗證工具。 ==作業系統的驗證問題都将轉成定理證明問題，解決定理證明問題最終依賴于定理證明器。==目前廣泛應用于作業系統驗證的定理證明器有 Z3、Isabelle、Coq。可信編譯器有 CompCert C，它嚴格保證了源代碼和編譯之後機器碼之間的語義一緻性，使得在源碼層驗證的定理很容易擴充到機器碼層。如果驗證用了 C 語言編寫的作業系統源代碼，通過可行編譯器生成的相應機器碼也可以被認為是通過驗證了。選用微核心作業系統作為驗證對象是減少驗證規模的一個重要方法，目前作業系統驗證工作取得一定成果的 seL4、mC2、PikeOS、uC/OS-Ⅱ。

現狀。Verve 微軟基于類型化彙編語言和霍爾邏輯，第一個證明了類型安全和記憶體安全作業系統。PikeOS、SeL4、CertiKOS、uC/OS-Ⅱ（僅證明了該系統互斥鎖不會發生優先級反轉，一共驗證了1400行左右的C代碼，證明器驗證腳本量 225000 行）。

1. 作業系統過于複雜。
2. 驗證成本高。驗證 1 行 C 代碼平均需要 25 行左右的證明代碼，以μC/OS-II 系統核心的驗證為例，1400 行 C 代碼用了 22 萬行 Coq 腳本代碼，其中包括驗證架構約 6 萬行，證明庫約 11 萬行，代碼證明約 4 萬行，證明政策約 1.5 萬行，共約 6 人年的工作量。
3. 專業人員少。形式化驗證工作全部依賴于非常專業的人員，除了需要具有深厚的形式化理論功底，豐富的證明工具使用經驗，還要對驗證的軟體有深刻的了解，過高的門檻使得這樣的專業人員非常稀缺。