滿足對應性屬性的平臺配置證明

徐明迪，高　楊，高雪原，張　帆

(1.武漢數字工程研究所，武漢 430205；　2.武漢輕工大學 數學與計算機學院，武漢 430023)(*通信作者電子郵箱whpuzf@whpu.edu.cn)

0　引言

遠程證明是可信計算提供的核心功能之一，能夠為云計算應用提供可信的計算環境。然而，遠程證明過程中的完整性度量、完整性存儲和完整性報告，都存在著不同程度的安全缺陷[1]。國內外眾多學者對完整性報告協議(Integrity Report Protocol, IRP)的安全性問題進行了廣泛研究[2]，發現該協議在抵御重放攻擊、篡改攻擊和假冒攻擊上存在安全缺陷。IRP包含了平臺身份證明和平臺配置證明(Platform Configuration Attestation, PCA)。在IRP的平臺配置證明研究方面，文獻[3-4]提出了IRP的平臺配置證明過程存在著平臺配置寄存器(Platform Configuration Register, PCR)可被任意讀寫操作，以及存儲度量日志(Stored Measurement Log, SML)可被任意修改的問題。在IRP形式化建模與驗證方面，Xu等[5]開發出了基于信息流完整性模型的遠程證明系統DR@FT，在CW-Lite模型的完整性度量框架基礎上，DR@FT將系統的可信性歸結為系統狀態變化的可信性。Arapinis等[6]用Horn子句對TPM的內部狀態寄存器PCR進行建模，并分析了PCR狀態的變化對BitLocker協議帶來的攻擊。Datta等[7]用LS2系統對靜態和動態完整性度量協議進行了形式化建模和證明。

文獻[8]圍繞授權策略給出了安全增強后的完整性報告協議，在協議應答者與平臺配置證明信息之間建立授權約束，解決包含全局攻擊者和局部攻擊者對IRP的平臺配置證明發起的四類攻擊，并通過原型系統進行了有效驗證，該文側重通過增加授權auth防止PCR和SML的篡改和假冒導致破壞平臺配置證明過程的攻擊。針對PCR和SML的篡改和假冒問題，文獻[4]通過安全進程代數對可信計算平臺內部子系統之間的安全可復合性進行了理論證明，得出了一些有意義的結論，但未對授權操作對應的理論問題進行探討。

IRP的參與方包括挑戰者和應答者，本文根據攻擊者所在位置的不同，將攻擊者分為全局攻擊者和局部攻擊者：全局攻擊者通過截獲、篡改、重放等攻擊手段對挑戰者或應答者進行中間人攻擊、偽裝攻擊和平臺配置隱私竊取等；局部攻擊者對應答者所在平臺的完整性度量架構(Integrity Measurement Architecture， IMA)和可信平臺模塊(Trusted Platform Module， TPM)發起攻擊，包括度量與加載時間差(Time of Check Time of Use, TOCTOU)攻擊、信任鏈攻擊和TPM硬件攻擊等[9]。針對IRP中的平臺配置證明存在的安全問題，為從理論上分析和解決該問題，本文擬從對應性屬性出發進行安全形式化驗證：首先對形式化描述語言StatVerif進行語法擴展，增加與完整性度量相關的構造和析構算子；然后基于對應性屬性給出局部和全局攻擊者的形式化描述，以及全局可靠和局部可靠的條件；最后通過對攻擊者能力進行建模，用形式化驗證工具Proverif對IRP的對應性進行證明，得出有意義的命題結論。

1　StatVerif語法擴展

StatVerif演算是對應用π演算的擴展[10]，在其基礎上通過新擴展的狀態進程對全局狀態變量進行描述，能夠對存在全局狀態的安全協議和系統進行建模。在StatVerif演算中，進程由項和進程算子構造而成。其中，項是用來表示數據，包括變量、名字、構造算子和析構算子。構造算子f(M1,M2,…,Mn)能夠根據一些已知項構造出新項。析構算子letx=g(M1,M2,…,Mn) inPelseQ表示進行析構操作g(M1,M2,…,Mn)，若成功則用析構結果替換進程P中所有x的出現后再運行進程P，否則運行進程Q。對于敵手attacker來說，若attacker已知消息m和公鑰pk，那么構造算子pencrypt為attacker(m)∧attacker(pk) ? attacker(pencrypt(m,pk))，相應地，析構算子pdecrypt為attacker(pencrypt(m,pk(sk)))∧attacker(sk) ? attacker(m)。

