基于擴展LS2的可信虛擬平臺信任鏈分析

常德顯，馮登國，秦宇，張倩穎,2

（1.中國科學(xué)院 軟件研究所，北京 100190；2.中國科學(xué)院 研究生院，北京 100049；3.解放軍信息工程大學(xué) 三院，河南 鄭州 450004）

1 引言

虛擬化技術(shù)因具有節(jié)省成本、提高效率等特有優(yōu)勢使其得以快速應(yīng)用推廣，比如，在云計算等大型計算應(yīng)用環(huán)境中，虛擬化平臺已經(jīng)成為承擔海量計算和應(yīng)用服務(wù)的基礎(chǔ)。但隨之而來的一個關(guān)鍵問題就是如何為虛擬化平臺提供服務(wù)可信的保障，用戶在使用虛擬化平臺提供的資源和服務(wù)時，亟需確認該服務(wù)平臺是否可信任。可信計算技術(shù)基于硬件信任根，能夠為平臺構(gòu)建從底層硬件到上層應(yīng)用程序的信任鏈，并結(jié)合度量與遠程證明機制為外部提供可信證明[1]，從而為平臺提供可信運行環(huán)境保障，因此，利用可信計算技術(shù)構(gòu)建可信虛擬平臺（TVP,trusted virtualization platform）環(huán)境并對其信任進行驗證成為目前的研究熱點。

針對虛擬化平臺多用戶操作系統(tǒng)實例，即多個虛擬機（VM, virtual machine）并發(fā)運行于同一物理平臺的需求，Stefan Berger[2]等人首先提出虛擬信任根（vRT, virtual root of trust）、虛擬可信平臺模塊（vTPM, virtual trusted platform module）的思想，通過為每個虛擬機提供獨立的虛擬信任根來構(gòu)建實現(xiàn)虛擬化可信平臺的原型系統(tǒng)。HP和IBM的研究人員在虛擬信任根的基礎(chǔ)上，分別提出各自的TVP概念[3,4]，并針對不同應(yīng)用需求建立用戶可定制TVP，他們的工作大大推動了 TVP，并使其在云計算環(huán)境中得到應(yīng)用[5,6]?？尚牌脚_需要提供其信任證明，為此，需要對構(gòu)建平臺信任的基石——信任鏈進行形式化建模與分析，以確保平臺信任的可驗證。陳書義等人利用一階邏輯對可信計算平臺啟動過程進行建模以分析其信任傳遞過程[7]，并提出長度受限的信任鏈模型。張興等人基于無干擾模型對信任鏈進行了建模分析[8]，從系統(tǒng)信息流控制角度驗證滿足傳遞無干擾安全策略的信息流才能構(gòu)建有效的信任鏈。為了驗證本地的信任屬性，需要利用遠程證明協(xié)議對遠程驗證方提供驗證。馮登國等[9,10]基于國際可信計算組織（TCG, Trusted Computing Group）的遠程證明方案，提出改進的遠程證明協(xié)議，并給出了基于可證明安全的形式化分析。這些針對平臺信任進行的形式化的分析與驗證工作，在一定程度上豐富了平臺信任鏈理論模型，為平臺信任證明提供有力支撐。

但是，上述方法主要針對普通可信計算平臺，并不能直接適用于TVP。目前，TVP的信任鏈模型形式化分析主要存在以下問題。

1) 缺乏統(tǒng)一的TVP及其信任鏈的抽象模型。目前，考慮到不同的功能需求，已有的多個TVP研究方案分別側(cè)重于不同的信任傳遞過程，導(dǎo)致它們在實現(xiàn)時也存在一定的差異，比如傳統(tǒng)解決方案[2～4,6]以及Jonathan M McCune等人提出利用新的處理器機制為虛擬化平臺提供動態(tài)信任鏈構(gòu)建的方案[11]等，這些方案分別給出針對相應(yīng)平臺的特定信任鏈模型，不具有普遍性，而且各個已有模型并未給出從底層虛擬機系統(tǒng)到虛擬信任根，再到用戶虛擬機的完整信任鏈。為了全面、有效地分析TVP信任鏈，需要建立一種統(tǒng)一的TVP及其完整信任鏈的抽象模型，以明確定義信任鏈傳遞過程應(yīng)滿足的信任屬性。

2) 缺乏針對TVP信任鏈分析的形式化方法。一方面，已有的形式化分析方法主要關(guān)注通信協(xié)議的安全性分析，比如 BAN邏輯[12]、應(yīng)用π演算[13]等，它們不適合應(yīng)用系統(tǒng)內(nèi)部程序的安全性分析（比如 TVP信任鏈傳遞屬性等），而且現(xiàn)有針對可信平臺信任鏈的形式化分析通?；蛘邆?cè)重于本地信任鏈的構(gòu)建與驗證[7,8]，或者側(cè)重于信任屬性的遠程證明[9,10]，因此不夠全面且不具有普適性；另一方面，由于虛擬化平臺的特性（如多虛擬機并發(fā)、內(nèi)存隔離、訪問控制等），使得針對普通可信平臺的分析方法不能直接應(yīng)用于TVP。為此，需要研究針對TVP信任鏈屬性形式化分析的新方法。

