石 源 張煥國(guó) 吳福生

(武漢大學(xué)計(jì)算機(jī)學(xué)院 武漢 430072) (空天信息安全與可信計(jì)算教育部重點(diǎn)實(shí)驗(yàn)室(武漢大學(xué)) 武漢 430072) (yuanshi@whu.edu.cn)

2017-06-11；

2017-07-31

國(guó)家自然科學(xué)基金項(xiàng)目(61332019)；國(guó)家“九七三”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃基金項(xiàng)目(2014CB340601)；國(guó)家“八六三”高技術(shù)研究發(fā)展計(jì)劃基金項(xiàng)目(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).

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

一種可信虛擬機(jī)遷移模型構(gòu)建方法

石 源 張煥國(guó) 吳福生

(武漢大學(xué)計(jì)算機(jī)學(xué)院 武漢 430072) (空天信息安全與可信計(jì)算教育部重點(diǎn)實(shí)驗(yàn)室(武漢大學(xué)) 武漢 430072) (yuanshi@whu.edu.cn)

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

可信虛擬機(jī)；虛擬機(jī)遷移；安全協(xié)議；標(biāo)號(hào)遷移系統(tǒng)；安全模型

隨著云計(jì)算與可信計(jì)算技術(shù)的興起與發(fā)展，可信虛擬化技術(shù)得到了廣泛的研究與應(yīng)用.虛擬化技術(shù)為云平臺(tái)實(shí)現(xiàn)資源抽象、隔離以及資源的按需分配提供技術(shù)支撐，可信計(jì)算技術(shù)為增強(qiáng)虛擬化安全提供了新的途經(jīng).在可信云虛擬化架構(gòu)中，可信虛擬機(jī)(virtual machine, VM)是系統(tǒng)資源虛擬化的直觀體現(xiàn)，也與云用戶密切相關(guān).

Fig. 1 vTPM architecture on KVM圖1 基于KVM的vTPM架構(gòu)

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

目前對(duì)于可信虛擬機(jī)遷移的研究主要集中在如何安全地構(gòu)建可信遷移平臺(tái)并實(shí)現(xiàn)虛擬機(jī)與vTPM的安全遷移，這些研究為將vTPM應(yīng)用于真實(shí)的云平臺(tái)提供了理論和實(shí)踐基礎(chǔ).作為一種特殊的虛擬機(jī)，可信虛擬機(jī)的遷移不僅依賴于虛擬機(jī)的動(dòng)態(tài)遷移技術(shù)，還涉及了可信計(jì)算的相關(guān)理論，因此屬于理論與實(shí)踐結(jié)合較為緊密的一項(xiàng)技術(shù).由于動(dòng)態(tài)遷移技術(shù)成熟，而可信計(jì)算理論尤其是可信虛擬化技術(shù)還在發(fā)展階段，存在一些尚未解決的關(guān)鍵問題，因此，將原始的動(dòng)態(tài)遷移技術(shù)應(yīng)用于vTPM虛擬機(jī)的遷移就存在著“技術(shù)與理論脫節(jié)”的問題.

具體來說，vTPM實(shí)例與虛擬機(jī)都能夠通過動(dòng)態(tài)遷移技術(shù)實(shí)現(xiàn)遷移，但是對(duì)于遷移的流程是否安全、vTPM隱私性是否得到保障以及遷移前后的vTPM虛擬機(jī)的可信程度是否等價(jià)等問題，都沒有統(tǒng)一的測(cè)試評(píng)估標(biāo)準(zhǔn)，因此可信虛擬機(jī)遷移的測(cè)試評(píng)估理論研究是一個(gè)刻不容緩的問題.所以現(xiàn)有的可信虛擬機(jī)遷移的研究還存在3方面問題和挑戰(zhàn)：

1) 可信虛擬機(jī)的遷移缺乏明確統(tǒng)一的標(biāo)準(zhǔn)，使得現(xiàn)有遷移模型不夠完整，難以形成明確的分析目標(biāo)和依據(jù)，無法有效地對(duì)遷移模型進(jìn)行安全分析和評(píng)估；

