一種可信虛擬機遷移模型構建方法

石 源 張煥國 吳福生

(武漢大學計算機學院 武漢 430072) (空天信息安全與可信計算教育部重點實驗室(武漢大學) 武漢 430072) (yuanshi@whu.edu.cn)

2017-06-11；

2017-07-31

國家自然科學基金項目(61332019)；國家“九七三”重點基礎研究發展計劃基金項目(2014CB340601)；國家“八六三”高技術研究發展計劃基金項目(2015AA016002) This work was supported by the National Natural Science Foundation of China (61332019), the National Basic Research Program of China (973 Program) (2014CB340601), and the National High Technology Research and Development Program of China (863 Program) (2015AA016002).

張煥國(liss@whu.edu.cn)

一種可信虛擬機遷移模型構建方法

石 源 張煥國 吳福生

(武漢大學計算機學院 武漢 430072) (空天信息安全與可信計算教育部重點實驗室(武漢大學) 武漢 430072) (yuanshi@whu.edu.cn)

虛擬機的安全遷移是保障云環境安全可信的重要需求之一.對于包含虛擬可信平臺模塊(virtual TPM, vTPM)的可信虛擬機，還需要考慮vTPM的安全遷移問題.目前，已有一些針對可信虛擬機的安全遷移的研究，但是由于研究可信虛擬機的模型不統一，導致遷移模型解決問題的方案不能適用所有的遷移方案，存在一定的局限性.針對可信虛擬機的遷移缺乏統一的安全模型及測試方法的問題，參考虛擬機遷移中普遍存在的安全問題以及可信計算和云的相關規范，從整體系統層面對可信虛擬機的遷移進行安全需求分析；提出一種可信虛擬機遷移框架，將可信遷移的參與組件進行了抽象并描述了遷移協議中的關鍵步驟和狀態；以標號遷移系統LTS為操作語義描述工具對可信遷移系統進行進一步的描述，以系統中遷移進程組件的建模為基礎構建出動態的遷移系統狀態遷移樹；分析了LTS模型可以用于可信遷移協議的一致性測試，并通過與其他相關工作的比較說明了模型在考慮安全屬性方面的完備性.

可信虛擬機；虛擬機遷移；安全協議；標號遷移系統；安全模型

隨著云計算與可信計算技術的興起與發展，可信虛擬化技術得到了廣泛的研究與應用.虛擬化技術為云平臺實現資源抽象、隔離以及資源的按需分配提供技術支撐，可信計算技術為增強虛擬化安全提供了新的途經.在可信云虛擬化架構中，可信虛擬機(virtual machine, VM)是系統資源虛擬化的直觀體現，也與云用戶密切相關.

Fig. 1 vTPM architecture on KVM圖1 基于KVM的vTPM架構

虛擬機動態遷移是構建可信云平臺的重要需求之一.目前與可信計算關聯最緊密的虛擬化技術是虛擬可信平臺模塊(virtual TPM, vTPM)，它是TPM虛擬化的一種實現方式，為運行在主機上的多個虛擬機提供可信計算功能.我們把包含vTPM的虛擬機簡稱為可信虛擬機，其基于內核虛擬機(kenerl-based virtual machine, KVM)的基本結構如圖1所示.在可信虛擬機的動態遷移過程中，為使遷移前后系統的安全狀態保持同步，需將虛擬機和與對應的vTPM實例一起遷移.這時，主要考慮被遷移vTPM實例內存狀態在源主機的加密存儲與目的主機的安全恢復，及遷移過程中虛擬機與vTPM實例數據的機密性和完整性保護.

目前對于可信虛擬機遷移的研究主要集中在如何安全地構建可信遷移平臺并實現虛擬機與vTPM的安全遷移，這些研究為將vTPM應用于真實的云平臺提供了理論和實踐基礎.作為一種特殊的虛擬機，可信虛擬機的遷移不僅依賴于虛擬機的動態遷移技術，還涉及了可信計算的相關理論，因此屬于理論與實踐結合較為緊密的一項技術.由于動態遷移技術成熟，而可信計算理論尤其是可信虛擬化技術還在發展階段，存在一些尚未解決的關鍵問題，因此，將原始的動態遷移技術應用于vTPM虛擬機的遷移就存在著“技術與理論脫節”的問題.

具體來說，vTPM實例與虛擬機都能夠通過動態遷移技術實現遷移，但是對于遷移的流程是否安全、vTPM隱私性是否得到保障以及遷移前后的vTPM虛擬機的可信程度是否等價等問題，都沒有統一的測試評估標準，因此可信虛擬機遷移的測試評估理論研究是一個刻不容緩的問題.所以現有的可信虛擬機遷移的研究還存在3方面問題和挑戰：

1) 可信虛擬機的遷移缺乏明確統一的標準，使得現有遷移模型不夠完整，難以形成明確的分析目標和依據，無法有效地對遷移模型進行安全分析和評估；

2) 現有的大部分遷移方案僅僅只關注可信遷移中的某個問題，而平臺環境又不盡相同，這也就導致部分安全分析和解決方案的通用性不強；

3) 目前對于可信虛擬機遷移模型缺乏通用的建模方法，對于其安全需求缺少抽象的形式化描述，導致對于可信虛擬機的靜態安全以及遷移過程的機密性、完整性等動態安全屬性缺少綜合的理論分析研究，不利于在vTPM虛擬機與云環境結合之后對可信虛擬機遷移的可信性進行準確的評價.