本文針對上述問題，首先建立了TVP及其完整的信任鏈模型，并詳細定義了TVP信任鏈的信任屬性。與已有只針對特定TVP實現(xiàn)的模型相比，該模型更為抽象，摒棄了平臺具體的實現(xiàn)方案（比如硬件信任根與虛擬信任根的映射關(guān)系建立等），涵蓋了普通可信平臺信任鏈及虛擬化平臺特有的上層用戶虛擬機的信任鏈。然后根據(jù)TVP信任鏈的分析需求，對安全系統(tǒng)邏輯（LS2, logic of secure system）的語法、語義及證明規(guī)則進行針對性擴展，并對這種規(guī)則擴展給出嚴格的正確性證明。最后，基于擴展LS2形式化驗證了TVP信任鏈有條件地滿足傳遞過程的正確性、唯一性，對實例系統(tǒng)信任鏈的分析表明本文提出的信任鏈模型的通用性及擴展LS2方法的有效性。

2 TVP及其信任鏈建模

本文主要針對 TVP信任鏈傳遞的形式化分析，因此不考慮虛擬化平臺自身的固有安全機制，比如虛擬機監(jiān)控器（VMM，virtual machine monitor）的特權(quán)操作、虛擬機之間的隔離及內(nèi)存操作控制等，可參考Gilles Barthe等給出的形式化描述與分析[14]。

2.1 TVP信任模型

HP、IBM等研究機構(gòu)都針對虛擬化環(huán)境提出并構(gòu)建了相應(yīng)的 TVP[2～4]，但這些研究主要側(cè)重于具體應(yīng)用場景的功能實現(xiàn)，缺乏一種抽象、通用的TVP定義。TVP在物理上體現(xiàn)為一個支持虛擬化技術(shù)的可信主機，它與普通可信計算平臺的區(qū)別主要在于：1）擁有構(gòu)建于硬件可信芯片可信平臺模塊（TPM, trusted platform module）基礎(chǔ)上的虛擬信任根；2）并發(fā)地為多個客戶應(yīng)用虛擬機提供信任環(huán)境?；谝延醒芯糠桨?，本文給出如圖 1所示的TVP基本運行架構(gòu)。

從功能上看，TVP主要分為4個層次，硬件信任根TPM作為最底層，是平臺信任的物理保障。第二層主要包括VMM 及管理域（主要是其內(nèi)核及相關(guān)域管理工具，簡記為 admindomker），它們通常被認為是TVP的可信計算基（TCB，trusted computing base）。第三層是vRT，由于實現(xiàn)方案不同（如圖1中a、b所示），其加載過程可能是傳統(tǒng)信任鏈的一部分，或直接利用動態(tài)加載機制如動態(tài)度量信任根（DRTM，dynamic root of trusted measurement）機制啟動，這使得它或者成為 TCB的一部分，或者作為應(yīng)用進程單獨存在。最上層是用戶虛擬機，是與用戶應(yīng)用密切相關(guān)的部分。基于上述分析，本文從功能角度給出以下TVP的抽象定義。

圖1 TVP基本運行架構(gòu)

定義1TVP是具有可信功能的虛擬化計算平臺，它主要包含2類功能組件：TVP:={M,RT}，其中，M 表示虛擬化平臺所有主機類型集合，包括構(gòu)成虛擬化平臺的基本組件VMM、管理域及用戶虛擬機等，它們是利用虛擬化技術(shù)為用戶提供資源與服務(wù)的主體；信任根（RT，root of trust）是構(gòu)建TVP信任環(huán)境的基礎(chǔ)，也是TVP的核心組件，對虛擬化平臺來說，它包括硬件可信芯片TPM和vRT。

對于TVP的主機M，根據(jù)其類型進一步細化為 M:={m,vm}，其中，m:={vmm, admindomker}，特指底層的VMM及admindomker，它們是TVP的TCB的主要組成部分。vm:={vm1,…,vmn}，表示虛擬化平臺上層的用戶虛擬機vm集合** 如無特別說明，本文所使用的vm均泛指任意用戶i的虛擬機 vmi。。

相似地，TVP的信任根也進一步分類為RT:={TPM, vRT}，其中，TPM 是硬件信任根，主要用于為物理平臺提供信任保障，它擁有非易失存儲及密鑰存儲等固有特性；vRT在功能實現(xiàn)上可表現(xiàn)為m中內(nèi)核組件或獨立的可信組件，這里將其抽象為一個獨立功能組件，通過特定的映射關(guān)系與硬件信任根TPM關(guān)聯(lián)以確保其可信性，即vRT依賴于TPM，它以軟件形式體現(xiàn)，用于為上層用戶虛擬機提供信任保障。

因此，TVP從功能角度可定義為 TVP:={(m,TPM), (vm1, vRT1),…,(vmn, vRTn)}，其中，m必須使用TPM來構(gòu)建信任，而虛擬機vm則是利用其相應(yīng)的vRT來構(gòu)建信任。

2.2 TVP信任鏈及其信任屬性

TCG組織從實體行為預(yù)期性角度給出可信的定義，并采用裝載前度量的方案，給出了信任鏈傳遞和控制權(quán)轉(zhuǎn)移的過程。與普通可信計算平臺類似，TVP的信任鏈同樣需要保障平臺能夠基于信任根，通過逐級的信任傳遞，構(gòu)建虛擬化平臺的可信運行環(huán)境。由于虛擬化平臺自身的特殊性，它要求并發(fā)地執(zhí)行多個用戶虛擬機實例，因此，其信任鏈與普通可信平臺的信任鏈存在不同（如圖1所示）。根據(jù)定義1可知，TVP的信任鏈不僅包括普通可信平臺從第一層到第二層的信任傳遞（主機 m），還要增加之后的第三層vRT與第四層用戶虛擬機的信任傳遞，而且第四層中的用戶虛擬機還需要多個實例并發(fā)執(zhí)行，使得信任傳遞會出現(xiàn)多個不同分支，這與可信計算最初構(gòu)建信任環(huán)境的思想并不一致。