2) 現(xiàn)有的大部分遷移方案僅僅只關(guān)注可信遷移中的某個(gè)問題，而平臺(tái)環(huán)境又不盡相同，這也就導(dǎo)致部分安全分析和解決方案的通用性不強(qiáng)；

3) 目前對(duì)于可信虛擬機(jī)遷移模型缺乏通用的建模方法，對(duì)于其安全需求缺少抽象的形式化描述，導(dǎo)致對(duì)于可信虛擬機(jī)的靜態(tài)安全以及遷移過程的機(jī)密性、完整性等動(dòng)態(tài)安全屬性缺少綜合的理論分析研究，不利于在vTPM虛擬機(jī)與云環(huán)境結(jié)合之后對(duì)可信虛擬機(jī)遷移的可信性進(jìn)行準(zhǔn)確的評(píng)價(jià).

因此，本文針對(duì)可信虛擬機(jī)動(dòng)態(tài)遷移缺乏統(tǒng)一的理論模型和測(cè)試方法的問題，提出了一種可信虛擬機(jī)遷移模型的構(gòu)建方法，主要工作有3方面：

1) 基于可信遷移的相關(guān)研究工作，分析可信虛擬機(jī)遷移的安全需求，這樣首先明確了評(píng)估可信遷移的主要內(nèi)容以及分析的目標(biāo)和依據(jù)，在此基礎(chǔ)之上從抽象的角度定義了參與可信遷移主要的相關(guān)實(shí)體，從而構(gòu)建一個(gè)完善且易于描述的可信遷移模型架構(gòu)；

2) 對(duì)可信虛擬機(jī)的遷移流程進(jìn)行抽象描述，并對(duì)可信虛擬機(jī)遷移的行為特征進(jìn)行推導(dǎo)，從動(dòng)態(tài)的角度建立可信遷移模型，再以標(biāo)號(hào)遷移系統(tǒng)(labeled transition system，LTS)為語義描述工具，對(duì)可信遷移協(xié)議進(jìn)行形式化說明，以便完整反映可信遷移時(shí)組件的交互過程以及系統(tǒng)的狀態(tài)變遷過程；

3) 分析了本文模型的用途和使用范圍，證明了用它來對(duì)可信遷移系統(tǒng)或協(xié)議進(jìn)行一致性測(cè)試可行性，并針對(duì)本文模型相對(duì)抽象的特點(diǎn)，證明簡(jiǎn)化了部分非關(guān)鍵流程的協(xié)議模型依然可以用來測(cè)試.

1 相關(guān)工作

對(duì)于可信虛擬機(jī)的安全遷移問題，在vTPM這一概念被提出時(shí)就得到關(guān)注[1]，目前國(guó)內(nèi)外也有許多學(xué)者以協(xié)議模型或具體實(shí)現(xiàn)的方式對(duì)可信虛擬機(jī)遷移展開研究.

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

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

上述可信虛擬機(jī)遷移方案中，或是提出一種概述性的可信虛擬機(jī)架構(gòu)和遷移方法，沒有明確的模型建立依據(jù)和目標(biāo)，或是針對(duì)vTPM遷移、密鑰遷移等問題提出的非通用的遷移方案，需要針對(duì)特定平臺(tái)設(shè)計(jì)新的遷移架構(gòu)或vTPM密鑰體系，雖然考慮到虛擬機(jī)遷移的靈活性，但失去了通用性，適用范圍有限.因此，本文更關(guān)注于從理論角度更加抽象和通用地描述一個(gè)可信虛擬機(jī)遷移系統(tǒng)或協(xié)議，結(jié)合可信虛擬機(jī)遷移的安全需求建立對(duì)可信遷移的進(jìn)行動(dòng)態(tài)的模型描述，以便對(duì)可信遷移系統(tǒng)進(jìn)行評(píng)估和測(cè)試.

2 可信遷移安全需求分析

可信虛擬機(jī)遷移系統(tǒng)包含大量相關(guān)聯(lián)的實(shí)體，為了便于對(duì)復(fù)雜的遷移系統(tǒng)進(jìn)行描述，首先應(yīng)該從較高的層級(jí)分析可信遷移有哪些必要的安全需求，在此基礎(chǔ)之上抽象地按照邏輯功能定義一些參與可信遷移主要的相關(guān)實(shí)體，從而構(gòu)建一個(gè)完善且易于描述的可信遷移模型架構(gòu).

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

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

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

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

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

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

