第四章可信鏈測評4.1安全模型簡介4.2可信鏈交互模型4.3可信鏈接口安全模型4.4一致性測試和安全性測試4.5可信鏈PC規(guī)范一致性測試4.6可信鏈規(guī)范安全性分析4.7可信鏈測試評估系統(tǒng)4.8本章小結(jié)

4.1安全模型簡介

4.1.1基于語言的安全模型

針對傳統(tǒng)安全模型的局限、困難與挑戰(zhàn)，現(xiàn)在的安全模型運(yùn)用了更接近計(jì)算實(shí)質(zhì)的、更先進(jìn)的計(jì)算機(jī)理論工具，比如進(jìn)程演算、類型理論、時(shí)態(tài)邏輯等；而且更注重與應(yīng)用需求相結(jié)合、考慮系統(tǒng)的可用性及系統(tǒng)安全開銷等問題，跨越形式化方法與實(shí)際應(yīng)用的“鴻溝”?；诔绦蛘Z言的安全模型以其直觀的應(yīng)用層安全規(guī)范、強(qiáng)大的安全推理能力及良好的程序設(shè)計(jì)語言實(shí)現(xiàn)等優(yōu)點(diǎn)正受到更多的關(guān)注，基于程序設(shè)計(jì)語言的安全模型的優(yōu)勢在于：

(1)形式化地提供精細(xì)顆粒度的訪問控制，安全控制的顆粒度可以細(xì)化到程序變量級。

(2)模型易于通過程序語言實(shí)現(xiàn)，允許程序員直接進(jìn)行安全應(yīng)用規(guī)范的抽象，如描述系統(tǒng)模塊、抽象數(shù)據(jù)類型等。

(3)能產(chǎn)生易于擴(kuò)展以適應(yīng)新應(yīng)用要求的安全策略，支持不同策略的復(fù)合與協(xié)商。

(4)安全屬性可以通過程序語言的方法證明。4.1.2安全進(jìn)程代數(shù)

1.SPA基本語法

安全進(jìn)程代數(shù)(SPA)是CCS的擴(kuò)展。SPA中的動(dòng)作(actions)被視為原子操作。為了描述多級安全系統(tǒng)中不同安全級之間的信息流關(guān)系，SPA將可見動(dòng)作劃分為高安全級動(dòng)作和低安全級動(dòng)作。SPA的基本語法符號包括：

2.SPA操作語義

SPA的操作語義模型是標(biāo)記變遷系統(tǒng)(LabelledTransitionSystem，LTS)模型(E，Act，→)，其中二元關(guān)系的結(jié)構(gòu)化操作語義［10］如圖4.1所示。圖4.1

SPA的結(jié)構(gòu)化操作語義4.1.3基于語義的安全屬性

為了能夠形式化地驗(yàn)證安全機(jī)制的正確性，我們需要精確定義安全屬性。近年來很多學(xué)者對安全屬性進(jìn)行了定義［11-24］。這里我們要處理的是一類特殊的安全屬性——信息流屬性(InformationFlowProperties)。信息流屬性是用于控制信息在不同實(shí)體間流動(dòng)的方法，并用于確保機(jī)密性，特別用于驗(yàn)證訪問控制策略是否能夠保障信息的秘

密性。

定義4.3

E在屬性X下是安全的，當(dāng)且僅當(dāng)CX［E］≈DX［E］?！?/p>

一個(gè)SPA上下文(Context)G是一個(gè)SPA項(xiàng)，例如G［－］=F+-。進(jìn)程E的上下文G寫為G［E］，G［E］=F+E。這里上下文CX和DX表示只有E的低級行為是可觀察的，因此行為等價(jià)就是比較進(jìn)程E的低級行為。

1.基于跡語義的安全屬性

2.基于互模擬語義的安全屬性

