1、第四章 可信链测评1 1第四章 可 信 链 测 评4.1安全模型简介4.2可信链交互模型4.3可信链接口安全模型4.4一致性测试和安全性测试4.5可信链PC规范一致性测试4.6可信链规范安全性分析4.7可信链测试评估系统4.8本章小结第四章 可信链测评2 24.1安全模型简介4.1.1基于语言的安全模型针对传统安全模型的局限、困难与挑战，现在的安全模型运用了更接近计算实质的、更先进的计算机理论工具，比如进程演算、类型理论、时态逻辑等；而且更注重与应用需求相结合、考虑系统的可用性及系统安全开销等问题，跨越形式化方法与实际应用的“鸿沟”。第四章 可信链测评3 3基于程序语言的安全模型以其直观的应用
2、层安全规范、强大的安全推理能力及良好的程序设计语言实现等优点正受到更多的关注，基于程序设计语言的安全模型的优势在于：(1)形式化地提供精细颗粒度的访问控制，安全控制的颗粒度可以细化到程序变量级。(2)模型易于通过程序语言实现，允许程序员直接进行安全应用规范的抽象，如描述系统模块、抽象数据类型等。(3)能产生易于扩展以适应新应用要求的安全策略，支持不同策略的复合与协商。(4)安全属性可以通过程序语言的方法证明。第四章 可信链测评4 44.1.2安全进程代数1.SPA基本语法安全进程代数(SPA)是CCS的扩展。SPA中的动作(actions)被视为原子操作。为了描述多级安全系统中不同安全级之间的
3、信息流关系，SPA将可见动作划分为高安全级动作和低安全级动作。SPA的基本语法符号包括：第四章 可信链测评5 5第四章 可信链测评6 6第四章 可信链测评7 72.SPA操作语义SPA的操作语义模型是标记变迁系统(Labelled Transition System，LTS)模型(E，Act，)，其中二元关系的结构化操作语义10如图4.1所示。第四章 可信链测评8 8图4.1SPA的结构化操作语义第四章 可信链测评9 94.1.3基于语义的安全属性为了能够形式化地验证安全机制的正确性，我们需要精确定义安全属性。近年来很多学者对安全属性进行了定义11-24。这里我们要处理的是一类特殊的安全属性信
4、息流属性(Information Flow Properties)。信息流属性是用于控制信息在不同实体间流动的方法，并用于确保机密性，特别用于验证访问控制策略是否能够保障信息的秘密性。第四章 可信链测评1010定义4.3E在属性X下是安全的，当且仅当CXEDXE。一个SPA上下文(Context)G是一个SPA项，例如G=F+-。进程E的上下文G写为GE，GE=F+E。这里上下文CX和DX表示只有E的低级行为是可观察的，因此行为等价就是比较进程E的低级行为。第四章 可信链测评11111.基于迹语义的安全属性第四章 可信链测评1212第四章 可信链测评13132.基于互模拟语义的安全属性为了能比
5、较迁移系统的中间状态，文献27提出了互模拟等价(Bisimulation Equivalence)的概念。互模拟刻画了两个系统之间的单步模拟思想，也就是说，当进程E执行一个动作到达E后，进程F也必须能够通过执行同样的动作到达F，进而模拟E所完成的单步过程，进程E和F继续重复进行接下来的单步过程。第四章 可信链测评1414 第四章 可信链测评1515第四章 可信链测评16163.基于测试语义的安全属性CSP语言提出了失效语义(Failture Semantics)28的概念，失效语义是对迹语义的细化(Refinement)。当执行一条特定的迹之后，失效语义能够观察哪些动作没有被执行。例如对于系统
6、E来说，令s是一条迹，X是动作集，(s，X)表示当系统E执行迹s后，X中的动作都不会被执行。第四章 可信链测评1717第四章 可信链测评1818定义4.10系统E和F是测试等价的，即EtestF，当且仅当对于每一个测试T而言都有：E may T F may T;E must T F must T。可以看出，当ETF时第1个条件成立，实际上，如果E may T，那么E可以执行一条迹，该迹能够让T前进到执行动作的状态；条件2对应着测试等价，其基本思想是如果E运行迹后不能执行特定的动作a，那么可以通过测试进程T运行迹的对偶动作 ，然后执行动作。第四章 可信链测评19194.1.4安全属性的可复合性安
7、全性质是信息流性质3，29。直接或间接的信息泄露都被看做系统中的信息流动，都可以使用信息流分析的技术找到系统中潜在的各种安全问题。定义4.11安全性质是可复合的，如果第四章 可信链测评20204.2可信链交互模型4.2.1可信链规范说明可信链PC规范说明如图4.2所示。从图4.2中可以看出，可信链PC规范说明主要定义了两种对象：(1)TPM访问规则对象；(2)可信链建立对象。第四章 可信链测评2121图4.2可信链PC规范说明第四章 可信链测评2222从图4.3可知，三个进程分别为：(1)可信平台模块(TPM)；(2)可信度量根(RTM)；(3)硬件、固件和软件所构成的系统(System)。第
8、四章 可信链测评2323图4.3可信链PC交互模型第四章 可信链测评24244.2.2可信链接口模型上一节我们给出了可信链PC规范说明模型，该模型描述了可信链建立过程中的实体交互关系。可信链规范不单纯是一个软件规范，也不仅仅是一个协议规范，它还包含：与系统进行交互的流程；逻辑上并行的可信链建立规则；软件功能接口。从安全进程代数的角度考虑，为了能够分析可信链建立过程的信息流安全，我们需要进一步对实体的交互关系进行细化(refine)，定义出实体间的输入和输出，并从安全的角度对这些输入、输出进行等级划分，验证可信链系统所符合的安全属性。第四章 可信链测评2525图4.4可信链PC规范说明实体交互第
9、四章 可信链测评2626下面我们用SPA语法对图4.3的三个进程实体作进一步说明。定义4.12令其中SRTM表示可信链规范说明，且限制集合Sy用于实体间的动作同步。第四章 可信链测评27274.3可信链接口安全模型4.3.1不可演绎模型在对不可演绎模型进行形式化描述之前，我们先给出相关的符号说明：第四章 可信链测评2828第四章 可信链测评2929第四章 可信链测评30301.输入不可演绎模型输入不可演绎模型(Non Deducibility on Inputs，NDI)源自Sutherland提出的信息流安全理论30。根据输入不可演绎模型，所谓不存在信息流，意味着从进程行为的低级观察中，不能
10、演绎地推导出关于进程高级行为的任何性质，或者说进程E具有不可演绎性质，如果进程的任何低级可观察行为low都不能推导出高级输入highinput的任何信息。根据文献30对NDI的描述，先给出NDI的反向定义。第四章 可信链测评3131第四章 可信链测评3232第四章 可信链测评3333第四章 可信链测评34342.带策略的不可演绎模型Wittbold引入带策略的不可演绎性38是为了避免不可演绎性的一些不期望的性质，即满足不可演绎性质定义的系统中可能存在着隐蔽通道。带策略的不可演绎性质(Non Deducibility on Strategies，NDS)是一类相当强的安全性质，它是可复合的。第四
11、章 可信链测评3535图4.5同步状态机的基本结构第四章 可信链测评3636定义4.17进程U的长度为n的策略是n个函数序列=(1，n)，对于每一个i，1in有：i:(IUOU)i-1IU。第四章 可信链测评3737第四章 可信链测评3838定义4.19一个同步状态机满足NDS性质，当且仅当任意长度为n的低安全级视图与高安全级进程长度为n的策略保持一致(consistent)。第四章 可信链测评39394.3.2可信链复合模型在4.3.1节我们对输入不可演绎模型进行了定义，下面我们用SPA给出可复合的不可演绎性质的定义。定义4.20令H ActH，EE，那么E具有可复合的不可演绎性质，当且仅当
12、lowviews(E)=lowviews(E|)H)。这里的lowviews()函数是low()函数的幂集，表示为 第四章 可信链测评4040定义4.21系统E和F的复合系统为1.CRTM与TPM的复合在4.2.2节中我们已经说明了CRTM和TPM中的所有动作都属于高安全级动作，因此当CRTM与TPM进行复合之后，需要同步的高安全级动作统统都转换为内部动作，该动作和高安全级动作对于低安全级视图是不可见的。CRTM与TPM的复合模型如图 4.6 所示。第四章 可信链测评4141图4.6CRTM与TPM的复合模型第四章 可信链测评4242图4.7CRTM与TPM的LTS系统第四章 可信链测评434
13、32.POSTBIOS与TPM的复合当CRTM对POSTBIOS度量完毕后，POSTBIOS需要对System的第一个启动组件进行完整性度量和完整性存储。这里的符号描述和SPA描述与上一小节基本相同，不再赘述。复合模型和复合系统分别如图4.8和图4.9所示。第四章 可信链测评4444图4.8POSTBIOS与TPM的复合模型第四章 可信链测评4545图4.9POSTBIOS与TPM的LTS系统第四章 可信链测评46463.System与TBB的复合从上面两小节可以知道，CRTM、POSTBIOS和TPM所组成的TBB中所有的输入、输出动作都是高安全级动作。那么对于动作序列和来说，由于是高安全级
14、动作，且没有低安全级输入、输出对高安全级动作的依赖，因此复合系统CRTM_TPM、POST_TPM都满足NDI和NDS安全属性。第四章 可信链测评4747图4.10System与TBB的复合模型第四章 可信链测评4848图4.11System与TBB的部分LTS系统第四章 可信链测评49494.3.3进一步的分析第四章 可信链测评5050第四章 可信链测评5151第四章 可信链测评52524.4一致性测试和安全性测试4.4.1一致性测试一般来说，规范通常是采用自然语言或者非形式化语言的一种描述，规范本身的高度抽象和二义性使得实际工程通常并未完全遵照规范说明来实现。第四章 可信链测评53534.
15、4.2安全性测试可信计算产品的设计依据源于规范说明，因此可信计算产品的安全程度和规范说明有着直接的联系。TCG制定的TPM保护轮廓规范通过了CC认证，Atmel公司的TPM产品AT97SC3201通过了认证实验室CygnaCom的EAL3认证，Infineon公司已经开始对生产的TPM进行最严格的硬件安全评估流程审核，计划要达到EAL4硬件安全水平。第四章 可信链测评54544.5可信链PC规范一致性测试4.5.1标记变迁系统(LTS)一个LTS由状态以及带标记的状态间的变迁组成。LTS是基于状态和变迁的抽象关系模型。任何一个给定的模型，给出全局状态和原子动作以及对应的状态变迁规则，就可以定义
16、出相应的变迁系统。许多并发系统的属性都可以用变迁系统进行描述。第四章 可信链测评5555定义4.25标记变迁系统是一个四元组(Q,A,q0)：Q是非空有限状态集合；A是有限的基本动作集合；A，是集合Q上的二元关系；q0Q是初始状态。第四章 可信链测评5656 第四章 可信链测评5757第四章 可信链测评5858第四章 可信链测评5959图4.12LTS的符号定义第四章 可信链测评60604.5.2可信链规范说明状态集我们将可信链一致性测试中使用的规范形式说明集合记为SPECS，将规范实现的集合记为IMPS。SPECS通常是对可信链实现的一种抽象定义，一般采用非形式化或者自然语言进行描述。系统实
17、现的过程是多种多样的。因此，所谓的“一致性”，就是IMPS与SPECS之间的一种关系，记为imp:imp IMPSSPECS，任何(i，s)imp或i imp s表示i是s的一种一致性实现。规范说明和规范实现都可以看做一个标记变迁系统，即认为规范实现i与规范说明s都有相应的LTS(i)和LTS(s)。第四章 可信链测评6161图4.13RTM与TPM、System之间的交互关系第四章 可信链测评6262图4.14可信链LTS(s)系统第四章 可信链测评63634.5.3可信链规范实现测试集对于测试用例而言，为了保证它尽可能多地满足各个测试需求，同时数量最少，需要对测试目标中的所有测试需求进行整
18、体优化，从而生成最少的测试用例，实现对测试目标的充分测试。第四章 可信链测评6464因此约简规则和约简条件可以表示为：(1)LTS(s)中的状态s1和s2是可以被去除的；(2)LTS(s)中的状态s8s14是可以被去除的；(3)LTS(s)的起始状态是s0，结束状态是s17；(4)LTS(s)必须包含状态s6和s15。第四章 可信链测评6565图4.15可信链LTS(i)系统第四章 可信链测评6666定义4.29令iLTS(i)，sLTS(s)，那么itr s，如果Trace(i)Trace(s)。迹前序表示规范实现的LTS树是规范说明的LTS树的子树。图4.14所刻画的是可信链规范说明中的L
19、TS(s)系统，而实际的可信链规范实现的LTS(i)系统和前者应该是一种tr二元关系的，也就是说Trace(i)Trace(s)，也就是图4.15所刻画的可信链LTS(i)系统。第四章 可信链测评6767定义4.30ites当且仅当 A*，aA，After(i，a)After(s，a)。测试前序和迹前序正好相反，te表示规范说明的LTS树是规范实现的LTS树的子树。这是由于规范说明中满足After(s，a)的a使得规范实现中的After(i，a)不成立，也就是i (a)，这也反映了规范实现与规范说明之间的差异。第四章 可信链测评6868命题4.5LTS(i)是经过对LTS(s)进行动作约简后得
20、到的标记变迁系统，LTS(i)和LTS(s)满足迹前序，即itr s。证明：根据定义4.29可知，若Trace(i)Trace(s)，则itr s成立，又根据定义4.26有Trace(q)=A*|q=,因此只需证明i s。根据命题条件：LTS(i)是经过对LTS(s)进行动作约简后所得的标记变迁系统，因此有Ai As，那么有A*i A*s,而iA*i，sA*s，因此有 i s。第四章 可信链测评6969第四章 可信链测评70704.5.4测试流程下面的工作是将可信链测试例和测试集进行形式化。一个测试例是测试者与被测对象相互作用的行为的描述。这种行为也可以表示成一个LTS，但是测试要在有限时间内
21、完成，因此测试行为以及描述测试例的LTS必须是确定且有限的。同时我们要给测试例的每个结束状态一个判决(pass or fail)。第四章 可信链测评7171下面是其定义：(1)测试例是一个五元组Q，A，v，s0，其中Q，A，s0是一个动作有限且确定的LTS，v是一个判决函数v:Qfail，pass。我们用LTSt(A)表示A上所有测试例的集合。而一个测试例可以看做是一个LTS的扩展。(2)测试套(Test Suite)T是测试例的一个集合：TP(LTSt(A)，这里P(LTSt(A)指LTSt(A)的幂集，即LTSt(A)的所有子集的集合。第四章 可信链测评7272图4.16可信链LTS(im
22、)子图第四章 可信链测评73734.6可信链规范安全性分析4.6.1可信链接口安全等级在可信链运行期间，RTM和TPM通过接口进行了复合，一方面，我们需要发现这种复合是否能够保护高级输入、输出，另一方面，RTM和TPM所组成的TBB子系统与System又进行了复合，我们需要进一步发现该复合能否满足不可演绎安全性。第四章 可信链测评74744.6.2可信链接口安全测试为了验证可信计算PC规范说明的SRTM是否满足SBNDC，我们使用CoPS(Checker of Persistents Security)对其进行验证。CoPS是Pivato等人开发的用于自动化验证多级安全属性的工具，用于验证系统
23、是否满足P_BNDC、PP_BNDC或SBNDC等安全性质。我们将刚才用SPA描述的System、RTM和TPM的接口函数转化为CoPS后，得到的验证结果如图4.17所示。第四章 可信链测评7575图4.17CoPS验证可信链规范说明第四章 可信链测评7676在验证过程中我们发现，根据上述划分的SRTM并不满足SBNDC安全性质，这是因为在System中存在着低安全级动作对高安全级动作的依赖，因此低安全级的System就可以通过隐式的方法获得TBB中的高级输入或者输出；我们可以通过消除这些依赖使得修改后的可信链规范说明满足SBNDC安全属性，如图4.18所示。表4.1给出了SRTM中所存在的低
24、安全级动作对高安全级动作的依赖。第四章 可信链测评7777图4.18CoPS验证修改后的可信链规范说明第四章 可信链测评7878第四章 可信链测评79794.7可信链测试评估系统4.7.1可信链测评对象可信链是可信计算平台的重要组成部分。我们认为可信链可分为基本可信链和扩展可信链。基本可信链包含了对CRTM、BIOS、OS Loader和平台相关启动组件的可信度量，扩展可信链包含了对操作系统、应用程序以及网络环境等组件的可信度量。将基本可信链中的CRTM、BIOS、OS Loader模块通过一定的关系组合，就能保证可信计算平台从硬件配置环境到操作系统、应用程序以及网络环境下运行的可靠性和安全性
25、。第四章 可信链测评8080图4.19可信链测试模型第四章 可信链测评81814.7.2可信链测评实例可信链测评是针对国内外不同的TPM/TCM可信计算平台开展的，其中，符合TCG的可信计算平台有三个，分别是HP6400、HP6230和ThinkPad R61i；符合中国可信计算密码支撑平台功能与接口规范的可信计算平台有两个。被测试系统的硬件和软件环境如表4.2所示。第四章 可信链测评8282第四章 可信链测评8383图4.20可信链测试拓扑结构第四章 可信链测评8484图4.21不同可信PC平台可信链测试结果第四章 可信链测评8585第四章 可信链测评86864.7.3可信链测评总结通过对不
26、同可信计算产品可信链进行测试发现，现有的所有可信计算产品都没有完全符合可信链规范说明，从规范符合性测试来看主要有以下几点：(1)完整性度量覆盖不全。(2)无证书。第四章 可信链测评87874.8本 章 小 结从规范角度来看，可信计算平台规范是一种理想情况下的产品实现参考，大部分厂商并未严格按照该规范研制产品。从功能上来说，该规范着重定义了BIOS、OS Loader访问TPM功能函数的接口以及BIOS建立OS启动之前的可信链流程；从安全性来说，该规范对不同等级的客体访问TPM作出了安全上的规定，如建立不同层次的TPM访问通道、对访问TPM内部非易失性存储区NVRAM所建立的映射关系。第四章 可
27、信链测评8888对于不同可信计算平台产品而言，其实现上的不同导致了单纯地从规范的角度对其进行测试的局限性和不完备性。根据可信计算平台规范所定义的可信链内容，结合PC启动的一般流程，我们将CRTM定义为可信链的最底层，它是事件的产生者；CRTM所创建的事件日志定义为中间层，它是构建可信链的依据；事件所产生的平台状态定义为最高层，它决定信任传递的正确与否。第四章 可信链测评8989从功能性来说，可信链规范着重定义了可信链的建立流程，以及为了建立可信链，外部实体需要访问TPM API的接口；从安全性来说，可信链规范规定了客体对象访问TPM的规则，如Locality使用原则、访问TPM内部NV存储的方
28、法。可信PC规范所包含的内容非常丰富，根据我们掌握的可信计算平台测试经验，不同可信PC产品在规范实现上的差异导致了单纯地从规范说明的角度对其进行逐一测试的局限性。第四章 可信链测评9090因此，我们从对实际产品进行测试的角度出发，根据实际可信PC产品系统实现的流程，遵循规范中应包含的技术要求和功能保障，将可信度量根测试又具体分为证书测试、支撑软件测试和对外接口测试；将事件测试具体分为事件覆盖测试和事件迭代测试；将状态测试具体分为状态集合测试和状态迁移测试。对于可信度量根的测试是保障可信链的基础，除了最基本的功能性测试之外，我们还计划对其进行安全分析和安全测试，找出其中隐藏的漏洞和安全隐患，进一步对设计高安全等级的计算机系统提供有力的反馈。