4) 原子性保護(hù).遷移無論成功與否，遷移虛擬機(jī)所擁有的數(shù)據(jù)和狀態(tài)都應(yīng)該是唯一的，遷移成功要?jiǎng)h除源主機(jī)的所有虛擬機(jī)的數(shù)據(jù)，遷移失敗則要將目的端的數(shù)據(jù)刪除，防止產(chǎn)生虛擬機(jī)和vTPM隱私信息泄露的安全問題.

3 可信遷移系統(tǒng)描述

3.1可信虛擬機(jī)遷移模型的邏輯構(gòu)成

可信遷移系統(tǒng)內(nèi)部包含大量可信虛擬機(jī)遷移相關(guān)的軟件和硬件實(shí)體，這些實(shí)體涉及的系統(tǒng)層次不同但又相互依存，不可能對(duì)所有的遷移相關(guān)的實(shí)體進(jìn)行建模.因此，首先要對(duì)遷移系統(tǒng)的架構(gòu)進(jìn)行進(jìn)一步的抽象，本文基于現(xiàn)有的遷移系統(tǒng)，然后根據(jù)第2節(jié)提出的可信虛擬機(jī)遷移的安全需求，將需求中所提的一些必要組件和流程體現(xiàn)在新的遷移框架中.本文主要是針對(duì)可信虛擬機(jī)的遷移流程進(jìn)行描述，所以遷移框架主要體現(xiàn)的是抽象的遷移組件之間的交互.

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

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

我們對(duì)圖3進(jìn)行說明：

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

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

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

圖3中的4個(gè)抽象實(shí)體通過不斷地交互來完成可信虛擬機(jī)遷移的操作，多個(gè)組件之間存在重復(fù)的交互，這種交互影響著遷移系統(tǒng)狀態(tài)在不斷地變化著，下面我們首先給出可信遷移系統(tǒng)和協(xié)議流程的抽象描述.

3.2遷移模型描述

基于2.2節(jié)中描述的基本框架與邏輯構(gòu)成，我們將可信遷移系統(tǒng)做抽象定義：

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

Table 1 Data Attributes and Definitions of Migration Protocol表1 遷移協(xié)議中的數(shù)據(jù)屬性和定義

Table 2 Action Attributes and Definitions of Migration Protocol表2 遷移協(xié)議中的動(dòng)作屬性和定義

為了更好地對(duì)遷移系統(tǒng)的全局狀態(tài)和原子動(dòng)作以及對(duì)應(yīng)的狀態(tài)變遷規(guī)則進(jìn)行描述，下面首先依據(jù)上述定義對(duì)整個(gè)遷移協(xié)議的流程進(jìn)行描述：

1) 建立安全會(huì)話

① 身份認(rèn)證

DH→SH：certificateDH；

SH，TTP：Authentication(certificateDH，TTP)；

SH→DH：certificateSH；

DH，TTP：Authentication(certificateSH，TTP)；

② 協(xié)商信道keychannel

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

③ 完整性驗(yàn)證

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) 數(shù)據(jù)傳輸

① 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

這里通過將可信遷移的部分安全需求體現(xiàn)在遷移的系統(tǒng)架構(gòu)中，然后將可信遷移系統(tǒng)抽象描述為4個(gè)實(shí)體之間的交互系統(tǒng)，一個(gè)遷移系統(tǒng)就能夠通過交互協(xié)議來進(jìn)行描述，并且其中的關(guān)鍵動(dòng)作還反映了系統(tǒng)的部分安全需求.基于交互協(xié)議中的關(guān)鍵動(dòng)作和狀態(tài)，我們就可利用標(biāo)號(hào)遷移系統(tǒng)對(duì)其進(jìn)行進(jìn)一步地形式化描述.

4 可信遷移系統(tǒng)的運(yùn)行狀態(tài)變遷模型