為了能比較遷移系統(tǒng)的中間狀態(tài)，文獻(xiàn)［27］提出了互模擬等價(jià)(BisimulationEquivalence)的概念?；ツM刻畫了兩個(gè)系統(tǒng)之間的單步模擬思想，也就是說，當(dāng)進(jìn)程E執(zhí)行一個(gè)動(dòng)作到達(dá)E′后，進(jìn)程F也必須能夠通過執(zhí)行同樣的動(dòng)作到達(dá)F′，進(jìn)而模擬E所完成的單步過程，進(jìn)程E′和F′繼續(xù)重復(fù)進(jìn)行接下來的單步過程。■

3.基于測試語義的安全屬性

CSP語言提出了失效語義(FailtureSemantics)［28］的概念，失效語義是對跡語義的細(xì)化(Refinement)。當(dāng)執(zhí)行一條特定的跡之后，失效語義能夠觀察哪些動(dòng)作沒有被執(zhí)行。例如對于系統(tǒng)E來說，令s是一條跡，X是動(dòng)作集，(s，X)表示當(dāng)系統(tǒng)E執(zhí)行跡s后，X中的動(dòng)作都不會(huì)被執(zhí)行。

定義4.10系統(tǒng)E和F是測試等價(jià)的，即E≈testF，當(dāng)且僅當(dāng)對于每一個(gè)測試T而言都有：

·EmayT

FmayT;

·EmustT

FmustT?！?/p>

可以看出，當(dāng)E≈TF時(shí)第1個(gè)條件成立，實(shí)際上，如果EmayT，那么E可以執(zhí)行一條跡，該跡能夠讓T前進(jìn)到執(zhí)行動(dòng)作ω的狀態(tài)；條件2對應(yīng)著測試等價(jià)，其基本思想是如果E運(yùn)行跡γ后不能執(zhí)行特定的動(dòng)作a，那么可以通過測試進(jìn)程T運(yùn)行跡γ的對偶動(dòng)作，然后執(zhí)行動(dòng)作ω。4.1.4安全屬性的可復(fù)合性

安全性質(zhì)是信息流性質(zhì)［3，29］。直接或間接的信息泄露都被看做系統(tǒng)中的信息流動(dòng)，都可以使用信息流分析的技術(shù)找到系統(tǒng)中潛在的各種安全問題。

定義4.11安全性質(zhì)Φ是可復(fù)合的，如果

■

4.2可信鏈交互模型

4.2.1可信鏈規(guī)范說明

可信鏈PC規(guī)范說明如圖4.2所示。

從圖4.2中可以看出，可信鏈PC規(guī)范說明主要定義了兩種對象：

(1)TPM訪問規(guī)則對象；

(2)可信鏈建立對象。圖4.2可信鏈PC規(guī)范說明從圖4.3可知，三個(gè)進(jìn)程分別為：

(1)可信平臺模塊(TPM)；

(2)可信度量根(RTM)；

(3)硬件、固件和軟件所構(gòu)成的系統(tǒng)(System)。圖4.3可信鏈PC交互模型4.2.2可信鏈接口模型

上一節(jié)我們給出了可信鏈PC規(guī)范說明模型，該模型描述了可信鏈建立過程中的實(shí)體交互關(guān)系?？尚沛溡?guī)范不單純是一個(gè)軟件規(guī)范，也不僅僅是一個(gè)協(xié)議規(guī)范，它還包含：①與系統(tǒng)進(jìn)行交互的流程；②邏輯上并行的可信鏈建立規(guī)則；③軟件功能接口。

從安全進(jìn)程代數(shù)的角度考慮，為了能夠分析可信鏈建立過程的信息流安全，我們需要進(jìn)一步對實(shí)體的交互關(guān)系進(jìn)行細(xì)化(refine)，定義出實(shí)體間的輸入和輸出，并從安全的角度對這些輸入、輸出進(jìn)行等級劃分，驗(yàn)證可信鏈系統(tǒng)所符合的安全屬性。圖4.4可信鏈PC規(guī)范說明實(shí)體交互下面我們用SPA語法對圖4.3的三個(gè)進(jìn)程實(shí)體作進(jìn)一步說明。

