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

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

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

1 引言

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

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

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

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

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

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

2 TVP及其信任鏈建模

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

2.1 TVP信任模型

HP、IBM等研究機構都針對虛擬化環境提出并構建了相應的 TVP[2～4]，但這些研究主要側重于具體應用場景的功能實現，缺乏一種抽象、通用的TVP定義。TVP在物理上體現為一個支持虛擬化技術的可信主機，它與普通可信計算平臺的區別主要在于：1）擁有構建于硬件可信芯片可信平臺模塊（TPM, trusted platform module）基礎上的虛擬信任根；2）并發地為多個客戶應用虛擬機提供信任環境。基于已有研究方案，本文給出如圖 1所示的TVP基本運行架構。

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

圖1 TVP基本運行架構

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

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

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

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

2.2 TVP信任鏈及其信任屬性

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

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

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

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

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

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

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

3 LS2及其擴展

3.1 LS2基本組成及特點

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

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

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

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

3.2 針對TVP的LS2擴展

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

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

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

圖2 針對TVP平臺的LS2擴展

2) LS2語法擴展

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

3) 證明系統擴展

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

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

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

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

4 TVP信任鏈分析

4.1 基本假定

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

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

圖3 TVP的信任傳遞證明

4.2 信任鏈的本地驗證

1) 本地程序執行

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

圖4 TVP中vm信任鏈傳遞

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

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

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

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

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

上述公式表示：如果TVP的vm基于信任鏈構建了本地信任環境，則其啟動過程一定是從 BL（Bootloader）跳轉到OS，而在此期間不會有其他程序執行。這就需要證明上述程序啟動序列與vPCR值之間的一一映射關系。基于前文的假定前提，要證明的信任鏈本地信任屬性如下。

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

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

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

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

定理1得證。

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

4.3 信任鏈的遠程驗證

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

1) 遠程驗證程序執行

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

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

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

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

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

根據遠程證明協議執行流程，給出以下信任傳遞屬性的遠程證明目標。

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

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

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

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

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

5 實例系統分析與討論

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

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

圖6 基于XEN的TVP實例系統

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

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

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

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

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

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

6 結束語

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

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

附錄：LS2擴展規則的正確性證明

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

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

證明

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

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

2) J ump（ vm ）規則

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

證明

①與硬件信任根為普通可信平臺提供的可信功能一樣，vm中每一次程序跳轉過程都需要vRT對目標程序進行度量和擴展，因此，在vm中程序跳轉過程中，vRT必須能夠正確加載并提供信任功能，否則就無法保證vPRC中度量值的正確性，進而無法確保不變量公式A的成立。因此，在Jump規則的假設中，必須包含前提條件 ? 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] 王麗娜，高漢軍，余榮威等.基于信任擴展的可信虛擬執行環境構建方法研究[J].通信學報, 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].計算機學報,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] 馮登國，秦宇.可信計算環境證明方法研究[J].計算機學報, 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 的屬性證明協議[J].中國科學,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.