第3.2節(jié)已經(jīng)將可信遷移模型的執(zhí)行流程以協(xié)議的形式進(jìn)行描述，那么為了進(jìn)一步對(duì)遷移系統(tǒng)的關(guān)鍵動(dòng)作和狀態(tài)進(jìn)行動(dòng)態(tài)的描述，就需要開展對(duì)協(xié)議實(shí)現(xiàn)的動(dòng)態(tài)分析.根據(jù)自動(dòng)機(jī)原理，標(biāo)號(hào)遷移系統(tǒng)[16]是由起點(diǎn)、輸入標(biāo)識(shí)、終點(diǎn)組成的一個(gè)系統(tǒng)轉(zhuǎn)換模型.由于標(biāo)號(hào)遷移系統(tǒng)不完全等同于自動(dòng)機(jī)，它沒有固定的初始狀態(tài)和接受狀態(tài)，所以在標(biāo)號(hào)遷移系統(tǒng)中，任何一個(gè)狀態(tài)都可以作為初始狀態(tài)，故標(biāo)號(hào)遷移系統(tǒng)在動(dòng)態(tài)分析密碼協(xié)議實(shí)現(xiàn)的安全中具有一定的優(yōu)勢(shì).因此，我們采用標(biāo)號(hào)遷移系統(tǒng)對(duì)可信遷移系統(tǒng)的協(xié)議實(shí)現(xiàn)進(jìn)行描述.

4.1LTS相關(guān)定義

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

定義4. 狀態(tài)收斂.q∈Q，q表示狀態(tài)q的收斂，那么：

2) 如果q，則qε；

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

定義5. 強(qiáng)模擬.設(shè)(Q，T)為一個(gè)標(biāo)號(hào)遷移系統(tǒng)，并設(shè)S是一個(gè)Q上的二元關(guān)系.一旦pSq總有條件成立：

定義6. 擴(kuò)展的強(qiáng)模擬.設(shè)(Q，T)為一個(gè)標(biāo)號(hào)遷移系統(tǒng).(Q′，T′)也是一個(gè)標(biāo)號(hào)遷移系統(tǒng)，S在Q×Q′上是一個(gè)二元關(guān)系，且p，q∈Q.如果pSq滿足條件：

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

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

標(biāo)號(hào)遷移系統(tǒng)的部分相關(guān)符號(hào)定義如表3所示：

Table 3 Partial Symbols and Definitions in LTS表3 標(biāo)號(hào)遷移系統(tǒng)的部分符號(hào)和定義

4.2可信遷移組件狀態(tài)圖

任何協(xié)議都可以看成多個(gè)實(shí)體(或稱為進(jìn)程)之間的交互，而每個(gè)實(shí)體都可以通過標(biāo)號(hào)遷移系統(tǒng)來形式化地描述其行為和狀態(tài)，例如典型的端到端的通信協(xié)議AB協(xié)議[17]可以將其中的發(fā)送方S和接收方R當(dāng)成2個(gè)進(jìn)程分別描述成LTS樹，如圖4所示，根據(jù)樹形表示可以很容易得到它們的行為和狀態(tài)轉(zhuǎn)換.

Fig. 4 Process state of AB protocol圖4 AB協(xié)議進(jìn)程狀態(tài)圖

根據(jù)上述方法，我們首先將3.1節(jié)中定義的遷移主體作為協(xié)議系統(tǒng)中的4個(gè)進(jìn)程分別進(jìn)行LTS樹建模，將這些進(jìn)程作為遷移模型的組件，每個(gè)組件的LTS狀態(tài)圖都可以當(dāng)成遷移整體架構(gòu)狀態(tài)圖的一個(gè)組成部分.根據(jù)遷移系統(tǒng)的特點(diǎn)，我們將SH,DD,TTP和SSH之間的通信過程定義為系統(tǒng)的可觀察動(dòng)作，而它們內(nèi)部組件的處理過程為系統(tǒng)不可觀察的內(nèi)部動(dòng)作，各組件主要包含交互規(guī)則：