定義4.12令

其中SRTM表示可信鏈規(guī)范說明，且限制集合Sy用于實(shí)體間的動(dòng)作同步?！?/p>

4.3可信鏈接口安全模型

4.3.1不可演繹模型

在對不可演繹模型進(jìn)行形式化描述之前，我們先給出相關(guān)的符號說明：

1.輸入不可演繹模型

輸入不可演繹模型(NonDeducibilityonInputs，NDI)源自Sutherland提出的信息流安全理論［30］。根據(jù)輸入不可演繹模型，所謂不存在信息流，意味著從進(jìn)程行為的低級觀察中，不能演繹地推導(dǎo)出關(guān)于進(jìn)程高級行為的任何性質(zhì)，或者說進(jìn)程E具有不可演繹性質(zhì)，如果進(jìn)程的任何低級可觀察行為low都不能推導(dǎo)出高級輸入highinput的任何

信息。根據(jù)文獻(xiàn)［30］對NDI的描述，先給出NDI的反向定義。

2.帶策略的不可演繹模型

Wittbold引入帶策略的不可演繹性［38］是為了避免不可演繹性的一些不期望的性質(zhì)，即滿足不可演繹性質(zhì)定義的系統(tǒng)中可能存在著隱蔽通道。帶策略的不可演繹性質(zhì)(NonDeducibilityonStrategies，NDS)是一類相當(dāng)強(qiáng)的安全性質(zhì)，它是可復(fù)合的。圖4.5同步狀態(tài)機(jī)的基本結(jié)構(gòu)

定義4.17進(jìn)程U的長度為n的策略是n個(gè)函數(shù)序列π=(π1，…，πn)，對于每一個(gè)i，1≤i≤n有：πi:(IU×OU)i-1→IU。

■

定義4.19一個(gè)同步狀態(tài)機(jī)滿足NDS性質(zhì)，當(dāng)且僅當(dāng)任意長度為n的低安全級視圖λ與高安全級進(jìn)程長度為n的策略保持一致(consistent)。

■4.3.2可信鏈復(fù)合模型

在4.3.1節(jié)我們對輸入不可演繹模型進(jìn)行了定義，下面我們用SPA給出可復(fù)合的不可演繹性質(zhì)的定義。

定義4.20令HActH，E∈E，那么E具有可復(fù)合的不可演繹性質(zhì)，當(dāng)且僅當(dāng)lowviews(E)=

lowviews((E|Π)＼H)?！?/p>

這里的lowviews()函數(shù)是low()函數(shù)的冪集，表示為

定義4.21系統(tǒng)E和F的復(fù)合系統(tǒng)為

■

1.CRTM與TPM的復(fù)合

在4.2.2節(jié)中我們已經(jīng)說明了CRTM和TPM中的所有動(dòng)作都屬于高安全級動(dòng)作，因此當(dāng)CRTM與TPM進(jìn)行復(fù)合之后，需要同步的高安全級動(dòng)作統(tǒng)統(tǒng)都轉(zhuǎn)換為內(nèi)部動(dòng)作τ，該動(dòng)作和高安全級動(dòng)作對于低安全級視圖是不可見的。CRTM與TPM的復(fù)合模型如圖4.6所示。圖4.6

CRTM與TPM的復(fù)合模型圖4.7

CRTM與TPM的LTS系統(tǒng)

2.POSTBIOS與TPM的復(fù)合

當(dāng)CRTM對POSTBIOS度量完畢后，POSTBIOS需要

對System的第一個(gè)啟動(dòng)組件進(jìn)行完整性度量和完整性存

儲。這里的符號描述和SPA描述與上一小節(jié)基本相同，

不再贅述。

復(fù)合模型和復(fù)合系統(tǒng)分別如圖4.8和圖4.9所示。圖4.8

POSTBIOS與TPM的復(fù)合模型圖4.9