因此，本文針對可信虛擬機動態遷移缺乏統一的理論模型和測試方法的問題，提出了一種可信虛擬機遷移模型的構建方法，主要工作有3方面：

1) 基于可信遷移的相關研究工作，分析可信虛擬機遷移的安全需求，這樣首先明確了評估可信遷移的主要內容以及分析的目標和依據，在此基礎之上從抽象的角度定義了參與可信遷移主要的相關實體，從而構建一個完善且易于描述的可信遷移模型架構；

2) 對可信虛擬機的遷移流程進行抽象描述，并對可信虛擬機遷移的行為特征進行推導，從動態的角度建立可信遷移模型，再以標號遷移系統(labeled transition system，LTS)為語義描述工具，對可信遷移協議進行形式化說明，以便完整反映可信遷移時組件的交互過程以及系統的狀態變遷過程；

3) 分析了本文模型的用途和使用范圍，證明了用它來對可信遷移系統或協議進行一致性測試可行性，并針對本文模型相對抽象的特點，證明簡化了部分非關鍵流程的協議模型依然可以用來測試.

1 相關工作

對于可信虛擬機的安全遷移問題，在vTPM這一概念被提出時就得到關注[1]，目前國內外也有許多學者以協議模型或具體實現的方式對可信虛擬機遷移展開研究.

文獻[1]首次提出了vTPM的實現方法，在遷移協議中加入了數據完整性保護機制以確保遷移數據的安全，可實現相同配置平臺間虛擬機的動態遷移，但文中研究建立在一個非常重要的假設上：遷移的目的主機是可信的，這就使其真正的可信性還需進一步研究.因為是最早提出的vTPM的方案，所以還未考慮其在真實云環境的應用場景，隨著vTPM和虛擬機技術的發展，遷移模型需要作出相應的調整，尤其是出于實際應用的考慮，相應的安全需求和解決方案都要考慮到更多的細節.文獻[2-3]在分析已有vTPM設計方案及相關遷移協議的基礎上，提出了遷移過程中的安全需求，然后針對這些需求，設計了一種新的密鑰體系，實現了可信虛擬機的安全遷移；文獻[4]提出一種可信虛擬機及其vTPM實例的安全遷移協議，但該協議中的遷移操作采用的是“掛起-傳輸-恢復”模式，并不是真正意義上的動態遷移；文獻[5]提出一個安全增強的遷移協議，在源主機與目的主機的認證過程中加入隨機數，以阻止截獲遷移數據的攻擊者對其他平臺進行重放攻擊；文獻[6]提出的實例對遷移協議解決了作為獨立域運行的時序問題；文獻[7]針對可信虛擬機遷移的整個流程中存在的攻擊隱患，提出了相應的改進協議，并通過分析驗證了新協議抵御各類攻擊的能力.

對于普通虛擬機遷移的安全研究相對比較成熟，文獻[8]通過實驗驗證了虛擬機動態遷移的安全問題主要源于3個層次：虛擬機監控器(virtual machine monitor, VMM)層、數據層和遷移模塊層，攻擊者可能利用虛擬化或遷移組件的漏洞獲得系統權限或虛擬機的隱私信息[9]，還可能利用遷移流程中的認證等協議的缺陷[10]獲取傳輸信道的數據.文獻[11]基于目前主流的KVM虛擬化環境，分析了遷移流程中可能存在的諸多安全問題，并基于混合隨機變換編碼機制提出了一種安全遷移模型.上述工作雖然是針對普通虛擬機的安全分析和建模，但其中涉及虛擬機動態遷移的安全問題在可信虛擬機遷移中也可能存在，因此，對普通虛擬機的遷移安全研究對于我們分析可信虛擬機的遷移以及建模工作有一定的指導意義.

上述可信虛擬機遷移方案中，或是提出一種概述性的可信虛擬機架構和遷移方法，沒有明確的模型建立依據和目標，或是針對vTPM遷移、密鑰遷移等問題提出的非通用的遷移方案，需要針對特定平臺設計新的遷移架構或vTPM密鑰體系，雖然考慮到虛擬機遷移的靈活性，但失去了通用性，適用范圍有限.因此，本文更關注于從理論角度更加抽象和通用地描述一個可信虛擬機遷移系統或協議，結合可信虛擬機遷移的安全需求建立對可信遷移的進行動態的模型描述，以便對可信遷移系統進行評估和測試.

2 可信遷移安全需求分析

可信虛擬機遷移系統包含大量相關聯的實體，為了便于對復雜的遷移系統進行描述，首先應該從較高的層級分析可信遷移有哪些必要的安全需求，在此基礎之上抽象地按照邏輯功能定義一些參與可信遷移主要的相關實體，從而構建一個完善且易于描述的可信遷移模型架構.

雖然可信虛擬機的遷移沒有明確的規范，但是我們可以根據以往的虛擬機遷移的安全分析[8,11]、可信計算組織(Trusted Computing Group, TCG)制定的可信計算的相關規范[12-13]以及云計算安全聯盟(Cloud Security Alliance, CSA)發布的《云安全指南》[14]來從可信虛擬機遷移的功能性和安全性2方面定義遷移實體的交互規則和安全規范.圖2從層級劃分的角度描述了可信虛擬遷移整體的安全需求.可以看出：可信遷移所包含的內容非常豐富，根據現有的研究我們發現，基于不同的硬件平臺和虛擬化架構會產生不同的可信遷移模型并導致模型在局部設計上存在一定的差異，例如在沒有使用物理TPM的平臺上就不存在TPM密鑰遷移的問題，但是從安全性的角度來看，基于硬件TPM保護可信虛擬機的隱私信息還是非常有必要的，而且現有的技術條件也支持云環境中基于TPM密鑰的遷移[15].

