迮 愷,陳 丹,莊 毅

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,南京 211106)

0 概述

由于分布式系統(tǒng)和計(jì)算機(jī)網(wǎng)絡(luò)的快速發(fā)展,以及經(jīng)濟(jì)全球化帶來的電子通信的全球化,對安全通信協(xié)議的需求也達(dá)到前所未有的高度。自二十世紀(jì)九十年代以來,嵌入式系統(tǒng)在軍事、工業(yè)和家用電器等方面得到了廣泛的應(yīng)用?？尚判宰鳛椴僮飨到y(tǒng)最重要的屬性之一,已成為嵌入式系統(tǒng)重點(diǎn)研究的方向。但現(xiàn)有系統(tǒng)可信判定模型大多局限于系統(tǒng)啟動(dòng)后對實(shí)體的靜態(tài)可信判定,且對于系統(tǒng)進(jìn)程可信的判斷過于苛刻,系統(tǒng)動(dòng)態(tài)可信的判定僅停留在充分性的解釋,難以完整支撐系統(tǒng)動(dòng)態(tài)可信理論。

為實(shí)現(xiàn)動(dòng)態(tài)的系統(tǒng)可信判定,本文在現(xiàn)有研究的基礎(chǔ)上,將計(jì)算機(jī)系統(tǒng)抽象為一個(gè)六元組,引入iP-可觀測屬性,由有限狀態(tài)自動(dòng)機(jī)對其進(jìn)行演化,在2種可觀測屬性之間產(chǎn)生關(guān)聯(lián),并針對動(dòng)態(tài)系統(tǒng)環(huán)境,采用P-可觀測屬性檢查算法確認(rèn)系統(tǒng)是否滿足動(dòng)態(tài)非傳遞無干擾(Intrasitive Noninterference,INI)理論,給出系統(tǒng)可信判定的充分必要條件。最后通過實(shí)例驗(yàn)證,說明P-可觀測屬性檢查算法的可行性,以及系統(tǒng)可信性與動(dòng)態(tài)非傳遞無干擾理論的關(guān)聯(lián)性。

1 研究背景

國際信息安全組織雖尚未對“安全性”作出確切定義,但一般認(rèn)為,安全性即在多安全等級的系統(tǒng)中,嚴(yán)格控制操控對象的多個(gè)實(shí)體間的信息流[1]?；诖?國內(nèi)外學(xué)者相繼提出多種信息流安全理論,包括不可推斷理論[2-5]、隔斷理論[6-8]、廣義無干擾理論[9-11]、解析理論[12]和不可演繹理論等。美國計(jì)算機(jī)科學(xué)實(shí)驗(yàn)室的RUSHBY等人改進(jìn)了以往的無干擾理論,提出了信息流領(lǐng)域著名的非傳遞無干擾模型。該模型擴(kuò)展了原始無干擾理論,并解釋了信道控制機(jī)制的一般化安全策略和協(xié)議。INI模型的核心思想是:無干擾能夠捕獲從高安全等級安全域發(fā)出的動(dòng)作h到低安全等級的安全域發(fā)出的動(dòng)作l的所有因果依賴關(guān)系[13]。這種因果依賴關(guān)系,即若前序安全域未發(fā)出動(dòng)作,則其后續(xù)安全域不能發(fā)出相應(yīng)依賴動(dòng)作。這種依賴性導(dǎo)致了一種不安全通信信道,稱為隱蔽信道,其具有傳送任何從高安全等級安全域到低安全等級安全域信息的能力。