1)SH負(fù)責(zé)發(fā)起建立安全會(huì)話的請(qǐng)求，通過與TTP和DH交互信息來驗(yàn)證目的主機(jī)的當(dāng)前安全狀態(tài).驗(yàn)證通過之后開始傳輸遷移數(shù)據(jù)，并根據(jù)傳輸過程中出現(xiàn)問題與否決定下一步的對(duì)剩余遷移數(shù)據(jù)的處理并進(jìn)行收尾工作，例如遷移數(shù)據(jù)成功之后，源主機(jī)刪除本地所有和遷移虛擬機(jī)相關(guān)的數(shù)據(jù).

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

3)TTP主要負(fù)責(zé)存儲(chǔ)遷移雙方的證書以及度量基準(zhǔn)值等可信信息，通過與遷移雙方交互來提供可信服務(wù).

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

根據(jù)4條規(guī)則，我們可信遷移協(xié)議中的發(fā)送進(jìn)程SH和接收進(jìn)程DH以及2個(gè)協(xié)調(diào)進(jìn)程TTP和SSH進(jìn)程分別描述成LTS樹，如圖5所示:

Fig. 5 The process state of trusted migration protocol圖5 可信遷移協(xié)議進(jìn)程狀態(tài)圖

4.3可信遷移系統(tǒng)整體狀態(tài)變遷模型

Fig. 6 LTS model of trusted migration system圖6 可信遷移系統(tǒng)的LTS模型

4.2節(jié)中的進(jìn)程組件狀態(tài)圖描述的是遷移過程中系統(tǒng)的主要組件的狀態(tài)變化，為了能夠準(zhǔn)確反映系統(tǒng)整體的動(dòng)態(tài)屬性，比如在可信遷移過程中執(zhí)行不同關(guān)鍵操作時(shí)進(jìn)程之間相互作用的反饋以及系統(tǒng)在某時(shí)刻的整體狀態(tài)等.因此，有必要根據(jù)可信協(xié)議整體流程的行為和狀態(tài)，結(jié)合3.2節(jié)中的各個(gè)進(jìn)程組件的描述刻畫出系統(tǒng)運(yùn)行時(shí)的狀態(tài)變遷圖LTS(P).

在交互行為集的基礎(chǔ)上，綜合上述組件模型以及變遷規(guī)則(見附表A1)，我們就可以進(jìn)一步刻畫出遷移系統(tǒng)運(yùn)行時(shí)的狀態(tài)變遷圖，為了與遷移流程對(duì)應(yīng)，我們將整體的LTS樹劃分為3個(gè)階段：

1) 圖6(a)表示系統(tǒng)在建立安全會(huì)話階段的狀態(tài)變遷圖，P0表示遷移系統(tǒng)的初始狀態(tài)，未開始遷移之前的任何異常錯(cuò)誤都可能導(dǎo)致系統(tǒng)回到初始狀態(tài).系統(tǒng)經(jīng)過一些安全遷移條件的判別來確認(rèn)系統(tǒng)是否滿足安全會(huì)話的條件.

2) 在系統(tǒng)狀態(tài)滿足所有的安全遷移判別條件之后，即建立起遷移主機(jī)雙方的安全會(huì)話達(dá)到如圖6(b)所示狀態(tài)P6.在開始內(nèi)存預(yù)拷貝之前，系統(tǒng)還需要根據(jù)當(dāng)前的系統(tǒng)配置和參數(shù)進(jìn)行一些準(zhǔn)備工作.

3) 內(nèi)存預(yù)拷貝結(jié)束之后開始執(zhí)行內(nèi)存的迭代傳輸，這些都屬于系統(tǒng)的內(nèi)部不可見動(dòng)作.如圖6(c)所示，在虛擬機(jī)所有數(shù)據(jù)傳輸結(jié)束之后，系統(tǒng)根據(jù)虛擬機(jī)是否成功恢復(fù)運(yùn)行執(zhí)行相應(yīng)的操作，如果遷移失敗，系統(tǒng)可能會(huì)恢復(fù)到遷移之前的狀態(tài).