Fig. 2 The security requirements for the migration of trusted VMs圖2 可信虛擬機遷移安全需求說明

根據圖2中的安全需求說明，可信遷移是建立在可信的系統架構之上，系統應包括采用支持TPM和可信啟動的可信服務器、構建可信的VM-vTPM管理環境以及支持可信虛擬機等特性.上述保障系統遷移環境的安全技術涉及了從硬件層到虛擬化層的眾多問題，不可能針對每個層級進行細致的抽象，因此這些都不是本文討論的重點.本文主要是針對可信虛擬機的遷移流程進行描述，因此我們主要從系統流程中抽取最基本的安全行為和狀態，從動態安全的角度，對這些行為和狀態進行建模和分析.根據可信虛擬機的特點，其遷移根據流程主要涉及4個方面的安全需求：

1) 建立安全會話.云平臺通常包含大量主機，在2臺主機之間遷移虛擬機之前，首先要在兩者之間建立安全會話.建立會話的過程涉及了許多安全協議，例如遷移雙方通過的身份認證及密鑰協商建立一個安全的加密信道，隨后為了確保對方環境的安全，還要驗證主機或者系統軟件的完整性；為了抵抗認證和密鑰協商過程中可能存在的攻擊，本文假設存在一個可信的第三方，該可信第三方包含CA的作用，負責存儲和管理主機的證書、軟件的度量基準值等.

2) vTPM數據保護.可信虛擬機包含了vTPM設備及其隱私信息，為了保障其使用過程的安全，需要在虛擬機讀寫vTPM時進行動態的加解密[15].上面提到的vTPM設備和密鑰都是屬于非易失性的數據，可以直接通過安全信道傳輸，但是vTPM設備內存這類特殊的易失性的數據，需要采用額外的技術手段[15]進行處理以便進行遷移.

3) 數據安全傳輸.安全數據的傳輸是建立在安全會話的基礎之上，出于性能的考慮，通常加密vTPM的密鑰并非TPM的內部密鑰，而是由TPM封裝保護的一個外部密鑰，那么在遷移vTPM和密鑰時自然要考慮到TPM密鑰的遷移，這就涉及到TPM2.0中的duplication機制[12].

4) 原子性保護.遷移無論成功與否，遷移虛擬機所擁有的數據和狀態都應該是唯一的，遷移成功要刪除源主機的所有虛擬機的數據，遷移失敗則要將目的端的數據刪除，防止產生虛擬機和vTPM隱私信息泄露的安全問題.

3 可信遷移系統描述

3.1可信虛擬機遷移模型的邏輯構成

可信遷移系統內部包含大量可信虛擬機遷移相關的軟件和硬件實體，這些實體涉及的系統層次不同但又相互依存，不可能對所有的遷移相關的實體進行建模.因此，首先要對遷移系統的架構進行進一步的抽象，本文基于現有的遷移系統，然后根據第2節提出的可信虛擬機遷移的安全需求，將需求中所提的一些必要組件和流程體現在新的遷移框架中.本文主要是針對可信虛擬機的遷移流程進行描述，所以遷移框架主要體現的是抽象的遷移組件之間的交互.

為了能夠抽象出可信遷移中的組件進程，建立不同組件之間的交互關系，我們從邏輯上將可信遷移系統抽象為4個主要部分：遷移源主機(source host,SH)集群、目的主機(destination host,DH)集群、可信第三方(trusted third party,TTP)、共享存儲服務器集群(shared storage host,SSH)，如圖3所示:

Fig. 3 The basic framework for the migration of trusted VMs圖3 可信虛擬機遷移基礎框架

我們對圖3進行說明：

1) 遷移主機集群.包括遷移源主機集群和目的主機集群，這里是從遷移系統的邏輯角度來對主機集群進行劃分，實際上這些主機都是等價的，都是參與可信虛擬機遷移的主體.遷移雙方通過共享服務器以及安全信道來交互數據.

2) 可信第三方.為遷移雙方的相互認證提供相應的證書和可信證據(主機、vTPM虛擬機等的完整性信息等)的管理.

3) 共享存儲服務器集群.為了提高遷移效率，一些如虛擬機鏡像的大型文件都通過共享存儲服務器來共享，避免信道傳輸大量的數據.

圖3中的4個抽象實體通過不斷地交互來完成可信虛擬機遷移的操作，多個組件之間存在重復的交互，這種交互影響著遷移系統狀態在不斷地變化著，下面我們首先給出可信遷移系統和協議流程的抽象描述.

3.2遷移模型描述

基于2.2節中描述的基本框架與邏輯構成，我們將可信遷移系統做抽象定義：