實(shí)際上,許多安全問題遠(yuǎn)遠(yuǎn)超出了最基本的無干擾范圍,尤其在多級安全等級系統(tǒng)中,加密信息的不可傳遞性問題給系統(tǒng)安全帶來極大隱患。如INI[14]的應(yīng)用示例是對密碼系統(tǒng)建模的3-域安全等級系統(tǒng),包括高安全等級安全域H、低安全等級安全域L以及降級安全域D。為確保來自私人的加密信息不會(huì)被輕易泄露給未加密的公共安全域,該系統(tǒng)僅允許安全域H發(fā)出的動(dòng)作h經(jīng)安全域D降級后才能干擾安全域發(fā)出的動(dòng)作l,即從H的視角觀察到的系統(tǒng)環(huán)境不能從L的視角觀察到,除非該觀察已被降級至L的視角層次。

由于非傳遞無干擾模型默認(rèn)系統(tǒng)安全域間的安全策略是隨進(jìn)程的推進(jìn)持續(xù)保持穩(wěn)定的,因此RUSHBY等人的理論模型未能考慮到系統(tǒng)運(yùn)行狀態(tài)改變帶給安全域間信息流干擾關(guān)系改變的影響。為將系統(tǒng)運(yùn)行狀態(tài)納入對整體可信性的考量,文獻(xiàn)[5]提出一種新的信息流傳遞模型——?jiǎng)討B(tài)非傳遞無干擾(Dynamic INI,DINI)模型[15]。該模型利用有限狀態(tài)自動(dòng)機(jī)對系統(tǒng)進(jìn)行建模,并將系統(tǒng)狀態(tài)與安全策略關(guān)聯(lián),即動(dòng)作的發(fā)生必然導(dǎo)致系統(tǒng)狀態(tài)的變化,同時(shí)產(chǎn)生對應(yīng)輸出,此時(shí)系統(tǒng)運(yùn)行時(shí)環(huán)境成為進(jìn)程間信息流干擾關(guān)系的重要考量,安全域u對于安全域v的干擾關(guān)系隨系統(tǒng)狀態(tài)的改變而改變。但DINI的無干擾判定定理為充分條件,對實(shí)體的可信判斷過于嚴(yán)格。

2 基于3-域系統(tǒng)的動(dòng)態(tài)非傳遞無干擾理論

本文研究計(jì)算機(jī)系統(tǒng)中進(jìn)程間的信息流傳遞。進(jìn)程由一系列特定的動(dòng)作構(gòu)成,隨著運(yùn)行的推進(jìn),系統(tǒng)環(huán)境不斷發(fā)生變化。一個(gè)動(dòng)作的結(jié)束驅(qū)使下一個(gè)動(dòng)作的開始,進(jìn)而引起系統(tǒng)狀態(tài)的轉(zhuǎn)變。進(jìn)程中動(dòng)作在系統(tǒng)函數(shù)的指導(dǎo)下進(jìn)行訪問操作(包括直接和間接訪問),依賴不同系統(tǒng)狀態(tài)產(chǎn)生不同輸出,同時(shí)系統(tǒng)也進(jìn)入一個(gè)新的狀態(tài)。下文將給出系統(tǒng)信息流傳遞模型的形式化定義。

2.1 形式化定義

現(xiàn)假設(shè)有計(jì)算機(jī)系統(tǒng)C,抽象為一個(gè)六元組C=(S,A,O,D,F,R)。該六元組中的元素解釋如下。

S為系統(tǒng)狀態(tài)集合,使用s表示系統(tǒng)狀態(tài):

S={s0,si,sn}

(1)

其中,s0為系統(tǒng)初始狀態(tài),si為系統(tǒng)中間的某一狀態(tài),n為系統(tǒng)的狀態(tài)總數(shù)。

A為系統(tǒng)動(dòng)作集合,指系統(tǒng)自身發(fā)出的控制動(dòng)作或輸入性質(zhì)的動(dòng)作,使用a表示系統(tǒng)動(dòng)作。

A*為系統(tǒng)動(dòng)作序列,使用α表示系統(tǒng)動(dòng)作序列,即一系列連續(xù)執(zhí)行的系統(tǒng)動(dòng)作。

O為系統(tǒng)輸出集合。