POSTBIOS與TPM的LTS系統(tǒng)

3.System與TBB的復(fù)合

從上面兩小節(jié)可以知道，CRTM、POSTBIOS和TPM所組成的TBB中所有的輸入、輸出動(dòng)作都是高安全級動(dòng)作。那么對于動(dòng)作序列和

來說，由于是高安全級動(dòng)作，且沒有低安全級輸入、輸出對高安全級動(dòng)作的依賴，因此復(fù)合系統(tǒng)CRTM_TPM、POST_TPM都滿足NDI和NDS安全屬性。圖4.10

System與TBB的復(fù)合模型圖4.11

System與TBB的部分LTS系統(tǒng)4.3.3進(jìn)一步的分析

4.4一致性測試和安全性測試

4.4.1一致性測試

一般來說，規(guī)范通常是采用自然語言或者非形式化語言的一種描述，規(guī)范本身的高度抽象和二義性使得實(shí)際工程通常并未完全遵照規(guī)范說明來實(shí)現(xiàn)。4.4.2安全性測試

可信計(jì)算產(chǎn)品的設(shè)計(jì)依據(jù)源于規(guī)范說明，因此可信計(jì)算產(chǎn)品的安全程度和規(guī)范說明有著直接的聯(lián)系。TCG制定的TPM保護(hù)輪廓規(guī)范通過了CC認(rèn)證，Atmel公司的TPM產(chǎn)品AT97SC3201通過了認(rèn)證實(shí)驗(yàn)室CygnaCom的EAL3認(rèn)證，Infineon公司已經(jīng)開始對生產(chǎn)的TPM進(jìn)行最嚴(yán)格的硬件安全評估流程審核，計(jì)劃要達(dá)到EAL4硬件安全水平。

4.5可信鏈PC規(guī)范一致性測試

4.5.1標(biāo)記變遷系統(tǒng)(LTS)

一個(gè)LTS由狀態(tài)以及帶標(biāo)記的狀態(tài)間的變遷組成。LTS是基于狀態(tài)和變遷的抽象關(guān)系模型。任何一個(gè)給定的模型，給出全局狀態(tài)和原子動(dòng)作以及對應(yīng)的狀態(tài)變遷規(guī)則，就可以定義出相應(yīng)的變遷系統(tǒng)。許多并發(fā)系統(tǒng)的屬性都可以用變遷系統(tǒng)進(jìn)行描述。

定義4.25標(biāo)記變遷系統(tǒng)是一個(gè)四元組(Q,A,－μ→,

q0)：Q是非空有限狀態(tài)集合；A是有限的基本動(dòng)作集合；μ∈A∪{τ}，－μ→是集合Q上的二元關(guān)系；q0∈Q是初始狀態(tài)?！觥鰣D4.12

LTS的符號定義4.5.2可信鏈規(guī)范說明狀態(tài)集

我們將可信鏈一致性測試中使用的規(guī)范形式說明集合記為SPECS，將規(guī)范實(shí)現(xiàn)的集合記為IMPS。SPECS通常是對可信鏈實(shí)現(xiàn)的一種抽象定義，一般采用非形式化或者自然語言進(jìn)行描述。系統(tǒng)實(shí)現(xiàn)的過程是多種多樣的。因此，所謂的“一致性”，就是IMPS與SPECS之間的一種關(guān)系，記為imp:impIMPS×SPECS，任何(i，s)∈imp或iimps表示i是s的一種一致性實(shí)現(xiàn)。規(guī)范說明和規(guī)范實(shí)現(xiàn)都可以看做一個(gè)標(biāo)記變遷系統(tǒng)，即認(rèn)為規(guī)范實(shí)現(xiàn)i與規(guī)范說明s都有相應(yīng)的LTS(i)和LTS(s)。圖4.13

RTM與TPM、System之間的交互關(guān)系圖4.14可信鏈LTS(s)系統(tǒng)4.5.3可信鏈規(guī)范實(shí)現(xiàn)測試集