定義1. 可信遷移系統.它是三元組(M，Ds，As)，其中M代表參與遷移的主體.其中，M代表遷移主體集合，包括了所有可遷移虛擬機的主機、可信第三方TTP以及共享存儲服務器，記為M={SH，DH，TTP，SSH},這里SH={SH1，SH2，…，SHn}表示所有的源主機，DH={DH1，DH2，…，DHn}表示所有的目的主機；Ds代表遷移過程中主體之間交互的數據集；As代表主體之間交互的動作的合集.上述定義中關鍵屬性的具體內容和說明如表1、表2所示：

Table 1 Data Attributes and Definitions of Migration Protocol表1 遷移協議中的數據屬性和定義

Table 2 Action Attributes and Definitions of Migration Protocol表2 遷移協議中的動作屬性和定義

為了更好地對遷移系統的全局狀態和原子動作以及對應的狀態變遷規則進行描述，下面首先依據上述定義對整個遷移協議的流程進行描述：

1) 建立安全會話

① 身份認證

DH→SH：certificateDH；

SH，TTP：Authentication(certificateDH，TTP)；

SH→DH：certificateSH；

DH，TTP：Authentication(certificateSH，TTP)；

② 協商信道keychannel

DH，SH：Keyexchange(secretSH，secretDH，protocol)；

③ 完整性驗證

DH→SH：Encrypt(Keychannel)(DH.measure_loc)；

SH→DH：Encrypt(Keychannel)(SH.measure_loc)；

TTP→DH：SH.measure_bak.

TTP→SH：DH.measure_bak；

SH：Cont(DH.measure_loc，DH.measure_bak)；

DH：Cont(SH.measure_loc，SH.measure_bak).

2) 數據傳輸

① VM-vTPM傳輸

SSH→DH：vm_image，vTPM_image；

DH：CreateDH.vmandDH.vTPM；SH→DH：lterative_memory；

SH：SuspendVM-vTPMand SaveSH.vTPM_state；

SH→DH：SH.vm_state，SH.vTPM_state；

DH:RestoreVM-vTPM；

② 密鑰遷移

SH：UnsealSH.KeyvTPM；

SH，DH：Duplication protocol；

DH：ImportSH.KeyvTPMand SealSH.KeyvTPM.

3) 原子判定

if (sessionfail∪keyimportfail∪VMrestore

fail∪vTPMrestorefail)

DH→SH：flag_fail；

DH：DeleteDH.data_VMandDH.data_vTPM；

else

DH→SH：flag_success；

SH：DeleteSH.data_VMandSH.data_vTPM.

end if

這里通過將可信遷移的部分安全需求體現在遷移的系統架構中，然后將可信遷移系統抽象描述為4個實體之間的交互系統，一個遷移系統就能夠通過交互協議來進行描述，并且其中的關鍵動作還反映了系統的部分安全需求.基于交互協議中的關鍵動作和狀態，我們就可利用標號遷移系統對其進行進一步地形式化描述.

4 可信遷移系統的運行狀態變遷模型

第3.2節已經將可信遷移模型的執行流程以協議的形式進行描述，那么為了進一步對遷移系統的關鍵動作和狀態進行動態的描述，就需要開展對協議實現的動態分析.根據自動機原理，標號遷移系統[16]是由起點、輸入標識、終點組成的一個系統轉換模型.由于標號遷移系統不完全等同于自動機，它沒有固定的初始狀態和接受狀態，所以在標號遷移系統中，任何一個狀態都可以作為初始狀態，故標號遷移系統在動態分析密碼協議實現的安全中具有一定的優勢.因此，我們采用標號遷移系統對可信遷移系統的協議實現進行描述.

4.1LTS相關定義

定義3. 動作跡(trace).Trace(p)={ω∈L*|p=ω?}表示狀態p上的所有可觀察動作的跡，L*表示L上所有跡的集合.Sub(p)={p′∈Q|?ω∈L*:|p=ω?p′}描述了跡存在性的表示方法，表示L中存在一條從狀態p到狀態p′的動作跡ω.

定義4. 狀態收斂.q∈Q，q表示狀態q的收斂，那么：

2) 如果q，則qε；

3) 如果qand (q=s?q′)，則qs.

定義5. 強模擬.設(Q，T)為一個標號遷移系統，并設S是一個Q上的二元關系.一旦pSq總有條件成立：

定義6. 擴展的強模擬.設(Q，T)為一個標號遷移系統.(Q′，T′)也是一個標號遷移系統，S在Q×Q′上是一個二元關系，且p，q∈Q.如果pSq滿足條件：

1)Q′?Q，T′?T；

2)p′，q′∈Q′，且α=α′，α' ∈T′.

標號遷移系統的部分相關符號定義如表3所示：

Table 3 Partial Symbols and Definitions in LTS表3 標號遷移系統的部分符號和定義

4.2可信遷移組件狀態圖

任何協議都可以看成多個實體(或稱為進程)之間的交互，而每個實體都可以通過標號遷移系統來形式化地描述其行為和狀態，例如典型的端到端的通信協議AB協議[17]可以將其中的發送方S和接收方R當成2個進程分別描述成LTS樹，如圖4所示，根據樹形表示可以很容易得到它們的行為和狀態轉換.

Fig. 4 Process state of AB protocol圖4 AB協議進程狀態圖

根據上述方法，我們首先將3.1節中定義的遷移主體作為協議系統中的4個進程分別進行LTS樹建模，將這些進程作為遷移模型的組件，每個組件的LTS狀態圖都可以當成遷移整體架構狀態圖的一個組成部分.根據遷移系統的特點，我們將SH,DD,TTP和SSH之間的通信過程定義為系統的可觀察動作，而它們內部組件的處理過程為系統不可觀察的內部動作，各組件主要包含交互規則：