D為系統(tǒng)進(jìn)程集合,每個(gè)進(jìn)程映射為一個(gè)安全域,且互為對應(yīng)關(guān)系,使用u表示安全域(進(jìn)程):

1)安全域(進(jìn)程)間通過動(dòng)作進(jìn)行交互。

2)每個(gè)安全域(進(jìn)程)均可執(zhí)行相應(yīng)動(dòng)作。

3)安全域(進(jìn)程)可觀察到動(dòng)作的輸出結(jié)果。

4)本文對安全域與進(jìn)程的概念不加區(qū)分,且直接使用安全域表示概念。

F為系統(tǒng)函數(shù)集合,包括以下函數(shù):

1)系統(tǒng)狀態(tài)單步轉(zhuǎn)換函數(shù):

step:S×A→S

(2)

step(si,a)=sj表示系統(tǒng)C在狀態(tài)si下執(zhí)行動(dòng)作a后,將轉(zhuǎn)變到狀態(tài)sj。

2)系統(tǒng)輸出函數(shù):

output:S×A→S

(3)

output(s,a)表示系統(tǒng)C在狀態(tài)s下執(zhí)行動(dòng)作a后的輸出結(jié)果。

3)系統(tǒng)動(dòng)作從屬函數(shù):

dom:A→D

(4)

dom(a)=u表示動(dòng)作a是由安全域u發(fā)出的。

4)系統(tǒng)運(yùn)行狀態(tài)轉(zhuǎn)換函數(shù)(系統(tǒng)狀態(tài)單步轉(zhuǎn)換函數(shù)的擴(kuò)展):

run:S×A*→S

(5)

run(si,α)=sj表示系統(tǒng)C在狀態(tài)αi下執(zhí)行動(dòng)作序列α(即一系列連續(xù)執(zhí)行的系統(tǒng)動(dòng)作)后,將轉(zhuǎn)變到狀態(tài)sj,有:

run(s,?)=s

(6)

run(s,aα)=run(step(s,a),α)

(7)

R為系統(tǒng)C上的二元關(guān)系集,R={～>,>},其中,～>表示安全域集合D上的干擾關(guān)系。

若安全域u發(fā)出的動(dòng)作會(huì)影響安全域v上的系統(tǒng)輸出,則稱安全域u對安全域v具有干擾關(guān)系,記為u～>v,否則稱安全域u對安全域v無干擾關(guān)系,記為u>v且干擾關(guān)系具有自反性。

?u∈D,u～>u

(8)

2.2 系統(tǒng)實(shí)例

現(xiàn)假設(shè)有系統(tǒng)C?A*,且系統(tǒng)C由有限自動(dòng)機(jī)G=(A,X,δ,x0)生成。將動(dòng)態(tài)非傳遞無干擾理論應(yīng)用到以下2個(gè)系統(tǒng)實(shí)例中。

實(shí)例1假設(shè)系統(tǒng)C為2-域系統(tǒng),包括所包含已分類信息的高安全級別的安全域H和所包含未分類信息的低安全級別的安全域L,即系統(tǒng)安全域集D={H,L}。安全域間的無干擾關(guān)系為:

～>={(L,H)}

(9)

即系統(tǒng)C中僅L>H,而H>L。

令h∈AH,l∈AL,且系統(tǒng)中存在2種有限自動(dòng)機(jī),分別為G1和G2,如圖1所示。

圖1 有限自動(dòng)機(jī)G1和G2

圖1給出了系統(tǒng)C可能的行為解釋。在有限自動(dòng)機(jī)G1的情況下,安全域L在初始狀態(tài)下不能執(zhí)行動(dòng)作l,而在其第二狀態(tài)下,即當(dāng)安全域H執(zhí)行完動(dòng)作h后,安全域L能夠執(zhí)行動(dòng)作l。由此可見,由安全域H發(fā)出的動(dòng)作h干擾了安全域L的后續(xù)行為,即安全域H中已分類的信息被泄漏到了信息未分類的安全域L中,違背了假設(shè)的系統(tǒng)C中的干擾關(guān)系(L>H,H>L)。因此,有限自動(dòng)機(jī)G1不滿足無干擾關(guān)系。在有限自動(dòng)機(jī)G2中,安全域L可在系統(tǒng)C任意狀態(tài)下執(zhí)行動(dòng)作l,而不受安全域H發(fā)出的動(dòng)作的影響,因此,有限自動(dòng)機(jī)G2滿足無干擾關(guān)系。