對于測試用例而言，為了保證它盡可能多地滿足各個(gè)測試需求，同時(shí)數(shù)量最少，需要對測試目標(biāo)中的所有測試需求進(jìn)行整體優(yōu)化，從而生成最少的測試用例，實(shí)現(xiàn)對測試目標(biāo)的充分測試。因此約簡規(guī)則和約簡條件可以表示為：

(1)LTS(s)中的狀態(tài)s1和s2是可以被去除的；

(2)LTS(s)中的狀態(tài)s8~s14是可以被去除的；

(3)LTS(s)的起始狀態(tài)是s0，結(jié)束狀態(tài)是s17；

(4)LTS(s)必須包含狀態(tài)s6和s15。圖4.15可信鏈LTS(i)系統(tǒng)

定義4.29令i∈LTS(i)，s∈LTS(s)，那么i≤tr

s，如果Trace(i)Trace(s)?！?/p>

跡前序表示規(guī)范實(shí)現(xiàn)的LTS樹是規(guī)范說明的LTS樹的子樹。圖4.14所刻畫的是可信鏈規(guī)范說明中的LTS(s)系統(tǒng)，而實(shí)際的可信鏈規(guī)范實(shí)現(xiàn)的LTS(i)系統(tǒng)和前者應(yīng)該是一種≤tr二元關(guān)系的，也就是說Trace(i)Trace(s)，也就是圖4.15所刻畫的可信鏈LTS(i)系統(tǒng)。

定義4.30

i≤tes當(dāng)且僅當(dāng)σ∈A*，a∈A，After(i，σ－a)After(s，σ－a)。■

測試前序和跡前序正好相反，≤te表示規(guī)范說明的LTS樹是規(guī)范實(shí)現(xiàn)的LTS樹的子樹。這是由于規(guī)范說明中滿足After(s，σ－a)的σ－a使得規(guī)范實(shí)現(xiàn)中的After(i，σ－a)不成立，也就是i(σ－a)，這也反映了規(guī)范實(shí)現(xiàn)與規(guī)范說明之間的差異。

命題4.5

LTS(i)是經(jīng)過對LTS(s)進(jìn)行動(dòng)作約簡后得到的標(biāo)記變遷系統(tǒng)，LTS(i)和LTS(s)滿足跡前序，即i≤tr

s。

證明：根據(jù)定義4.29可知，若Trace(i)Trace(s)，則i≤tr

s成立，又根據(jù)定義4.26有Trace(q)={σ∈A*|q=σ},因此只需證明{σi}{σs}。

根據(jù)命題條件：LTS(i)是經(jīng)過對LTS(s)進(jìn)行動(dòng)作約簡后所得的標(biāo)記變遷系統(tǒng)，因此有Ai

As，那么有A*i

A*s,而σi∈A*i，σs∈A*s，因此有{σi}{σs}。■4.5.4測試流程

下面的工作是將可信鏈測試?yán)蜏y試集進(jìn)行形式化。一個(gè)測試?yán)菧y試者與被測對象相互作用的行為的描述。這種行為也可以表示成一個(gè)LTS，但是測試要在有限時(shí)間內(nèi)完成，因此測試行為以及描述測試?yán)腖TS必須是確定且有限的。同時(shí)我們要給測試?yán)拿總€(gè)結(jié)束狀態(tài)一個(gè)判決(passorfail)。下面是其定義：

(1)測試?yán)且粋€(gè)五元組〈Q，A，－μ→，v，s0〉，其中〈Q，A，－μ→，s0〉是一個(gè)動(dòng)作有限且確定的LTS，v是一個(gè)判決函數(shù)v:Q→{fail，pass}。我們用LTSt(A)表示A上所有測試?yán)募?。而一個(gè)測試?yán)梢钥醋鍪且粋€(gè)LTS的擴(kuò)展。