與ProVerif相同，StatVerif演算中與密碼相關的操作是通過構造子和析構子完成的，除了密碼學函數外，本文擴展了與平臺配置證明相關的構造算子，見表1。readpcr(x)表示讀取TPM中第x個PCR的值；extendpcr(x,y)表示用y對TPM的第x個PCR進行迭代；readsml(x)表示讀取SML中第x個eventlog結構；logsml(x)表示用eventlog結構x對SML進行追加；eventlog(x1,x2,y1,y2,z)表示構造出一個新的eventlog結構，(x1,x2,y1,y2,z)分別表示PCR索引、事件類型、事件摘要、事件長度和事件數據。

表1　與完整性度量相關的構造算子Tab. 1　Constructors for integrity measurement

與完整性度量相關的析構算子見表2。其中：前5條規則表示通過元組操作從事件日志中獲取單個項；calsml()表示從SML中獲取PCRi對應的eventlog結構并對其進行迭代計算；checkevent()表示對SML的單個eventlog結構進行驗證；checksml()表示對PCR和SML進行驗證。

表2　與完整性度量相關的析構算子Tab. 2　Destructors for integrity measurement

ProVerif是能夠接收應用π演算作為輸入的自動定理證明工具，已被用于驗證各種安全協議和安全系統的安全屬性，包括可達屬性(reachability properties)、一致性斷言(correspondence assertions)和可觀察等價性(observational equivalence)，這些有助于分析秘密性屬性和認證性屬性(secrecy and authentication properties)。文獻[10]指出：ProVerif是有效的，如果ProVerif驗證了安全協議滿足安全性質，則安全協議不存在實際的攻擊序列；同時ProVerif是不完備的，可能產生誤報(false attack)，但是實驗證明在實際使用中ProVerif誤報率很低，并且ProVerif輸出非常詳細，適用于檢查是否有誤報發生。

2　平臺配置證明安全

2.1　局部攻擊和全局攻擊

Sailer等[11]提出的完整性報告協議見表3，應答者PB為了向挑戰者PA證明平臺身份和平臺配置完整性，需要經過一系列的協議交互，其中nonce為不可預知的隨機數，AIKpriv和AIKpub為證明身份密鑰對，loadkey(AIKpriv)表示從可信平臺模塊TPM中裝載證明身份密鑰AIKpriv,SML為平臺完整性度量的存儲日志，cert(AIKpub)為PrivacyCA向平臺簽發的AIKpub證書，sign{PCR,nonce}AIKpriv表示用AIKpriv作為私鑰對PCR和收到的隨機數nonce進行簽名。

表3　TCG完整性報告協議Tab. 3　TCG integrity report protocol

在TCG完整性報告協議中，平臺配置證明涉及到表3中步驟3b、3c以及5b、5c：步驟3b和3c用于獲取應答者PB的PCR和SML，步驟5b和5c用于對應答者PB的PCR和SML進行安全驗證。在應答者PB獲得本地平臺PCR和SML的過程中，TCG規范沒有對PCR和SML的訪問或操作進行安全約束，這使得應答者PB中的局部攻擊者attackerl可直接進行惡意修改或破壞，造成應答者PB獲取的PCR和SML的可信狀態不可控，攻擊路徑見表4和表5；同時，全局攻擊者attackerg能夠直接對明文SML進行替換攻擊，導致挑戰者PA對PCR和SML的驗證結果與應答者PB的本地實際狀態并不一致，攻擊路徑見表6。

表4　局部攻擊者攻擊PBTab. 4　Local attackers tamper PB

表5　局部攻擊者欺騙PATab. 5　Local attackers deceit PA

