满足对应性属性的平台配置证明

徐明迪，高　杨，高雪原，张　帆

(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)已被执行。基于迹的原子语法见表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.