為了確保這種信任傳遞的正確性，需要對TVP信任鏈進行形式化驗證，證明在程序控制權(quán)傳遞過程中，各個進程的確能夠按照預(yù)期執(zhí)行，整個過程不存在信任缺失（比如存在其他程序執(zhí)行、加載等情況），而且能夠?qū)ν庾C明上述屬性。本文將上述驗證目標抽象為信任鏈的信任屬性（TP, trusted property），這種信任屬性的驗證包括2個方面，一方面是信任鏈在本地平臺構(gòu)建過程中的唯一性、正確性驗證，另一方面是平臺向外部實體R證明自己確實構(gòu)建了該信任鏈。其抽象定義如下。

定義2（TVP信任鏈的信任屬性TPTVP） TVP的信任屬性定義為一個二元組 TPTVP:={TCTVP,VerTVP}，其中，TCTVP表示TVP信任鏈構(gòu)建時所包含的可信程序傳遞序列，VerTVP表示對該信任鏈執(zhí)行序列的遠程驗證。按照2.1節(jié)中對TVP中相應(yīng)功能組件的定義，該信任屬性可以進一步細化為TPTVP:={(TCm, TCvRT,TCvm),(Verm, VervRT, Vervm)}?？梢?，該信任屬性根據(jù)組件類型可分為3類：主機m的信任屬性TPm、vRT信任屬性TPvRT及用戶虛擬機的信任屬性TPvm。

1) 主機 m的信任屬性表示為 TPm:={TCm,Verm}，其中，TCm表示基于硬件信任根構(gòu)建的信任鏈，即主機 m在本地正確地完成從可信度量根（CRTM，core root of trust for measurement）到上層用戶應(yīng)用的可信啟動過程：(CRTM→BL→OS→App)TPM，且在信任傳遞過程中不存在其他程序代碼加載。Verm:=Verify(m,TCm)表示對外驗證主機 m所聲稱的信任屬性 TCm，使遠程驗證者確信TVP平臺主機m擁有這樣的信任鏈屬性TCm。

2) vRT的信任屬性為TPvRT:= {TCvRT,VervRT}，表示 vRT的本地可信加載及其對外的證明。需要注意的是，vRT的信任屬性與其實現(xiàn)方式密切相關(guān)（圖1中的a、b），它可能實現(xiàn)為一個微內(nèi)核系統(tǒng)或一個應(yīng)用進程，而且需要建立 vRT與硬件信任根之間的強依賴關(guān)系，以硬件信任根保障軟件vRT的可信。

3) vm的信任屬性與上述主機m的信任屬性類似，表示為TPvm:={TCvm,Vervm}，其中，TCvm:=(INIT→BL→OS→App)vRT，表示 vm的從初始啟動程序INIT開始的本地信任鏈傳遞過程。與 TVP平臺主機 m直接依賴于硬件信任根 TPM 有所不同,TCvm成立的關(guān)鍵是 vRT的正確加載。Vervm:=Verify(vm,TCvm)表示vm信任鏈的外部驗證。

上述可信屬性TPTVP的定義蘊含一個成立的前提，即 TVP信任鏈構(gòu)建過程一定是從主機m→vRT→vm。此外，vm的信任屬性TPvm必須依賴于TPvRT，即其信任屬性建立于硬件信任根與vRT之上，而 vRT的信任構(gòu)建還與其實現(xiàn)方案密切相關(guān)。在本文建立的TVP模型中，對vRT不同實現(xiàn)方案進行了抽象：如果是圖1中的a，則需要依賴于TPm，如果是圖1中的b，則依賴于DRTM機制。

3 LS2及其擴展

3.1 LS2基本組成及特點

2009年，CMU大學(xué)的Anupam Datta等人提出一種可擴展的 LS2，用于對安全應(yīng)用系統(tǒng)的安全屬性進行推理分析[15]。LS2基于協(xié)議組合邏輯（PCL，protocol composition logic），適合于對具有明確時序關(guān)系的復(fù)雜安全應(yīng)用系統(tǒng)（比如TVP）的安全屬性進行分析。

LS2主要由3部分組成：編程模型、LS2語義語法和LS2證明系統(tǒng)，其中，編程模型用于對安全應(yīng)用系統(tǒng)中的行為、參與主體等進行建模，比如基本的密碼學(xué)操作、內(nèi)存控制及程序跳轉(zhuǎn)等。LS2語義語法用于建立目標系統(tǒng)抽象的安全屬性，通常以模態(tài)公式A表示，該式的含義為：線程I在時間段(tb,te]順序地執(zhí)行程序P時，公式A成立。LS2的證明系統(tǒng)用于為上述抽象安全屬性提供形式化推理證明，是LS2的核心，需要對其正確性進行嚴格的證明。由于LS2語義直觀、便于擴展，而且不需要對敵手進行單獨建模，并支持對未知代碼加載執(zhí)行的推理，因此適合對復(fù)雜應(yīng)用系統(tǒng)安全屬性的分析驗證，具有廣闊的應(yīng)用前景。