根據(jù)可信遷移的相關(guān)安全需求和協(xié)議規(guī)則，圖6描述了遷移系統(tǒng)在4個(gè)主要參與實(shí)體的影響下的狀態(tài)變遷關(guān)系.因?yàn)楦鶕?jù)具體的實(shí)現(xiàn)和人為的設(shè)定，遷移系統(tǒng)的動(dòng)作的集合是會(huì)發(fā)生變化的，為了能夠通用且準(zhǔn)確地測(cè)試遷移系統(tǒng)，需要確定遷移過程中通用的可觀察狀態(tài)，即說明系統(tǒng)的狀態(tài)是收斂，LTS(P)不存在狀態(tài)變遷和內(nèi)部動(dòng)作的無窮組合，因此，我們提出命題和證明：

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

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

證畢.

命題1說明了我們定義的遷移系統(tǒng)運(yùn)行狀態(tài)是收斂的，即不存在無窮的狀態(tài)變遷和內(nèi)部變化，這也滿足了具體遷移實(shí)現(xiàn)需求，即從遷移初始狀態(tài)開始，系統(tǒng)能夠經(jīng)過有限的狀態(tài)變遷，達(dá)到預(yù)期的收斂狀態(tài)，不會(huì)出現(xiàn)一些無意義的導(dǎo)致系統(tǒng)出現(xiàn)死鎖等狀態(tài)的中間狀態(tài).由此可證明模型的建立是符合需求規(guī)則的.

4.4狀態(tài)樹約減

通常一個(gè)系統(tǒng)或協(xié)議在實(shí)際運(yùn)行過程中不是一成不變的，這和系統(tǒng)的設(shè)計(jì)和運(yùn)行環(huán)境都有密切的聯(lián)系，但是在符合規(guī)范的前提下，系統(tǒng)必然有一些必達(dá)的運(yùn)行狀態(tài)，這些狀態(tài)之間的路徑都是受相關(guān)的安全規(guī)則所約束的，因此，為了提升測(cè)試的效率和可靠性，我們可以對(duì)4.3中的LTS樹進(jìn)行約減.

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

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

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

5 模型的應(yīng)用與分析

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

5.1協(xié)議一致性測(cè)試

協(xié)議一致性測(cè)試主要包含2個(gè)方面[17]：測(cè)試生成和測(cè)試執(zhí)行.測(cè)試生成通過分析協(xié)議說明來確定要測(cè)試的各個(gè)方面，從而產(chǎn)生測(cè)試套(測(cè)試?yán)?；測(cè)試執(zhí)行部分分為測(cè)試?yán)倪\(yùn)行提供環(huán)境，并分析測(cè)試結(jié)果，給出測(cè)試判決.本文針對(duì)可信遷移系統(tǒng)所描述的LTS(P)即可作為一致性測(cè)試中的測(cè)試?yán)?利用第4節(jié)的LTS建模方法，我們可將任意的遷移協(xié)議或系統(tǒng)i描述成LTS(I)樹，我們將其稱為測(cè)試對(duì)象.通過將本文模型與其他模型進(jìn)行比較，即將LTS(P)與LTS(I)進(jìn)行一致性測(cè)試，驗(yàn)證協(xié)議i對(duì)應(yīng)模型所有的與本文定義的可觀察動(dòng)作有哪些是匹配的又有哪些是不在LTS(P)所定義的規(guī)則內(nèi)的.例如假設(shè)LTS(I)對(duì)應(yīng)遷移系統(tǒng)沒有考慮TPM密鑰的遷移，那么其LTS樹中肯定沒有與LTS(P)的P14所匹配的狀態(tài)和路徑，那么反過來說明通過本模型確實(shí)能夠發(fā)現(xiàn)其他遷移系統(tǒng)中的缺陷.

根據(jù)“一致性”的定義[17]，我們將測(cè)試中使用的遷移協(xié)議形式化說明集合記為MIGSPECS，將協(xié)議實(shí)現(xiàn)的集合記為MIGIMPS，它們之間的關(guān)系記為imp，其定義為

imp?MIGSPECS×MIGIMPS，

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

命題2. 存在一個(gè)測(cè)試?yán)齃TS(P)和一個(gè)測(cè)試對(duì)象LTS(I)，測(cè)試套T是測(cè)試?yán)囊粋€(gè)集合，?i∈LTS(I)，若i能夠通過T，則存在impLTS?LTS(P)×LTS(I).