表6　全局攻擊者攻擊SMLTab. 6　Global attackers tamper SML

2.2　攻擊者能力建模

根據Dolev-Yao模型，攻擊者能夠監聽所有消息，通過重寫規則來修改消息并發送它所擁有的消息。下面給出攻擊者具有的初始知識Init-adversary的定義。

定義1令Init為有限名集，如果Q是不包含事件的閉進程且fn(Q)?Init，那么Q為Init-adversary。

Init表示了攻擊者Q可獲得的初始知識。在完整性報告協議中，對于平臺配置完整性而言，TPM命令執行引擎、BIOS服務中斷和可信軟件棧(TCG Software Stack, TSS)核心服務提供者接口都提供了多個直接對PCR和SML進行操作的命令，這些命令集合InitPCR和InitSML構成了攻擊者Q的初始知識，具體命令見表7。

從跡語義的角度出發，若一條跡滿足attacker(M)，說明攻擊者擁有M，或者M被Init中的公有通道發送;跡滿足message(M,M′)，說明消息M′被通過通道M發送;跡滿足event(M)，說明事件event(M)已被執行?；谯E的原子語法見表8。

表7　攻擊者具有的初始知識Tab. 7　Attacker’s initial knowledge

表8　基于跡的原子語法Tab. 8　Atom grammar based on trace

定義4X|→f表示：通過已知的事實X能夠獲得事實f，其中|→為推導算子。

定義5令C為破壞平臺配置證明的攻擊者，那么：

C=vx.vy.vz.

letxh=hash(x) in

letyp=readpcr(y) in

letzs=eventlog(z) in

extendpcr(y,yp|xh).logsml(zs).

通過定義5可以看出，攻擊者通過破壞應答者的平臺配置完整性證明過程，最終讓挑戰者認為應答者的平臺配置完整性不滿足安全約束。攻擊者破壞平臺配置信息有三種方式：攻擊者將構造子應用在已有的知識上構造出新的消息；攻擊者將析構子應用在已有的消息上分析出新的知識；攻擊者在公共信道上發送消息和偷聽消息。攻擊者可通過構造子、析構子、名字生成并形成攻擊者知識，進而對平臺配置證明過程進行攻擊，攻擊者的構造算子和析構算子見表9。

2.3　平臺配置證明的局部攻擊

通過上文可以看出，在局部和全局攻擊者存在的情況下，應答者PB并不能向挑戰者PA證明自身的真實平臺配置信息，原因在于沒有對PCR和SML設置安全訪問策略，導致了局部攻擊者能夠對PCR和SML進行任意非授權寫操作，以及全局攻擊者對明文SML進行任意篡改操作，造成了IRP中的應答者PB和挑戰者PA之間難以滿足對應性關系。

平臺配置證明的局部攻擊包括對PCR和SML的攻擊，圖3列出了攻擊者具備的所有對PCR、SML和eventlog的初始知識。這里需要解釋說明的是，在平臺配置證明中，存儲度量日志SML由多個事件結構(Event Structure, ES)組成，每個ESi, j都是一個五元組，包括平臺配置寄存器索引idxi、事件類型typei, j、事件摘要digesti, j、事件長度sizei, j和數據eventi, j。其中digesti, j::=hash(eventi, j)，挑戰者對接收到的SML進行平臺配置證明。圖1給出了應答者PB上的局部攻擊者Init-adversary對平臺配置完整性的破壞。

表9　攻擊者的構造子和析構子Tab. 9　Attacker’s constructors and destructors

圖1　攻擊者利用局部接口的平臺配置完整性攻擊Fig. 1　Attacker’s compromising to platform configuration integrity by using local API

定義6令PA、PB分別表示挑戰者和應答者，ζ=ε,S∪{p,s},P表示PB運行協議時使用的平臺配置，p和s分別表示PCR和SML，那么對PA的認證性表示為p,s|→PA:φ。如果PB完成了協議，那么PB認為已經給PA發送了運行協議時使用的p和s，且PA收到了PB發送的p和s。