目前，已有的形式化分析方法（比如 BAN邏輯、應(yīng)用π演算等）主要側(cè)重于對網(wǎng)絡(luò)系統(tǒng)通信協(xié)議的安全屬性進行建模分析，而對于應(yīng)用系統(tǒng)內(nèi)部程序的安全性分析支持不夠，尤其是無法分析那些影響系統(tǒng)安全的不可預(yù)知程序的加載行為（比如可信計算平臺信任鏈傳遞過程中的程序控制權(quán)轉(zhuǎn)移）。與這些方法相比，LS2的主要特點在于：1）語義簡單且具有可擴展性，該邏輯利用已有進程演算的方法，對密碼操作、并發(fā)進程之間的網(wǎng)絡(luò)通信等進行抽象，便于對安全應(yīng)用系統(tǒng)功能進行建模，而且可擴展新的安全操作，比如適用于可信計算環(huán)境中的平臺配置寄存器（PCR，platform configuration register）的擴展操作等；2）不需要專門對敵手行為進行推理分析，它將攻擊者作為程序執(zhí)行時的一個額外線程，在遵守邏輯系統(tǒng)規(guī)則與約定的條件下，隱式地與正常參與的線程并發(fā)執(zhí)行，證明系統(tǒng)確保違反安全屬性的可能攻擊者能夠被檢測；3）適合于對有時序規(guī)則的動態(tài)加載代碼執(zhí)行的行為分析，它利用新的不變量規(guī)則如程序跳轉(zhuǎn)Jump、重置Reset等來推理未知代碼動態(tài)加載的行為。

上述特點使得LS2非常適合用于對可信平臺信任鏈傳遞過程中程序加載的不可預(yù)知性進行分析驗證，因此，本文選擇LS2對TVP信任鏈進行分析驗證。

3.2 針對TVP的LS2擴展

由于已有 LS2是一種通用的系統(tǒng)安全屬性分析方法，其基本編程語言、語義語法等無法充分描述TVP的程序行為及其信任鏈模型，進而不能直接應(yīng)用該方法對相應(yīng)的信任屬性進行分析驗證。因此，本文基于第3節(jié)TVP的抽象模型及其信任鏈的信任屬性定義，對原始 LS2進行了如圖2所示的擴展。

1) 編程語言及操作語義的擴展

語義擴展主要是根據(jù)第2節(jié)中TVP的定義，對原有LS2中無法精確表示的主體對象進行進一步細化，主要包括主機、內(nèi)存及與主機相關(guān)的線程等。對于操作語義來說，需要新增有關(guān)vm的操作定義(Reset vm)和(Jump vm)，分別表示vm的重置和程序跳轉(zhuǎn)，其中，涉及到vm自身的初始啟動程序init以及內(nèi)存鎖定處理，相應(yīng)的推理規(guī)則在證明系統(tǒng)中進行擴展。本文將其作為一個特殊功能實體（單一程序）進行抽象，因此并未定義其內(nèi)部的跳轉(zhuǎn)操作，其 Reset操作也是作為一個單獨程序的重載來處理，因此不需要對操作語義進行新的擴展。

圖2 針對TVP平臺的LS2擴展

2) LS2語法擴展

由于在TVP中存在3種不同的主機實體，因此需要定義各自的Reset動作，需要注意的是，Reset(m)一定會導(dǎo)致Reset(vRT)和Reset(vm)，這也符合TVP的實際執(zhí)行過程。由于 Reset(vRT)和 Reset(vm)在TVP中可以各自獨立執(zhí)行，為了構(gòu)建vm的可信運行環(huán)境，必須滿足vRT先于vm啟動，且vm重啟時vRT保持正常運行而不能重啟。

3) 證明系統(tǒng)擴展

證明系統(tǒng)是LS2的核心，直接關(guān)系到安全屬性驗證過程的正確性、有效性。除了原有LS2中主機m 的 Reset、Jump規(guī)則，本文擴展定義了 vm 的Resetvm和Jumpvm規(guī)則。

Resetvm規(guī)則主要針對虛擬機的重啟。該規(guī)則表示的是在TVP中vm重新啟動后仍然保持其信任傳遞屬性（公式A）成立。該規(guī)則成立的前提條件是vRT在 vm啟動過程中未重新啟動，即?Reset

規(guī)則Jumpvm針對未知程序加載。該規(guī)則表示在TVP的vm中程序P在跳轉(zhuǎn)后仍然保持之前的可信屬性（公式A）成立，該規(guī)則成立的前提條件與Resetvm相同：，即 vRT未被重置。

本文對LS2的擴展主要包括2個方面，一方面是對 LS2編程語言、操作語義及語法進行的擴展，另一方面是對其證明系統(tǒng)的擴展。對編程語言、操作語義及語法的擴展主要是從應(yīng)用需求出發(fā)，對其能夠表述的語義進行豐富，這種擴展主要用于對 TVP信任鏈的安全屬性進行定義與描述，因此不需要對其進行正確性證明。由于安全屬性的分析驗證依賴于 LS2證明系統(tǒng)，證明系統(tǒng)的正確性與安全屬性驗證結(jié)論是否有效直接相關(guān)，因此，必須對上述擴展的 LS2證明系統(tǒng)（規(guī)則）提供嚴格的正確性、有效性證明，其詳細證明過程參見附錄。

4 TVP信任鏈分析

4.1 基本假定