實(shí)例2在實(shí)例1的基礎(chǔ)上,假設(shè)系統(tǒng)C為3-域系統(tǒng),系統(tǒng)安全域集D={H,D,L},其中安全域D為降級域。安全域間的無干擾關(guān)系為:

～>={(H,D),(D,L),(D,H),(L,D),(L,H)}

(10)

即系統(tǒng)C中僅H>L。

令h∈AH,d∈AD,l∈AL,且系統(tǒng)中存在2種有限自動(dòng)機(jī),分別為G3和G4,如圖2所示。

圖2 有限自動(dòng)機(jī)G3和G4

圖2(a)中的有限自動(dòng)機(jī)G3也不滿足非傳遞無干擾關(guān)系,因?yàn)榘踩騆發(fā)出的動(dòng)作l不能在hd后的狀態(tài)下出現(xiàn),卻在hdh后的狀態(tài)下發(fā)生,即安全域H發(fā)出的動(dòng)作h干擾了動(dòng)作l的發(fā)生。但圖2(b)中的有限自動(dòng)機(jī)G4不存在這樣的情況:低安全級別的安全域L在動(dòng)作h發(fā)生的前后狀態(tài)下均可發(fā)生,同理,經(jīng)過降級安全域D后,連續(xù)動(dòng)作ll也可在動(dòng)作h發(fā)生的前后狀態(tài)下發(fā)生。可見,高安全級別的安全域H對低安全級別的安全域L無直接干擾關(guān)系,滿足系統(tǒng)假設(shè)(H>L)。而在降級安全域D發(fā)出動(dòng)作d的前后狀態(tài)下,安全域H是可以通過安全域D對安全域L產(chǎn)生干擾的,即高安全級別的安全域H對低安全級別的安全域L有間接干擾關(guān)系,同樣滿足題設(shè)。

3 iP-可觀測屬性

本文以下內(nèi)容均基于3-域系統(tǒng),即系統(tǒng)安全域集D={H,D,L},其中安全域D為降級域。安全域間的無干擾關(guān)系見式(10)。在該3-域系統(tǒng)中,僅低安全等級的安全域L對高安全等級安全域H存在干擾問題,即允許L>H,而H>L。

3.1 屬性引入

引入iP-可觀測屬性,實(shí)現(xiàn)對系統(tǒng)可信判定的充分必要條件。系統(tǒng)K滿足DINI當(dāng)且僅當(dāng)對于(A*,AL),系統(tǒng)K滿足動(dòng)態(tài)iP-可觀測屬性。

由于已有對(A*,AL)檢查系統(tǒng)K是否滿足動(dòng)態(tài)iP-可觀測屬性的前提,因此D-iPurge(s,α,l)等價(jià)于D-iPurge(s,α)。

為檢查系統(tǒng)C是否滿足DINI,可通過檢查系統(tǒng)C是否滿足動(dòng)態(tài)iP-可觀測屬性。由于現(xiàn)有算法都是關(guān)于動(dòng)態(tài)P-可觀測屬性,因此考慮引入iP-可觀測屬性,由有限狀態(tài)自動(dòng)機(jī)對其進(jìn)行演化,在2種可觀測屬性之間產(chǎn)生關(guān)聯(lián),并針對動(dòng)態(tài)系統(tǒng)環(huán)境采用P-可觀測屬性檢查算法,在確認(rèn)系統(tǒng)是否滿足DINI理論的同時(shí),給出系統(tǒng)可信判定的充分必要條件。文獻(xiàn)[15]通過從原始系統(tǒng)K構(gòu)造的新的系統(tǒng)KiP,給出系統(tǒng)K的iP-可觀測屬性與系統(tǒng)KiP的等價(jià)性證明。