1)SH負責發起建立安全會話的請求，通過與TTP和DH交互信息來驗證目的主機的當前安全狀態.驗證通過之后開始傳輸遷移數據，并根據傳輸過程中出現問題與否決定下一步的對剩余遷移數據的處理并進行收尾工作，例如遷移數據成功之后，源主機刪除本地所有和遷移虛擬機相關的數據.

2)DH負責接受遷移的虛擬機，通過與TTP和交互信息來驗證源主機的安全狀態；驗證通過之后開始接收遷移數據，并根據傳輸過程中出現問題與否決定下一步的對剩余遷移數據的處理并進行收尾工作，例如遷移數據失敗之后，目的主機刪除本地所有和遷移虛擬機相關的數據.

3)TTP主要負責存儲遷移雙方的證書以及度量基準值等可信信息，通過與遷移雙方交互來提供可信服務.

4)SSH主要負責在源主機和目的主機之間共享虛擬機鏡像、vTPM鏡像等容量較大的文件，在遷移這一流程中SS僅接收源主機和目的主機的請求，并進行相應的處理后返回結果.

根據4條規則，我們可信遷移協議中的發送進程SH和接收進程DH以及2個協調進程TTP和SSH進程分別描述成LTS樹，如圖5所示:

Fig. 5 The process state of trusted migration protocol圖5 可信遷移協議進程狀態圖

4.3可信遷移系統整體狀態變遷模型

Fig. 6 LTS model of trusted migration system圖6 可信遷移系統的LTS模型

4.2節中的進程組件狀態圖描述的是遷移過程中系統的主要組件的狀態變化，為了能夠準確反映系統整體的動態屬性，比如在可信遷移過程中執行不同關鍵操作時進程之間相互作用的反饋以及系統在某時刻的整體狀態等.因此，有必要根據可信協議整體流程的行為和狀態，結合3.2節中的各個進程組件的描述刻畫出系統運行時的狀態變遷圖LTS(P).

在交互行為集的基礎上，綜合上述組件模型以及變遷規則(見附表A1)，我們就可以進一步刻畫出遷移系統運行時的狀態變遷圖，為了與遷移流程對應，我們將整體的LTS樹劃分為3個階段：

1) 圖6(a)表示系統在建立安全會話階段的狀態變遷圖，P0表示遷移系統的初始狀態，未開始遷移之前的任何異常錯誤都可能導致系統回到初始狀態.系統經過一些安全遷移條件的判別來確認系統是否滿足安全會話的條件.

2) 在系統狀態滿足所有的安全遷移判別條件之后，即建立起遷移主機雙方的安全會話達到如圖6(b)所示狀態P6.在開始內存預拷貝之前，系統還需要根據當前的系統配置和參數進行一些準備工作.

3) 內存預拷貝結束之后開始執行內存的迭代傳輸，這些都屬于系統的內部不可見動作.如圖6(c)所示，在虛擬機所有數據傳輸結束之后，系統根據虛擬機是否成功恢復運行執行相應的操作，如果遷移失敗，系統可能會恢復到遷移之前的狀態.

根據可信遷移的相關安全需求和協議規則，圖6描述了遷移系統在4個主要參與實體的影響下的狀態變遷關系.因為根據具體的實現和人為的設定，遷移系統的動作的集合是會發生變化的，為了能夠通用且準確地測試遷移系統，需要確定遷移過程中通用的可觀察狀態，即說明系統的狀態是收斂，LTS(P)不存在狀態變遷和內部動作的無窮組合，因此，我們提出命題和證明：

命題1. 在LTS(P)中存在狀態Pi，Pj∈Q且i

證明. 假設?Sub(P0)，Pi∈Q(i>0)，根據定義2和定義3則有?ω∈L*使得P0=ω?Pi，說明LTS(P)中存在一條從狀態P0到Pi的動作跡ω，因為在LTS(P)中P0是系統的初始狀態，所有顯然P0，再根據定義4可知，如果P0且存在P0到Pi的動作跡ω，那么Piω.同理，若Pi，則根據相同的推理規則可以得出Pi后續狀態也是收斂的某個動作.命題1得證.

證畢.

命題1說明了我們定義的遷移系統運行狀態是收斂的，即不存在無窮的狀態變遷和內部變化，這也滿足了具體遷移實現需求，即從遷移初始狀態開始，系統能夠經過有限的狀態變遷，達到預期的收斂狀態，不會出現一些無意義的導致系統出現死鎖等狀態的中間狀態.由此可證明模型的建立是符合需求規則的.

4.4狀態樹約減

通常一個系統或協議在實際運行過程中不是一成不變的，這和系統的設計和運行環境都有密切的聯系，但是在符合規范的前提下，系統必然有一些必達的運行狀態，這些狀態之間的路徑都是受相關的安全規則所約束的，因此，為了提升測試的效率和可靠性，我們可以對4.3中的LTS樹進行約減.