在對 TVP信任鏈屬性分析之前本文假定以下條件是滿足的：1）TVP中涉及到的所有系統(tǒng)鏡像文件（包括主機 m及各個用戶虛擬機）的完整性未受破壞，且用戶虛擬機已預(yù)先植入所需的可信度量及證明代理；2）主機m支持動態(tài)加載DRTM技術(shù)，能夠為vRT提供動態(tài)的可信運行環(huán)境；3）vRT的平臺身份密鑰（AIK，attestation identity key）已得到可信第三方的認證并頒發(fā)證書，這里不考慮其具體實現(xiàn)方案（參見 vTPM[2]及 TrustVisor[11]等）；4）遠程驗證方案基于TCG組織給出的完整性報告協(xié)議，且在遠程挑戰(zhàn)者R與本地TVP之間已經(jīng)建立了安全信道。

根據(jù)定義1和定義2，本文對TVP信任鏈的信任屬性分析驗證主要包括 2部分：本地信任鏈構(gòu)建的驗證及該信任鏈的遠程驗證，如圖3所示。其中，對主機m和vRT（將其作為一個單獨的軟件組件擴展信任傳遞）的信任屬性證明可參考Anupam Datta等人[15]基于 LS2對普通可信計算平臺的可信屬性進行的分析過程。在此基礎(chǔ)上，本文重點對vm的信任鏈進行分析，一方面驗證在TVP中，利用vRT所構(gòu)建的本地vm的信任鏈是否唯一、正確；另一方面確保遠程挑戰(zhàn)者R能夠驗證該vm的確基于該信任鏈構(gòu)建了信任環(huán)境。

圖3 TVP的信任傳遞證明

4.2 信任鏈的本地驗證

1) 本地程序執(zhí)行

根據(jù)2.2節(jié)中TVP用戶虛擬機信任屬性TPvm定義，其信任鏈本地執(zhí)行過程中涉及到的程序如圖4所示。

圖4 TVP中vm信任鏈傳遞

程序執(zhí)行流程：首先確保vRT的正確加載并運行；然后vRT將控制權(quán)傳遞給初始程序INIT(vm)，它從虛擬機內(nèi)存地址 vm.bl_loc中讀取 Bootloader中的代碼b，將其擴展到一個虛擬PCR中（其中，m.vpcr.vm表示該虛擬機在這里存儲所有相關(guān)度量值，且該虛擬機的度量值存儲于主機m而不是vm）；之后執(zhí)行指令 Jumpb將控制權(quán)交給 Bootloader；Bootloader繼續(xù)按序從內(nèi)存vm.os_loc讀取OS的代碼o，將其擴展到 m.vpcr.vm，然后轉(zhuǎn)換控制權(quán)給OS；OS執(zhí)行相似的過程將控制權(quán)交給虛擬機的應(yīng)用代碼a。

在此過程中，要求 TVP的用戶虛擬機必須在vRT成功加載之后啟動，否則會導(dǎo)致在vRT啟動之前的 vm 無法使用該 vRT，將其表示為此外，TVP在啟動vm時，相應(yīng)的線程J對必須能夠?qū)Ξ斍皏m對應(yīng)的虛擬PCR值有鎖控制，這種控制對潛在的攻擊者也成立，表示為

由于vRT被抽象為一個單獨的軟件程序（無論其實現(xiàn)形式是獨立的輕量級可信執(zhí)行環(huán)境或僅是提供可信功能的應(yīng)用進程），利用 Latelaunch(m)動態(tài)加載機制確保其可信執(zhí)行，即JDRTM成立[15]。

2) 本地可信屬性描述及證明

根據(jù)上述信任鏈傳遞中程序執(zhí)行過程可知，最終體現(xiàn)vm信任鏈的是虛擬平臺的vPCR值，它與執(zhí)行程序之間存在唯一性、確定性映射。因此，基于定義2及上述映射關(guān)系，可將vm的本地信任傳遞屬性歸納為：如果最終的vPCR中度量值序列是正確的值，那么在該虛擬機上信任鏈所加載的程序順序就是正確的。即vm的本地信任傳遞屬性就是要求所有相應(yīng)啟動程序如Bootloader、OS、APP等都能按確定的先后順序加載。以擴展LS2將這種順序形式化表示為

上述公式表示：如果TVP的vm基于信任鏈構(gòu)建了本地信任環(huán)境，則其啟動過程一定是從 BL（Bootloader）跳轉(zhuǎn)到OS，而在此期間不會有其他程序執(zhí)行。這就需要證明上述程序啟動序列與vPCR值之間的一一映射關(guān)系?；谇拔牡募俣ㄇ疤?，要證明的信任鏈本地信任屬性如下。

定理1如果vRT加載（即JDRTM）成功，而且與該 vm啟動過程對應(yīng)的vPCR值為seq(INIT(vm),BL(vm),OS(vm),APP(vm))，那么該vm的本地信任鏈傳遞過程就是唯一的、正確的，即確定地從INIT(vm)到BL(vm)再到OS(vm)。該信任屬性形式化表示為成立，反復(fù)利用PCR公理即可直接得到在該序列中的所有子序列一定在時間t之前就出現(xiàn)在m.vpcr.vm中，即

接下來考慮圖4中程序執(zhí)行過程，最先執(zhí)行的操作是啟動vm，即Reset(vm,J)，然后vm利用vRT執(zhí)行第一個信任程序 INIT(vm)。利用圖 2中規(guī)則Resetvm，建立并證明程序 INIT(vm)的不變量：在某個時間tΒ，程序會跳轉(zhuǎn)到b且在其他時間不會有程序跳轉(zhuǎn)，內(nèi)存位置（即vPCR值）被該線程鎖定。即有以下屬性(1)成立