證明. 如果i能夠通過T，那么存在LTS(P)∈T，i能夠通過測(cè)試?yán)齃TS(P)，那么就存在協(xié)議說明p∈LTS(P)，使得i能夠通過p，根據(jù)上述“一致性”的定義，因此就存在協(xié)議說明和協(xié)議實(shí)現(xiàn)之間的一致性關(guān)系，即存在(p，i)∈imp，那么對(duì)于p∈LTS(P)，i∈LTS(I)，就存在impLTS?LTS(P)×LTS(I).命題2得證.

證畢.

命題2說明了在測(cè)試?yán)齃TS(P)滿足一定條件的情況下，可以通過協(xié)議的一致性測(cè)試來證明測(cè)試?yán)c其他協(xié)議實(shí)現(xiàn)的LTS的一致性關(guān)系.需要注意的是，實(shí)際測(cè)試一般不能證明一致性，而只能證明某些協(xié)議實(shí)現(xiàn)與協(xié)議說明不一致[17].由于目前可信遷移系統(tǒng)還沒商業(yè)化或者開源的實(shí)際系統(tǒng)的應(yīng)用，因此還無法對(duì)真實(shí)的系統(tǒng)進(jìn)行測(cè)試，但是通過本節(jié)的分析已經(jīng)說明了測(cè)試的可行性，后續(xù)我們也將基于本文的模型和方法開展對(duì)仿真系統(tǒng)中可信遷移系統(tǒng)的測(cè)試，為今后真實(shí)的平臺(tái)測(cè)試打下良好的基礎(chǔ).

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

命題3. 如果去除可信遷移流程中的非關(guān)鍵部分，且簡(jiǎn)化前后協(xié)議的安全屬性具有一致性，那么在分析評(píng)估系統(tǒng)的安全狀態(tài)遷移時(shí)，簡(jiǎn)化的流程可以等價(jià)于原系統(tǒng).

證畢.

5.2與現(xiàn)有模型對(duì)比

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

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

本文基于上述研究成果，總結(jié)和分析了可信虛擬機(jī)遷移的安全需求，并且還考慮了目前可信計(jì)算和云平臺(tái)結(jié)合的發(fā)展現(xiàn)狀，因此，綜合來看本文所建模型考慮的安全屬性還是較為全面和符合真實(shí)應(yīng)用場(chǎng)景的，能夠較完整地體現(xiàn)可信遷移系統(tǒng)的安全需求.

6 總 結(jié)

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

[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)

(楊永嬌, 嚴(yán)飛, 毛軍鵬, 等. Ng-vTPM: 新一代TPM虛擬化框架設(shè)計(jì)[J]. 武漢大學(xué)學(xué)報(bào): 理學(xué)版, 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)

(熊海泉, 劉志勇, 徐衛(wèi)志, 等. VMM中Guest OS非陷入系統(tǒng)調(diào)用指令截獲與識(shí)別[J]. 計(jì)算機(jī)研究與發(fā)展, 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)

(萬濤, 劉遵雄, 馬建峰. 多服務(wù)器架構(gòu)下認(rèn)證與密鑰協(xié)商協(xié)議[J]. 計(jì)算機(jī)研究與發(fā)展, 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 虛擬化動(dòng)態(tài)遷移技術(shù)的安全防護(hù)模型[J]. 軟件學(xué)報(bào), 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)

(蔣凡, 寧華中. 基于標(biāo)號(hào)變遷系統(tǒng)的測(cè)試集自動(dòng)生成[J]. 計(jì)算機(jī)研究與發(fā)展, 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)

(徐明迪, 張煥國(guó), 嚴(yán)飛. 基于標(biāo)記變遷系統(tǒng)的可信計(jì)算平臺(tái)信任鏈測(cè)試[J]. 計(jì)算機(jī)學(xué)報(bào), 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)

(趙波, 戴忠華, 向騻, 等. 一種云平臺(tái)可信性分析模型建立方法[J]. 軟件學(xué)報(bào), 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