根據遷移系統的安全需求和各個動作的必要性，我們將一些動作定義為可以約減的動作：1)在真實的云環境中，遷移雙方的身份認證實際上是可以由云管理中心的策略來控制實現的，遷移系統本身可以不參與到該流程中，因此狀態P1，P2是可以移除的；2)在遷移雙方建立安全會話之后，目的主機可能需要進行一些準備工作，例如從共享服務器獲取鏡像文件、創建空的VM和vTPM等，但是這些都不是必須的，因此這些準備工作可能在開始遷移之間已經做好了，因此在狀態P7～P11中只有P9是必須保留的，而其他狀態可以和P9進行合并；3)在遷移結束階段，P15不是必須的，因為在恢復虛擬機運行階段已包含了驗證的邏輯，因此不需要系統主動發起狀態檢查，除非需要建立特殊的反饋系統提供給云管理中心.

根據上述規則，LTS(P)約減樹如圖6(d)所示，系統狀態從約減之前的17種約減為10種，Q×Q上的二元關系從36種減少為19種.為了評價約減前后的LTS之間的關系,我們引入了最常見的等價關系跡前序≤t r，根據定義7以及相關的證明[18-19]，可以推導出：在本文中，由于約減標號遷移樹LTS(P′)是由LTS(P)經過正確約減得出的，那么它們滿足跡前序≤t r，即：

定義7. 設p∈LTS(p)，q∈LTS(q)，若LTS(p)是LTS(q)的子樹則兩者滿足關系≤tr，即有traces(p)?traces(q).

5 模型的應用與分析

第4節已經討論了利用LTS對可信遷移系統進行建模，并證明其正確性，下面將主要討論如何利用該模型來對其他的可信遷移系統進行測試，其中涉及了協議一致性測試的工作，我們將結合本文模型進行描述.為了更好地討論本文模型，本節最后還將本文的模型與其他相關的工作進行了比較分析.

5.1協議一致性測試

協議一致性測試主要包含2個方面[17]：測試生成和測試執行.測試生成通過分析協議說明來確定要測試的各個方面，從而產生測試套(測試例集合)；測試執行部分分為測試例的運行提供環境，并分析測試結果，給出測試判決.本文針對可信遷移系統所描述的LTS(P)即可作為一致性測試中的測試例.利用第4節的LTS建模方法，我們可將任意的遷移協議或系統i描述成LTS(I)樹，我們將其稱為測試對象.通過將本文模型與其他模型進行比較，即將LTS(P)與LTS(I)進行一致性測試，驗證協議i對應模型所有的與本文定義的可觀察動作有哪些是匹配的又有哪些是不在LTS(P)所定義的規則內的.例如假設LTS(I)對應遷移系統沒有考慮TPM密鑰的遷移，那么其LTS樹中肯定沒有與LTS(P)的P14所匹配的狀態和路徑，那么反過來說明通過本模型確實能夠發現其他遷移系統中的缺陷.

根據“一致性”的定義[17]，我們將測試中使用的遷移協議形式化說明集合記為MIGSPECS，將協議實現的集合記為MIGIMPS，它們之間的關系記為imp，其定義為

imp?MIGSPECS×MIGIMPS，

任何(p，i)∈imp或pimpi表示p是i的一個一致性關系.對于p∈LTS(P)，i∈LTS(I)，MIGIMPS與MIGSPECS的“一致性”關系還可以定義在形式化的系統之上記為impLTS?LTS(P)×LTS(I).為了說明通過一致性測試可以證明協議LTS的一致性關系，我們給出命題和證明：

命題2. 存在一個測試例LTS(P)和一個測試對象LTS(I)，測試套T是測試例的一個集合，?i∈LTS(I)，若i能夠通過T，則存在impLTS?LTS(P)×LTS(I).

證明. 如果i能夠通過T，那么存在LTS(P)∈T，i能夠通過測試例LTS(P)，那么就存在協議說明p∈LTS(P)，使得i能夠通過p，根據上述“一致性”的定義，因此就存在協議說明和協議實現之間的一致性關系，即存在(p，i)∈imp，那么對于p∈LTS(P)，i∈LTS(I)，就存在impLTS?LTS(P)×LTS(I).命題2得證.

證畢.

命題2說明了在測試例LTS(P)滿足一定條件的情況下，可以通過協議的一致性測試來證明測試例與其他協議實現的LTS的一致性關系.需要注意的是，實際測試一般不能證明一致性，而只能證明某些協議實現與協議說明不一致[17].由于目前可信遷移系統還沒商業化或者開源的實際系統的應用，因此還無法對真實的系統進行測試，但是通過本節的分析已經說明了測試的可行性，后續我們也將基于本文的模型和方法開展對仿真系統中可信遷移系統的測試，為今后真實的平臺測試打下良好的基礎.

另外，本文可信遷移模型更加抽象，在建模過程中簡化了遷移中的部分非關鍵流程(不影響協議的安全屬性)，為了說明簡化的遷移流程的有效性，我們給出命題和證明：

命題3. 如果去除可信遷移流程中的非關鍵部分，且簡化前后協議的安全屬性具有一致性，那么在分析評估系統的安全狀態遷移時，簡化的流程可以等價于原系統.

證畢.

5.2與現有模型對比