類似地，當程序跳轉(zhuǎn)并執(zhí)行 BL(vm)時，利用Jumpvm規(guī)則建立并證明 BL(vm)的不變量：在BL(vm)執(zhí)行后的某個時間點，程序必然跳轉(zhuǎn)到OS(vm)且期間不會有其他程序跳轉(zhuǎn)，即有以下屬性(2)成立

根據(jù)式(1)、式(2)可知，如果前提條件滿足，那么 vm 上執(zhí)行程序的順序一定是從 INIT(vm)到BL(vm)再到OS(vm)

定理1得證。

雖然上述證明過程未顯式地描述攻擊者的存在，但已經(jīng)蘊含著攻擊場景。比如，在INIT(vm)之后跳轉(zhuǎn)到b的過程中，由于b是從內(nèi)存vm.bl_loc讀取的，而該位置可能在之前已被攻擊者線程寫入其他程序，但可信計算技術(shù)提供的度量擴展機制使得能夠推理只有得到正確的內(nèi)存值時才能繼續(xù)運行下一個程序。同樣的，需要證明從b跳轉(zhuǎn)到o的正確性。利用LS2提供的Resetvm規(guī)則和Jumpvm規(guī)則，證明TVP上本地信任鏈傳遞的唯一性、正確性成立。

4.3 信任鏈的遠程驗證

TVP的vm需要向外部挑戰(zhàn)者證明自己所聲稱信任屬性，即其信任鏈傳遞過程中所執(zhí)行程序的確定序列，使外部挑戰(zhàn)者相信它的確按上述信任鏈構(gòu)建了可信執(zhí)行環(huán)境，需要證明 MeasuredBootSRTM(vm,t)成立。

1) 遠程驗證程序執(zhí)行

首先，根據(jù) TCG遠程證明協(xié)議規(guī)范及在虛擬化平臺中的實現(xiàn)[16,17]，給出vm信任傳遞的遠程驗證過程中涉及到的程序，如圖5所示。

圖5 TVP中虛擬機信任傳遞的遠程驗證程序

首先，vm讀取本地虛擬PCR值，用自己的AIK簽名并將其發(fā)送給挑戰(zhàn)者。然后，挑戰(zhàn)者驗證該簽名，并用預(yù)期的度量值序列與收到的值進行對比，如果匹配，則表明該vm擁有所聲稱的可信屬性，否則驗證失敗。在此過程中，vRT必須先于vm啟動以確保vm信任鏈建立，且遠程驗證者與vm應(yīng)是不同實體，以保證該驗證過程的有效性。

將這些前提條件形式化表示為

2) 信任鏈屬性的遠程驗證

根據(jù)遠程證明協(xié)議執(zhí)行流程，給出以下信任傳遞屬性的遠程證明目標。

定理2 如果遠程驗證者確認vm提供的度量值是唯一的、正確的，那么該vm對應(yīng)的PCR值一定是如下的確定序列seq(INIT(vm),BL(vm),OS(vm),APP(vm))，因為根據(jù)定理1可知，該序列表明該虛擬機的確執(zhí)行了相應(yīng)的信任鏈傳遞過程。形式化表示為

分別利用等值公理Eq和Read公理，有

此時需要判定e"的值，根據(jù)上述推理過程可知有2種可能：

即定理2屬性式(3)得證。利用屬性式(4)結(jié)論及定義1，可直接證明屬性式(4)成立。

根據(jù)上述證明可知，在TVP信任鏈構(gòu)建過程中，能夠有條件地保持其信任屬性，即構(gòu)建信任鏈所需要執(zhí)行的不同程序在跳轉(zhuǎn)過程中，不會被其他惡意代碼所控制或插入，從而不存在信任缺失的情況，且這種信任屬性能夠向遠程驗證者提供證明。

5 實例系統(tǒng)分析與討論

上述分析驗證過程是針對第 2節(jié)提出的 TVP抽象模型進行的，為了在實際系統(tǒng)中應(yīng)用本文的分析方法，選擇課題組已經(jīng)構(gòu)建的 TVP實例系統(tǒng)[18]（如圖6所示）并對其信任鏈進行分析。該實例系統(tǒng)基于XEN半虛擬化平臺，其中，vRT被實現(xiàn)為一個獨立的可信服務(wù)域（TSD, trusted service domain），以減輕虛擬化平臺管理域的運行負載。

根據(jù)第2節(jié)的通用TVP抽象模型，該實例系統(tǒng)信任鏈由3部分組成：第一部分如圖6中1)所示，即 m:={vmm, admindomker}的加載運行過程，主要包括 CRTM→BL→(VMM+OS)，由 TPM 為其提供信任保障。第二部分如圖6中2)所示，是由微內(nèi)核及其中的可信功能所構(gòu)成的TSD，由于TSD中只有內(nèi)核空間代碼，因此可將其看作獨立運行的可信軟件。第三部分是用戶虛擬機的運行（圖6中3)），其信任鏈與第2節(jié)中定義一致。

圖6 基于XEN的TVP實例系統(tǒng)