定義7令PA、PB分別表示挑戰者和應答者，p和s分別表示PCR和SML，那么對PB的認證性表示為p,s|→PB:φ。如果PA完成了協議，那么PA獲得的p和s的確是PB發送出來的。

文獻[2]提出完整性報告協議存在平臺替換攻擊，并指出其主要原因是用戶與平臺之間沒有綁定關系。同樣，在平臺配置證明過程中，PCR和SML的值與平臺之間也沒有綁定關系，任意主體都能夠對PCR和SML進行操作，因此，應答者PB進行平臺配置證明所使用的PCR和SML并不能反映PB當前的真實運行狀態。同時，也無法說明挑戰者PA接收的SML與應答者PB的對應性。因此，從對應性安全屬性出發，定義6和定義7給出了應答者PB向挑戰者PA證明自身平臺配置信息需滿足的條件。

定義8令應答者的平臺配置為ζ0=ε0,S0,P0，其中S0包含平臺配置寄存器P和存儲度量日志S，令p、s分別為P和S的當前會話實例，若存在locks和lockp，ε0,S0∪{lockp,s},P0→E0,S0,P0∪{p,s}，則稱P和S都是寫保護的。

通過定義8可以看出，若P和S的當前會話實例存在加鎖或者策略保護，那么可以通過加鎖機制或授權策略機制，實現平臺配置證明過程中p和s對應答者保持的唯一性。

3　滿足對應性屬性的平臺配置證明

安全協議的認證性是用對應性進行描述的，對應性一般使用兩個事件event1(M)和event2(M)，它們位于安全協議不同的角色子進程，event1(M)在消息M的發送者子進程中，event2(M)在消息M的接收者子進程中。對應性又可分為單射對應性、非單射對應性和一般對應性。

命題1令p和s分別表示PCR和SML，若p,s|→PA:φ且p,s|→PB:φ，則平臺配置證明過程是全局可靠但局部不可靠的。

從安全協議的認證性角度出發，命題1給出了對挑戰者PA的認證性和對應答者PB的認證性，如果PB運行完了協議，那么PB認為已經給PA發送了正確的SML和PCR，且PA的確收到了PB發送的SML和PCR；同時，如果PA運行完了協議，那么PA獲得的SML和PCR的確是PB發送出來的。

證畢。

命題1的現實意義在于，在認證性安全屬性約束下，IRP協議中的變量p和s不會受到全局攻擊，也就是不會出現篡改和假冒攻擊，但是在局部攻擊存在的情況下，p和s并不能代表PB的真實配置情況。

從命題1可知，p和s的狀態在全局可靠的情況下存在著局部不可靠的安全隱患，這是由于局部攻擊者具有的初始知識讓p和s的狀態發生了改變，而這種狀態改變在IRP中是無法表達的，造成局部攻擊者發起的攻擊難以被發現。為更好地對平臺配置證明過程進行安全描述，下面將用對應性屬性描述局部狀態變化引起的一致性關系。對應性屬性也稱為對應性斷言，用于描述多個事件之間發生的邏輯關系，即：“如果事件e發生了，那么事件e′在此之前也發生了”。下面將通過對應性屬性描述平臺配置證明。

表10　利用局部接口攻擊平臺配置完整性的形式化描述Tab. 10　Formulized description for local compromising to platform configuration integrity

則平臺配置證明過程存在平臺配置全局攻擊和局部攻擊。

證明當m=1時，

證畢。

則平臺配置證明過程存在局部攻擊。

證明當m=1時，

當m>1時，證明過程同上，不再贅述。

證畢。

對命題2和命題3的證明采用形式化驗證工具Proverif，證明結果如下：

query event(completedA(nonce,pcr,idx1,sml,idx2))==>

event(startedB(nonce,pcr,sml)).

The event completedA(n_512,p_513,i_514,s_515,i_516)

is executed.

A trace has been found.

RESULT event(completedA(x_271,y_272,z_273,m_274,

n_275))==>

event(startedB(x_271,y_272,m_274)) is false.

證明從命題條件