本文從抽象的角度概括了可信遷移中的一些安全屬性，基于這些屬性我們將本文的模型與其他同類工作中的協議或者模型進行對比分析，如表4所示.本文模型基于遷移系統、可信虛擬機的具體實現以及遷移和可信計算相關理論的研究概括總結出更加完備的系統安全屬性.文獻[1]首次提出了vTPM的概念，為之后的可信虛擬化的發展奠定了基礎，但此時可信虛擬機遷移的概念還不夠成熟，也沒有在真實的系統上實現和應用，因此遷移流程只能考慮到與可信計算相關的細節，無法全面考慮到實際的應用場景的安全需求；文獻[2]對一些基于Xen的vTPM虛擬機遷移方案進行介紹和分析，指出了vTPM虛擬機遷移所面臨的安全問題，最后設計并實現了vTPM虛擬機遷移方案，該方案的安全需求考慮的還是比較全面，但是關鍵的對于vTPM隱私信息的保護和遷移并沒有得到有效的解決；文獻[3-4]主要是針對vTPM密鑰樹以及相關密鑰遷移協議的設計與分析，解決了密鑰在云環境中遷移的問題，但是缺少對實際云環境中vTPM的安全需求的考慮；文獻[6]基于TPM2.0的平臺設計vTPM密鑰樹以及VM-vTPM遷移協議，比較符合目前可信虛擬化的發展趨勢，并采用Ban邏輯對協議的安全性進行了證明，該方案解決了VM-vTPM的狀態同步和vTPM遷移時序問題，但是沒有討論vTPM的非易失性信息的遷移問題；文獻[7]分析了現有的VM-vTPM方案，并從攻擊的角度分析可信虛擬機遷移的安全問題，提出一種改進的vTPM虛擬機動態遷移協議，該協議利用基于TPM的TLS協議進行身份認證，建立安全信道，然后利用基于TPM的vTPM遷移條件判別方法驗證遷移過程中參與實體的完整性，最后在源主機與目的主機間進行數據傳輸，TPM可遷移密鑰對暫停階段遷移的數據做加密保護，本文考慮的安全屬性較為全面，但是沒有對vTPM隱私保護相關TPM密鑰的遷移展開討論.

Table 4 Comparison Between our Model and Other Related Models表4 本文模型與其他相關模型的比較

本文基于上述研究成果，總結和分析了可信虛擬機遷移的安全需求，并且還考慮了目前可信計算和云平臺結合的發展現狀，因此，綜合來看本文所建模型考慮的安全屬性還是較為全面和符合真實應用場景的，能夠較完整地體現可信遷移系統的安全需求.

6 總 結

針對可信虛擬機遷移缺少統一的安全分析模型的問題，本文基于虛擬機遷移安全的實踐與經驗，結合可信計算以及云安全的一些理論知識，抽象出可信遷移中的一些關鍵的動態安全屬性；然后基于標號遷移系統對可信遷移系統的行為和安全屬性進行建模，以系統中遷移進程組件的建模為基礎構建出動態的遷移系統狀態遷移樹，并根據相關規則對其進行了約減，以提高測試效率；之后分析了本文模型在協議一致性測試工作的應用場景，并通過理論證明了其有效性；最后將本文模型與其他相關工作進行了比較.在后續的研究中我們將繼續完善可信虛擬機遷移模型，首先對安全需求進行進一步的分析，使得模型更加完備；其次，可信遷移中還涉及到很多深層次的協議和理論，隨著研究的深入，還應該在模型中考慮到更加細粒度的安全屬性；最后，在考慮安全性的基礎之上，分析遷移系統的可用性、可靠性等其他屬性.

[1] Berger S, Goldman K A, Perez R, et al. vTPM: Virtualizing the trusted platform module[C] //Proc of the 15th USENIX Security Symp. Berkeley, CA: USENIX Association, 2006: 305-320

[2] Masti R J. On the security of virtual machine migration and related topics[D]. Zurich: Department of Computer Sciences, Swiss Federal Institute of Technology Zurich, 2010

[3] Liang Xinlong, Jiang Rui, Kong Huafeng. Secure and reliable VM-vTPM migration in private cloud [C] //Proc of the 2nd Int Symp on Instrumentation and Measurement, Sensor Network and Automation. Piscataway, NJ: IEEE, 2013: 510-514

[4] Danev B, Masti R J, Karame G O, et al. Enabling secure VM-vTPM migration in private clouds [C] //Proc of the 27th Annual Computer Security Applications Conf. New York: ACM, 2011: 187-196

[5] Chang Dexian, Chu Xiaobo, Wei Ge. Analysis of the security-enhanced vTPM migration protocol based on ProVerif [C] //Proc of the 5th Int Conf on Computational and Information Sciences. Piscataway, NJ: IEEE, 2013: 1437-1440

[6] Yang Yongjiao, Yan Fei, Mao Junpeng, et al. Ng-vTPM: A next generation virtualized TPM architecture[J]. Journal of Wuhan University: Natural Science Edition, 2015, 61(2): 103-111 (in Chinese)

(楊永嬌, 嚴飛, 毛軍鵬, 等. Ng-vTPM: 新一代TPM虛擬化框架設計[J]. 武漢大學學報: 理學版, 2015, 61(2): 103-111)

[7] Fan Peiru, Zhao Bo, Shi Yuan, et al. An improved vTPM-VM live migration protocol[J]. Wuhan University Journal of Natural Sciences, 2015, 20(6): 512-520

[8] Rehman A, Alqahtani S, Altameem A, et al. Virtual machine security challenges: Case studies[J]. International Journal of Machine Learning & Cybernetics, 2014, 5(5): 729-742