本文建立的通用抽象模型不關(guān)注具體系統(tǒng)實現(xiàn)細節(jié)，以上述實例系統(tǒng)為例，由于目前較新的DRTM機制對其保護的應(yīng)用有諸多限制，比如要求受保護的代碼自包含等，因此上述實例系統(tǒng)在實現(xiàn)時并未采用DRTM機制保障TSD的安全，而是將TSD作為admindomker之后加載的第一個應(yīng)用進程。這種實現(xiàn)上的調(diào)整不影響本文所建立的抽象模型，只需在推理時，將底層m原有信任鏈增加一個可信進程的控制傳遞節(jié)點即可，即將圖 4中的latelaunch(m)更改為TPMSRTM(m)[15]，相應(yīng)地在分析過程中增加從(VMM+OS)到TSD的不變量證明。可見，具體的系統(tǒng)實現(xiàn)僅是對推理細節(jié)的改變，本文所建立的抽象信任鏈模型及其信任屬性能夠滿足具體系統(tǒng)實現(xiàn)建模需求，不同的實現(xiàn)只需調(diào)整相應(yīng)推理細節(jié)。

在分析過程中，驗證了第 4節(jié)中為確保 TVP信任鏈的正確性所必須滿足的前提條件。結(jié)合上述實例系統(tǒng)討論如下。

1) 必須保障vRT自身的可信。在實例系統(tǒng)中，TSD作為vRT，其安全性直接關(guān)系到用戶虛擬機的信任鏈構(gòu)建。TSD作為特殊功能域，必須利用底層硬件信任根保證其可信性，即建立硬件信任根與TSD之間的強綁定關(guān)系。孤立的 TSD會使從(VMM+OS)到TSD的不變量不滿足，從而后續(xù)獲得運行權(quán)限的程序INIT(vm)不可信，導(dǎo)致vm信任鏈構(gòu)建失敗的結(jié)論。

為此，在實例系統(tǒng)中除了在TSD與TPM之間構(gòu)建了密鑰關(guān)聯(lián)關(guān)系之外，對主機m的信任鏈作了如下擴展：CRTM→BL→ (VMM+OS)→ TSD，以確保其VRT的TSD的可信加載。

2) 必須確保 vRT（即實例系統(tǒng)中的 TSD）先于用戶虛擬機加載運行。在分析過程中，如果有普通用戶虛擬機先于TSD啟動，則會導(dǎo)致推理過程中由于內(nèi)存鎖操作的失敗而無法證明程序跳轉(zhuǎn)時的不變量成立，這是由于產(chǎn)生了信任環(huán)路。此外，vm運行后的TSD重啟動操作（即Reset）會導(dǎo)致已有鎖定的PCR值不可信（比如丟失或被破壞），從而得出信任缺失的證明結(jié)論。

在實例系統(tǒng)中通過對 TSD加載運行的調(diào)度監(jiān)控來解決該問題。監(jiān)控進程位于實例系統(tǒng)的管理域內(nèi)核中，由于初始信任鏈能夠保證管理域內(nèi)核可信，從而保障監(jiān)控進程的可信，確保TSD正確的加載順序。

6 結(jié)束語

信任鏈是構(gòu)建TVP的基礎(chǔ)，但目前缺乏針對其信任傳遞正確性的形式化分析。為此，本文首次建立了抽象度更高的TVP完整信任鏈的模型，并詳細定義其應(yīng)滿足的信任屬性。擴展已有LS2的編程語言、語義語法和證明系統(tǒng)，并對這種擴展提供嚴格的正確性證明?；跀U展LS2對TVP鏈傳遞過程的正確性、唯一性進行了形式化分析驗證。對實例系統(tǒng)信任鏈的分析表明本文所建立模型的通用性及擴展LS2分析方法的有效性，并討論了TVP信任鏈為保持其信任傳遞屬性所必須滿足的前提條件。

TCG組織于2011年9月發(fā)布了虛擬可信平臺架構(gòu)規(guī)范[19]，為 TVP的設(shè)計與實現(xiàn)提供架構(gòu)性指導(dǎo)，但并未給出其信任鏈構(gòu)建及遠程證明的詳細方案，本文對此做出有意義的探索，滿足了TVP信任鏈形式化分析的需求，并為可信計算平臺的建模分析提供參考。未來將在此基礎(chǔ)上，研究基于擴展LS2的安全屬性自動化分析方法，進一步提高其分析效率。

附錄：LS2擴展規(guī)則的正確性證明

為了證明TVP信任鏈的信任屬性，本文對LS2的證明系統(tǒng)規(guī)則進行如下的擴展，2個規(guī)則各自含義及其正確性證明如下。

該規(guī)則的含義是：對于TVP的虛擬機來說，在其重新啟動過程中（INIT(vm)）如果沒有vRT重置事件(Reset(vRT))發(fā)生，則在虛擬機重新啟動之后，之前的屬性A依然成立。

證明

①與硬件信任根為單一平臺提供信任保障不同，TVP的 vRT需要為多個不同用戶虛擬機提供信任保障，用戶虛擬機的錯誤執(zhí)行可能導(dǎo)致信任的斷裂或環(huán)路。虛擬機vm的INIT(vm)表示其啟動過程中的程序序列，保持其信任屬性的前提是 vRT的正常運行，如果 vRT在此過程中發(fā)生重置Reset，就會導(dǎo)致相應(yīng)的信任傳遞斷裂，新運行的vRT就無法保證當前 INIT(vm)的正確性，進而無法確保安全屬性即不變量A的成立。因此，必須要求 ? Reset(vRT)on( tb, te)這一前提條件滿足。