因此平臺配置證明是局部可靠的。

證畢。

則稱平臺配置證明是全局可靠的，即

證明從命題條件

因此平臺配置證明是全局可靠的。

證畢。

對命題4和命題5的證明同樣采用形式化驗證工具Proverif，證明結果如下：

Starting query event(completedA(x_265,y_266,z_267,

m_268,n_269))==>

event(startedB(x_265,y_266,m_268)).

goal reachable: begin(startedB(n_9,

p_10[!1=@sid_476],s_11[!2=@sid_477]->

end(completedA(n_9,p_10[!1=@sid_476],

@sid=@sid_476,s_11[!2=@sid_477],

@sid=@sid_477))

RESULT event(completedA(x_265,y_266,z_267,m_268,

n_269))==>

event(startedB(x_265,y_266,m_268)) is true.

4　結語

針對可信計算的完整性報告協議存在的安全問題，首先對形式化描述語言StatVerif進行了語法擴展，增加了與完整性度量相關的構造和析構算子，以對IRP進行形式化分析。對平臺配置證明安全進行分析后，發現其存在的局部攻擊和全局攻擊問題，通過對攻擊者能力進行建模，用形式化驗證工具Proverif對IRP的對應性進行了證明。

參考文獻:

[1]徐明迪,張煥國,張帆,等.可信系統信任鏈研究綜述[J].電子學報,2014,42(10):2024-2031. (XU M D, ZHANG H G, ZHANG F, et al. Survey on chain of trust of trusted system [J]. Acta Electronica Sinica, 2014, 42(10): 2024-2031.)

[2]馬卓.無線網絡可信接入理論及其應用研究[D].西安:西安電子科技大學,2010:23-44. (MA Z. Trusted access in wireless network theory and applications [D]. Xi’an: Xidian University, 2010: 23-44)

[3]徐明迪,張煥國,趙恒,等.可信計算平臺信任鏈安全性分析[J].計算機學報,2010,33(7):1165-1176. (XU M D, ZHANG H G, ZHAO H, et al. Security analysis on trust chain of trusted computing platform [J]. Chinese Journal of Computers, 2010, 33(7): 1165-1176.)

[4]ZHANG H, YAN F, FU J, et al. Research on theory and key technology of trusted computing platform security testing and evaluation [J]. Science China: Information Sciences, 2010, 53(3): 434-453.

[5]XU W, ZHANG X, HU H, et al. Remote attestation with domain-based integrity model and policy analysis [J]. IEEE Transactions on Dependable and Secure Computing, 2012, 9(3): 429-442.

[6]ARAPINIS M, RITTER E, RYAN M D. StatVerif: verification of stateful processes [C]// CSF 2011: Proceedings of the 24th IEEE Computer Security Foundations Symposium. Washington, DC: IEEE Computer Society, 2011: 33-47.

[7]DATTA A, FRANKLIN J, GARG D, et al. A logic of secure systems and its application to trusted computing [C]// SP 2009: Proceedings of the 30th IEEE Symposium on Security and Privacy. Washington, DC: IEEE Computer Society, 2009: 221-236.

[8]徐明迪,張煥國,張帆,等.授權約束下的平臺配置證明研究[J].電子學報,2017,45(6):1389-1395. (XU M D, ZHANG H G, ZHANG F, et al. Authorization restriction-based platform configuration attestation [J]. Acta Electronica Sinica, 2017, 45(6): 1389-1395.)

[9]JAIN L, VYAS J. Security analysis of remote attestation, CS259 Project Report [R]. Palo Alto: Stanford University, 2008: 1-8.

[10]BLANCHET B, ABADI M, FOURNET C. Automated verification of selected equivalences for security protocols [J]. The Journal of Logic and Algebraic Programming, 2008, 75(1): 3-51.

[11]SAILER R, ZHANG X L, JAEGER T, et al. Design and implementation of a TCG-based integrity measurement architecture [C]// SSYM 2004: Proceedings of the 13th Conference on USENIX Security Symposium. Berkeley, CA: USENIX Association, 2004, 13: 223-238.