基于iP-可觀測(cè)屬性的動(dòng)態(tài)非傳遞無(wú)干擾模型

迮 愷,陳 丹,莊 毅

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

0 概述

由于分布式系統(tǒng)和計(jì)算機(jī)網(wǎng)絡(luò)的快速發(fā)展,以及經(jīng)濟(jì)全球化帶來(lái)的電子通信的全球化,對(duì)安全通信協(xié)議的需求也達(dá)到前所未有的高度。自二十世紀(jì)九十年代以來(lái),嵌入式系統(tǒng)在軍事、工業(yè)和家用電器等方面得到了廣泛的應(yīng)用。可信性作為操作系統(tǒng)最重要的屬性之一,已成為嵌入式系統(tǒng)重點(diǎn)研究的方向。但現(xiàn)有系統(tǒng)可信判定模型大多局限于系統(tǒng)啟動(dòng)后對(duì)實(shí)體的靜態(tài)可信判定,且對(duì)于系統(tǒng)進(jìn)程可信的判斷過(guò)于苛刻,系統(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-可觀測(cè)屬性,由有限狀態(tài)自動(dòng)機(jī)對(duì)其進(jìn)行演化,在2種可觀測(cè)屬性之間產(chǎn)生關(guān)聯(lián),并針對(duì)動(dòng)態(tài)系統(tǒng)環(huán)境,采用P-可觀測(cè)屬性檢查算法確認(rèn)系統(tǒng)是否滿足動(dòng)態(tài)非傳遞無(wú)干擾(Intrasitive Noninterference,INI)理論,給出系統(tǒng)可信判定的充分必要條件。最后通過(guò)實(shí)例驗(yàn)證,說(shuō)明P-可觀測(cè)屬性檢查算法的可行性,以及系統(tǒng)可信性與動(dòng)態(tài)非傳遞無(wú)干擾理論的關(guān)聯(lián)性。

1 研究背景

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

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

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

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

本文研究計(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)作的開(kāi)始,進(jìn)而引起系統(tǒng)狀態(tài)的轉(zhuǎn)變。進(jìn)程中動(dòng)作在系統(tǒng)函數(shù)的指導(dǎo)下進(jìn)行訪問(wèn)操作(包括直接和間接訪問(wè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è)安全域,且互為對(duì)應(yīng)關(guān)系,使用u表示安全域(進(jìn)程):

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

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

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

4)本文對(duì)安全域與進(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對(duì)安全域v具有干擾關(guān)系,記為u～>v,否則稱安全域u對(duì)安全域v無(wú)干擾關(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)非傳遞無(wú)干擾理論應(yīng)用到以下2個(gè)系統(tǒng)實(shí)例中。

實(shí)例1假設(shè)系統(tǒng)C為2-域系統(tǒng),包括所包含已分類信息的高安全級(jí)別的安全域H和所包含未分類信息的低安全級(jí)別的安全域L,即系統(tǒng)安全域集D={H,L}。安全域間的無(wú)干擾關(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。由此可見(jiàn),由安全域H發(fā)出的動(dòng)作h干擾了安全域L的后續(xù)行為,即安全域H中已分類的信息被泄漏到了信息未分類的安全域L中,違背了假設(shè)的系統(tǒng)C中的干擾關(guān)系(L>H,H>L)。因此,有限自動(dòng)機(jī)G1不滿足無(wú)干擾關(guān)系。在有限自動(dòng)機(jī)G2中,安全域L可在系統(tǒng)C任意狀態(tài)下執(zhí)行動(dòng)作l,而不受安全域H發(fā)出的動(dòng)作的影響,因此,有限自動(dòng)機(jī)G2滿足無(wú)干擾關(guān)系。

實(shí)例2在實(shí)例1的基礎(chǔ)上,假設(shè)系統(tǒng)C為3-域系統(tǒng),系統(tǒng)安全域集D={H,D,L},其中安全域D為降級(jí)域。安全域間的無(wú)干擾關(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也不滿足非傳遞無(wú)干擾關(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不存在這樣的情況:低安全級(jí)別的安全域L在動(dòng)作h發(fā)生的前后狀態(tài)下均可發(fā)生,同理,經(jīng)過(guò)降級(jí)安全域D后,連續(xù)動(dòng)作ll也可在動(dòng)作h發(fā)生的前后狀態(tài)下發(fā)生。可見(jiàn),高安全級(jí)別的安全域H對(duì)低安全級(jí)別的安全域L無(wú)直接干擾關(guān)系,滿足系統(tǒng)假設(shè)(H>L)。而在降級(jí)安全域D發(fā)出動(dòng)作d的前后狀態(tài)下,安全域H是可以通過(guò)安全域D對(duì)安全域L產(chǎn)生干擾的,即高安全級(jí)別的安全域H對(duì)低安全級(jí)別的安全域L有間接干擾關(guān)系,同樣滿足題設(shè)。

3 iP-可觀測(cè)屬性

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

3.1 屬性引入

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

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

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

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

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

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

(11)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 結(jié)束語(yǔ)

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