[9] Xiong Haiquan, Liu Zhiyong, Xu Weizhi, et al. Interception and identification of guest OS non-trapping system call instruction within VMM[J]. Journal of Computer Research and Development, 2014, 51(10): 2348-2359 (in Chinese)

(熊海泉, 劉志勇, 徐衛志, 等. VMM中Guest OS非陷入系統調用指令截獲與識別[J]. 計算機研究與發展, 2014, 51(10): 2348-2359)

[10] Wan Tao, Liu Zunxiong, Ma Jianfeng, et al. Authentication and key agreement protocol for multi-server architecture[J]. Journal of Computer Research and Development, 2016, 53(11): 2446-2453 (in Chinese)

(萬濤, 劉遵雄, 馬建峰. 多服務器架構下認證與密鑰協商協議[J]. 計算機研究與發展, 2016, 53(11): 2446-2453)

[11] Fan Wei, Kong Bin, Zhang Zhujun, et al. Security protection model on live migration for KVM virtualization[J]. Journal of Software, 2016, 27(6): 1402-1416 (in Chinese)

(范偉, 孔斌, 張珠君, 等. KVM 虛擬化動態遷移技術的安全防護模型[J]. 軟件學報, 2016, 27(6): 1402-1416)

[12] Trusted Computing Group. Trusted platform module library family 2.0 level 00 revision 01.16 [EB/OL]. [2017-05-23]. http：//www. trustedcomputinggroup.org

[13] Trusted Computing Group. TCG specifications[EB/OL]. [2017-05-23]. http：//www.trustedcomputinggroup.org

[14] Cloud Security Alliance. Security guidance for critical areas of focus in cloud computing v3.0[EB/OL]. [2017-05-23]. http：//www.Cloudse curityalliance.org/guidance/csaguide.v3.0.pdf

[15] Shi Yuan, Zhao Bo, Yu Zhao, et al. A security-improved scheme for virtual TPM based on KVM[J]. Wuhan University Journal of Natural Sciences, 2015, 20(6): 505-511

[16] Milner R. Communicating and mobile systems: Theπ-calculus[M]. Cambridge, UK: Cambridge University Press, 1999

[17] Jiang Fan, Ning Huazhong. Automatic test suite generation based on labelled transition system[J]. Journal of Computer Research and Development, 2001, 38(12): 1435-1445 (in Chinese)

(蔣凡, 寧華中. 基于標號變遷系統的測試集自動生成[J]. 計算機研究與發展, 2001, 38(12): 1435-1445)

[18] Xu Mingdi, Zhang Huanguo, Yan Fei. Testing on trust chain of trusted computing platform based on labeled transition system[J]. Chinese Journal of Computers, 2009, 32(4): 635-645 (in Chinese)

(徐明迪, 張煥國, 嚴飛. 基于標記變遷系統的可信計算平臺信任鏈測試[J]. 計算機學報, 2009, 32(4): 635-645)

[19] Zhao Bo, Dai Zhonghua, Xiang Shuang, et al. Model constructing method for analyzing the trusty of cloud[J]. Journal of Software, 2016, 27(6): 1349-1365 (in Chinese)

(趙波, 戴忠華, 向騻, 等. 一種云平臺可信性分析模型建立方法[J]. 軟件學報, 2016, 27(6): 1349-1365)

AMethodofConstructingtheModelofTrustedVirtualMachineMigration

Shi Yuan, Zhang Huanguo, and Wu Fusheng

(SchoolofComputerScience,WuhanUniversity,Wuhan430072) (KeyLaboratoryofAerospaceInformationSecurityandTrustedComputing(WuhanUniversity),MinistryofEducation,Wuhan430072)

The security migration of virtual machines (VMs) is one of the important requirements to ensure the security of cloud environment. For trusted VMs that contain vTPM (virtual TPM), the security migration of vTPM is also need to consider. At present, there are some researches on the security migration of trusted VMs. However, due to the non-uniform model of trusted VMs, the solution of the migration model cannot be applied to all migration schemes, so there are some limitations that there are no uniform security model and test method for the migration of trusted VMs. Regarding the issues above and referring to the common security issues in virtual machine migration and the relevant specifications for trusted computing and cloud, we analysis the security requirements of trusted VMs. Based on the requirements analysis, we propose a migration framework of trusted VMs that abstracts the participation components of trusted migration and describes the key steps and states in the migration process. Then the labeled transition system (LTS) is used to model the behavior and security attributes of the trusted migration system, and we construct a dynamic state transition tree of migration system based on the model of migration components in the system. The migration model of the migration system is constructed based on the modeling of the process components. We prove that our model can be applied to the consistency test of trusted migration protocol, and the comparison with other related work shows that the model is more fully considering the security attributes in trusted migration.

trusted virtual machine; virtual machine migration; security protocol; labeled transition system; security model

TP309

ShiYuan, born in 1991. PhD candidate at the School of Computer Science, Wuhan University. His main research interests include trusted computing and information security.

ZhangHuanguo, born in 1945. Professor and PhD director of the School of Computer Science, Wuhan University. His main research interests include information security, cryptography, trusted computing, cloud computing, fault tolerance, and computer application.

WuFusheng, born in 1974. PhD candidate at the School of Computer Science, Wuhan University. His main research interests include design of cryptographic protocols and security analysis of cryptographic protocols.

附錄A

Table A1 The State Transition of Trusted Migration System