(2)測試套(TestSuite)T是測試?yán)囊粋€(gè)集合：T∈P(LTSt(A))，這里P(LTSt(A))指LTSt(A)的冪集，即LTSt(A)的所有子集的集合。圖4.16可信鏈LTS(im)子圖

4.6可信鏈規(guī)范安全性分析

4.6.1可信鏈接口安全等級

在可信鏈運(yùn)行期間，RTM和TPM通過接口進(jìn)行了復(fù)合，一方面，我們需要發(fā)現(xiàn)這種復(fù)合是否能夠保護(hù)高級輸入、輸出，另一方面，RTM和TPM所組成的TBB子系統(tǒng)與System又進(jìn)行了復(fù)合，我們需要進(jìn)一步發(fā)現(xiàn)該復(fù)合能否滿足不可演繹安全性。4.6.2可信鏈接口安全測試

為了驗(yàn)證可信計(jì)算PC規(guī)范說明的SRTM是否滿足SBNDC，我們使用CoPS(CheckerofPersistentsSecurity)對其進(jìn)行驗(yàn)證。CoPS是Pivato等人開發(fā)的用于自動(dòng)化驗(yàn)證多級安全屬性的工具，用于驗(yàn)證系統(tǒng)是否滿足P_BNDC、PP

_BNDC或SBNDC等安全性質(zhì)。

我們將剛才用SPA描述的System、RTM和TPM的接口函數(shù)轉(zhuǎn)化為CoPS后，得到的驗(yàn)證結(jié)果如圖4.17所示。圖4.17

CoPS驗(yàn)證可信鏈規(guī)范說明在驗(yàn)證過程中我們發(fā)現(xiàn)，根據(jù)上述劃分的SRTM并不滿足SBNDC安全性質(zhì)，這是因?yàn)樵赟ystem中存在著低安全級動(dòng)作對高安全級動(dòng)作的依賴，因此低安全級的System就可以通過隱式的方法獲得TBB中的高級輸入或者輸出；我們可以通過消除這些依賴使得修改后的可信鏈規(guī)范說明滿足SBNDC安全屬性，如圖4.18所示。表4.1給出了SRTM中所存在的低安全級動(dòng)作對高安全級動(dòng)作的依賴。圖4.18

CoPS驗(yàn)證修改后的可信鏈規(guī)范說明

4.7可信鏈測試評估系統(tǒng)

4.7.1可信鏈測評對象

可信鏈?zhǔn)强尚庞?jì)算平臺的重要組成部分。我們認(rèn)為可信鏈可分為基本可信鏈和擴(kuò)展可信鏈?；究尚沛湴藢RTM、BIOS、OSLoader和平臺相關(guān)啟動(dòng)組件的可信度量，擴(kuò)展可信鏈包含了對操作系統(tǒng)、應(yīng)用程序以及網(wǎng)絡(luò)環(huán)境等組件的可信度量。將基本可信鏈中的CRTM、BIOS、OSLoader模塊通過一定的關(guān)系組合，就能保證可信計(jì)算平臺從硬件配置環(huán)境到操作系統(tǒng)、應(yīng)用程序以及網(wǎng)絡(luò)環(huán)境下運(yùn)行的可靠性和安全性。圖4.19可信鏈測試模型4.7.2可信鏈測評實(shí)例

可信鏈測評是針對國內(nèi)外不同的TPM/TCM可信計(jì)算平臺開展的，其中，符合TCG的可信計(jì)算平臺有三個(gè)，分別是HP6400、HP6230和ThinkPadR61i；符合中國可信計(jì)算密碼支撐平臺功能與接口規(guī)范的可信計(jì)算平臺有兩個(gè)。被測試系統(tǒng)的硬件和軟件環(huán)境如表4.2所示。圖4.20可信鏈測試拓?fù)浣Y(jié)構(gòu)圖4.21不同可信PC平臺可信鏈測試結(jié)果4.7.3可信鏈測評總結(jié)

通過對不同可信