②在①基礎(chǔ)上，分析需要證明的目標：對于任何時間點t0，都存在一個時間跡I滿足

2) J ump（ vm ）規(guī)則

該規(guī)則的含義是：對于虛擬化平臺中的虛擬機來說，如果某程序執(zhí)行時屬性A成立，在該程序跳轉(zhuǎn)后，如果vRT未重啟，則程序跳轉(zhuǎn)之前的屬性A依然成立。

證明

①與硬件信任根為普通可信平臺提供的可信功能一樣，vm中每一次程序跳轉(zhuǎn)過程都需要vRT對目標程序進行度量和擴展，因此，在vm中程序跳轉(zhuǎn)過程中，vRT必須能夠正確加載并提供信任功能，否則就無法保證vPRC中度量值的正確性，進而無法確保不變量公式A的成立。因此，在Jump規(guī)則的假設(shè)中，必須包含前提條件 ? Reset（ vR T ）on （tb,te） 。

[1] REINER S, XIAOLAN Z.Design and implementation of a TCG-based integrity measurement architecture[A].Proc of the 13th USENIX Security Symposium[C].Berkeley, USA, 2004.223-238.

[2] BERGER S, CACERES R, GOLDMAN K A,et al.VTPM: virtualizing the trusted platform module[A].Proc of the 15th USENIX Security Symposium[C].Berkeley, USA, 2006.305-320.

[3] CHRIS I D, DAVID P, WOLFGANG W,et al.Trusted virtual platforms:a key enabler for converged client devices[A].Proc of the ACM SIGOPS Operating Systems Review[C].New York, USA, 2009.36-43.

[4] BERGER S, RAMON C, DIMITRIOS P,et al.TVDc: managing security in the trusted virtual datacenter[A].Proc of ACM SIGOPS Operating Systems Review[C].New York, USA, 2008.40-47.

[5] KRAUTHEIM F J, DHANANJAV S P, ALAN T S.Introducing the trusted virtual environment module: a new mechanism for rooting trust in cloud computing[A].Proc of the 3rd International Conference on Trust and Trustworthy Computing[C].2010.211-227.

[6] 王麗娜，高漢軍，余榮威等.基于信任擴展的可信虛擬執(zhí)行環(huán)境構(gòu)建方法研究[J].通信學(xué)報, 2011, 32(9):1-8.WANG L N,GAO H J,YU R W,et al.Research of constructing trusted virtual execution environment based on trust extension[J].Journal on Communications, 2011, 32(9):1-8.

[7] CHEN S Y, WEN Y Y,ZHAO H.Formal analysis of secure bootstrap in trusted computing[A].Proc of the 4th International Conference on Autonomic and Trusted Computing[C].Berlin, Springer, 2007.352-360.

[8] 張興, 黃強, 沈昌祥.一種基于無干擾模型的信任鏈傳遞分析方法[J].計算機學(xué)報,2010,33(1):74-81.ZHANG X, HUANG Q, SHEN C X.A formal method based on noninterference for analyzing trust chain of trusted computing platform[J].Chinese Journal of Computers, 2010, 33(1):74-81.

[9] 馮登國，秦宇.可信計算環(huán)境證明方法研究[J].計算機學(xué)報, 2008,31(9):1640-1652.FENG D G, QIN Y.Research on attestation method for trust computing environment[J].Chinese Journal of Computers, 2008, 31(9):1640-1652.

[10] 馮登國，秦宇.一種基于 TCM 的屬性證明協(xié)議[J].中國科學(xué),2010,53(3):454-464.FENG D G, QIN Y.A property-based attestation protocol for TCM[J].Science China, 2010,53(3):454-464.

[11] JONATHAN M M, NING Q, LI Y L,et al.TrustVisor: ef fi cient TCB reduction and attestation[A].Proc of the IEEE Symposium on Security and Privacy[C].Oakland, USA, 2010.143-158.

[12] BURROWS M, ABADI M, NEEDHAM M R.A logic of authentication[A].Proc of the Royal Society[C].London, UK, 1989.233-271.

[13] ABADI M, FOURNET C.Mobile values, new names, and secure communication[A].Proc of the 28th Symposium on Principles of Programming Languages[C].London, ACM, 2001.104-115.

[14] GILLES B, GUSTAVO B, JUAN D C,et al.Formally verifying isolation and availability in an idealized model of virtualization[A].Proc of the 17th International Conference on Formal Methods[C].Berlin,Springer, 2011.231-245.

[15] DATTA A, FRANKLIN J, GARG D,et al.A logic of secure systems and its application to trusted computing[A].Proc of the 30th IEEE Symposium on Security and Privacy[C].Los Alamitos, USA, 2009.221-236.

[16] Trusted Computing Group.TCG infrastructure working group architecture part II-integrity management version 1.0[EB/OL].http://www.trustedcomputinggroup.org, 2006.

[17] CABUK S, CHEN L Q, PLAQUIN D,et al.Trusted integrity measurement and reporting for virtualized platforms[A].Proc of the International Conference on Trusted Systems[C].Berlin, Springer, 2010.180-196.

[18] CHANG D X, CHU X B, QIN Y,et al.TSD: a flexible root of trust for the cloud[A].Proc of the IEEE 11th International Conference on Trust,Security and Privacy in Computing and Communications[C].Liverpool.Springer, 2012, 119-126.

[19] Trusted Computing Group.Virtualized trusted platform architecture specification version 1.0 [EB/OL].http://www.trustedcomputinggroup.org.