3.2 系統(tǒng)可信判定

定義生成KiP的有限自動(dòng)機(jī)G=(A,X,δ,x0)。

令K=L(G),GiP=(AiP,X,δiP,x0),其中過渡函數(shù)δiP:X×AiP→X定義如下:

(11)

若有限自動(dòng)機(jī)G在初始狀態(tài)下,不包含降級安全域D中自循環(huán)的動(dòng)作,則生成系統(tǒng)KiP的狀態(tài)機(jī)為GiP,即KiP=L(GiP),且通過去除有限自動(dòng)機(jī)G在初始狀態(tài)下包含的所有降級安全域D中自循環(huán)的動(dòng)作得到有限狀態(tài)機(jī)F,且J=L(F),則對于(A*,AL)而言,當(dāng)且僅當(dāng)J滿足iP-可觀測屬性,系統(tǒng)C滿足iP-可觀測屬性。引入iP-可觀測屬性后的系統(tǒng)可信判定流程中,P-可觀測屬性檢查算法步驟如下:

4)系統(tǒng)KiP滿足P-可觀測屬性,當(dāng)且僅當(dāng)其所有可能的狀態(tài)都具有一致性。

系統(tǒng)可信判定流程如圖3所示。

圖3 系統(tǒng)可信判定流程

針對現(xiàn)有系統(tǒng)動(dòng)態(tài)可信判定要求過于嚴(yán)格,且直接對系統(tǒng)進(jìn)行iP-可觀測屬性檢查難度較大的問題,本文對系統(tǒng)進(jìn)程進(jìn)行最小動(dòng)作序列約簡,即從高安全級別域出發(fā),替換所有不可觀察的動(dòng)作,將降級安全域初始狀態(tài)下可能存在的自循環(huán)動(dòng)作解循環(huán),生成系統(tǒng)有限狀態(tài)自動(dòng)機(jī)。該狀態(tài)下若低安全級別的安全域在所有狀態(tài)下都被定義,或者都未被定義,則系統(tǒng)滿足一致性要求。而當(dāng)系統(tǒng)所有狀態(tài)下都滿足一致性要求,則系統(tǒng)滿足P-可觀測屬性,進(jìn)而滿足系統(tǒng)DINI理論,完成對系統(tǒng)可信性的判定。

4 實(shí)驗(yàn)與結(jié)果分析

4.1 系統(tǒng)實(shí)例設(shè)計(jì)

假設(shè)有限自動(dòng)機(jī)G,其中包括3-域系統(tǒng),且h∈AH,d∈AD,l∈AL,如圖4所示。系統(tǒng)實(shí)例設(shè)計(jì)如下:

1)計(jì)算自動(dòng)機(jī)G的最小動(dòng)作序列,如圖5所示。

2)根據(jù)ADiP={[aα′]|α′∈L(G′)∧a∈AD∧aα′∈L(G)}得到ADiP={[hd],[hdh],[lld],[lldh]}。

3)自動(dòng)機(jī)GiP如圖6所示。

6)經(jīng)檢查,KiP滿足動(dòng)態(tài)P-可觀測屬性,即系統(tǒng)K滿足DINI。

圖4 帶有循環(huán)的自動(dòng)機(jī)G

圖5 自動(dòng)機(jī)G的最小動(dòng)作序列

圖6 自動(dòng)機(jī)GiP

圖7 自動(dòng)機(jī)

圖8 自動(dòng)機(jī)

4.2 系統(tǒng)實(shí)例驗(yàn)證

本文用于驗(yàn)證系統(tǒng)動(dòng)態(tài)可信判定功能的實(shí)驗(yàn)在基于龍芯3A2000處理器的硬件可信平臺(tái)上進(jìn)行,軟件環(huán)境為集成有虛擬可信平臺(tái)模塊的 Ubuntu Core 16.0.2 LTS 精簡操作系統(tǒng),構(gòu)建系統(tǒng)啟動(dòng)前的可信計(jì)算環(huán)境,并在啟動(dòng)后首次進(jìn)行靜態(tài)可信度量,確保系統(tǒng)運(yùn)行前的環(huán)境可信。

本文進(jìn)行以下仿真驗(yàn)證,以充分驗(yàn)證4.1節(jié)系統(tǒng)實(shí)例的有效性。

為簡化不必要的的影響因素,對實(shí)例作如下模擬:

1)可信系統(tǒng)環(huán)境中設(shè)置3個(gè)進(jìn)程:process_A,process_B,process_C,分別對應(yīng)高安全級別域、降級可信通道以及低安全級別域。

2)可信系統(tǒng)運(yùn)行時(shí),process_A可通過process_B訪問process_C,訪問操作包括對低安全級別域的讀(觀察)、寫(修改)以及調(diào)用3種。

3)系統(tǒng)設(shè)置有全局變量activeProcess,用來標(biāo)記當(dāng)前激活的進(jìn)程,幫助系統(tǒng)識(shí)別實(shí)時(shí)信息流的走向。

4)進(jìn)程間的每一步操作都將基于上一步操作可信的前提下進(jìn)行,當(dāng)系統(tǒng)完成預(yù)定訪問操作后,若系統(tǒng)仍處于可信狀態(tài),則會(huì)輸出“The output can be trusted.”,否則,將輸出“The output can not be trusted.”。

系統(tǒng)可信初始化過程如圖9所示。正常運(yùn)行開始后,系統(tǒng)會(huì)首先剔除所有不可觀察的動(dòng)作,將降級安全域初始狀態(tài)下可能存在的自循環(huán)動(dòng)作解循環(huán),并始終保持可信的狀態(tài)直至結(jié)束。此時(shí),若注入錯(cuò)誤,即修改讀(觀察)、寫(修改)以及調(diào)用系統(tǒng)函數(shù),添加進(jìn)程日志功能,記錄下系統(tǒng)訪問操作的每一步運(yùn)行過程,顯然這破壞了可信系統(tǒng)的完整性和機(jī)密性。此時(shí),當(dāng)系統(tǒng)運(yùn)行完畢,則會(huì)不接受系統(tǒng)的輸出,并提示用戶輸出不可信,如圖10所示。

圖9 系統(tǒng)可信初始化過程

圖10 系統(tǒng)可信判定過程

系統(tǒng)運(yùn)行時(shí),進(jìn)程間的每一步的訪問操作均基于自動(dòng)機(jī)轉(zhuǎn)換后的可信判定結(jié)果,且成功檢測出系統(tǒng)可信狀態(tài)的改變,并提示用戶輸出不可信,從而驗(yàn)證了4.1節(jié)中系統(tǒng)實(shí)例的有效性。

5 結(jié)束語

本文從無干擾理論、系統(tǒng)狀態(tài)可觀察性和系統(tǒng)狀態(tài)影響因素3個(gè)方面出發(fā),構(gòu)建一種基于iP-可觀測屬性檢查的動(dòng)態(tài)非傳遞無干擾模型,將系統(tǒng)狀態(tài)的變化因素關(guān)聯(lián)到系統(tǒng)安全策略中,并引入iP-可觀測屬性,得到對系統(tǒng)DINI檢查的充分必要條件。最后結(jié)合實(shí)例給出預(yù)設(shè)系統(tǒng)的P-可觀測屬性判定算法。下一步將結(jié)合自動(dòng)機(jī)模型轉(zhuǎn)換方法對DINI理論的充分必要條件進(jìn)行詳細(xì)證明。