基于iP-可觀測屬性的動態非傳遞無干擾模型

迮 愷,陳 丹,莊 毅

(南京航空航天大學 計算機科學與技術學院,南京 211106)

0 概述

由于分布式系統和計算機網絡的快速發展,以及經濟全球化帶來的電子通信的全球化,對安全通信協議的需求也達到前所未有的高度。自二十世紀九十年代以來,嵌入式系統在軍事、工業和家用電器等方面得到了廣泛的應用。可信性作為操作系統最重要的屬性之一,已成為嵌入式系統重點研究的方向。但現有系統可信判定模型大多局限于系統啟動后對實體的靜態可信判定,且對于系統進程可信的判斷過于苛刻,系統動態可信的判定僅停留在充分性的解釋,難以完整支撐系統動態可信理論。

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

1 研究背景

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

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

由于非傳遞無干擾模型默認系統安全域間的安全策略是隨進程的推進持續保持穩定的,因此RUSHBY等人的理論模型未能考慮到系統運行狀態改變帶給安全域間信息流干擾關系改變的影響。為將系統運行狀態納入對整體可信性的考量,文獻[5]提出一種新的信息流傳遞模型——動態非傳遞無干擾(Dynamic INI,DINI)模型[15]。該模型利用有限狀態自動機對系統進行建模,并將系統狀態與安全策略關聯,即動作的發生必然導致系統狀態的變化,同時產生對應輸出,此時系統運行時環境成為進程間信息流干擾關系的重要考量,安全域u對于安全域v的干擾關系隨系統狀態的改變而改變。但DINI的無干擾判定定理為充分條件,對實體的可信判斷過于嚴格。

2 基于3-域系統的動態非傳遞無干擾理論

本文研究計算機系統中進程間的信息流傳遞。進程由一系列特定的動作構成,隨著運行的推進,系統環境不斷發生變化。一個動作的結束驅使下一個動作的開始,進而引起系統狀態的轉變。進程中動作在系統函數的指導下進行訪問操作(包括直接和間接訪問),依賴不同系統狀態產生不同輸出,同時系統也進入一個新的狀態。下文將給出系統信息流傳遞模型的形式化定義。

2.1 形式化定義

現假設有計算機系統C,抽象為一個六元組C=(S,A,O,D,F,R)。該六元組中的元素解釋如下。

S為系統狀態集合,使用s表示系統狀態:

S={s0,si,sn}

(1)

其中,s0為系統初始狀態,si為系統中間的某一狀態,n為系統的狀態總數。

A為系統動作集合,指系統自身發出的控制動作或輸入性質的動作,使用a表示系統動作。

A*為系統動作序列,使用α表示系統動作序列,即一系列連續執行的系統動作。

O為系統輸出集合。

D為系統進程集合,每個進程映射為一個安全域,且互為對應關系,使用u表示安全域(進程):

1)安全域(進程)間通過動作進行交互。

2)每個安全域(進程)均可執行相應動作。

3)安全域(進程)可觀察到動作的輸出結果。

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

F為系統函數集合,包括以下函數:

1)系統狀態單步轉換函數:

step:S×A→S

(2)

step(si,a)=sj表示系統C在狀態si下執行動作a后,將轉變到狀態sj。

2)系統輸出函數:

output:S×A→S

(3)

output(s,a)表示系統C在狀態s下執行動作a后的輸出結果。

3)系統動作從屬函數:

dom:A→D

(4)

dom(a)=u表示動作a是由安全域u發出的。

4)系統運行狀態轉換函數(系統狀態單步轉換函數的擴展):

run:S×A*→S

(5)

run(si,α)=sj表示系統C在狀態αi下執行動作序列α(即一系列連續執行的系統動作)后,將轉變到狀態sj,有:

run(s,?)=s

(6)

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

(7)

R為系統C上的二元關系集,R={～>,>},其中,～>表示安全域集合D上的干擾關系。

若安全域u發出的動作會影響安全域v上的系統輸出,則稱安全域u對安全域v具有干擾關系,記為u～>v,否則稱安全域u對安全域v無干擾關系,記為u>v且干擾關系具有自反性。

?u∈D,u～>u

(8)

2.2 系統實例

現假設有系統C?A*,且系統C由有限自動機G=(A,X,δ,x0)生成。將動態非傳遞無干擾理論應用到以下2個系統實例中。

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

～>={(L,H)}

(9)

即系統C中僅L>H,而H>L。

令h∈AH,l∈AL,且系統中存在2種有限自動機,分別為G1和G2,如圖1所示。

圖1 有限自動機G1和G2

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

實例2在實例1的基礎上,假設系統C為3-域系統,系統安全域集D={H,D,L},其中安全域D為降級域。安全域間的無干擾關系為:

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

(10)

即系統C中僅H>L。

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

圖2 有限自動機G3和G4

圖2(a)中的有限自動機G3也不滿足非傳遞無干擾關系,因為安全域L發出的動作l不能在hd后的狀態下出現,卻在hdh后的狀態下發生,即安全域H發出的動作h干擾了動作l的發生。但圖2(b)中的有限自動機G4不存在這樣的情況:低安全級別的安全域L在動作h發生的前后狀態下均可發生,同理,經過降級安全域D后,連續動作ll也可在動作h發生的前后狀態下發生。可見,高安全級別的安全域H對低安全級別的安全域L無直接干擾關系,滿足系統假設(H>L)。而在降級安全域D發出動作d的前后狀態下,安全域H是可以通過安全域D對安全域L產生干擾的,即高安全級別的安全域H對低安全級別的安全域L有間接干擾關系,同樣滿足題設。

3 iP-可觀測屬性

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

3.1 屬性引入

引入iP-可觀測屬性,實現對系統可信判定的充分必要條件。系統K滿足DINI當且僅當對于(A*,AL),系統K滿足動態iP-可觀測屬性。

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

為檢查系統C是否滿足DINI,可通過檢查系統C是否滿足動態iP-可觀測屬性。由于現有算法都是關于動態P-可觀測屬性,因此考慮引入iP-可觀測屬性,由有限狀態自動機對其進行演化,在2種可觀測屬性之間產生關聯,并針對動態系統環境采用P-可觀測屬性檢查算法,在確認系統是否滿足DINI理論的同時,給出系統可信判定的充分必要條件。文獻[15]通過從原始系統K構造的新的系統KiP,給出系統K的iP-可觀測屬性與系統KiP的等價性證明。

3.2 系統可信判定

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

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

(11)

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

4)系統KiP滿足P-可觀測屬性,當且僅當其所有可能的狀態都具有一致性。

系統可信判定流程如圖3所示。

圖3 系統可信判定流程

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

4 實驗與結果分析

4.1 系統實例設計

假設有限自動機G,其中包括3-域系統,且h∈AH,d∈AD,l∈AL,如圖4所示。系統實例設計如下:

1)計算自動機G的最小動作序列,如圖5所示。

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

3)自動機GiP如圖6所示。

6)經檢查,KiP滿足動態P-可觀測屬性,即系統K滿足DINI。

圖4 帶有循環的自動機G

圖5 自動機G的最小動作序列

圖6 自動機GiP

圖7 自動機

圖8 自動機

4.2 系統實例驗證

本文用于驗證系統動態可信判定功能的實驗在基于龍芯3A2000處理器的硬件可信平臺上進行,軟件環境為集成有虛擬可信平臺模塊的 Ubuntu Core 16.0.2 LTS 精簡操作系統,構建系統啟動前的可信計算環境,并在啟動后首次進行靜態可信度量,確保系統運行前的環境可信。

本文進行以下仿真驗證,以充分驗證4.1節系統實例的有效性。

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

1)可信系統環境中設置3個進程:process_A,process_B,process_C,分別對應高安全級別域、降級可信通道以及低安全級別域。

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

3)系統設置有全局變量activeProcess,用來標記當前激活的進程,幫助系統識別實時信息流的走向。

4)進程間的每一步操作都將基于上一步操作可信的前提下進行,當系統完成預定訪問操作后,若系統仍處于可信狀態,則會輸出“The output can be trusted.”,否則,將輸出“The output can not be trusted.”。

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

圖9 系統可信初始化過程

圖10 系統可信判定過程

系統運行時,進程間的每一步的訪問操作均基于自動機轉換后的可信判定結果,且成功檢測出系統可信狀態的改變,并提示用戶輸出不可信,從而驗證了4.1節中系統實例的有效性。

5 結束語

本文從無干擾理論、系統狀態可觀察性和系統狀態影響因素3個方面出發,構建一種基于iP-可觀測屬性檢查的動態非傳遞無干擾模型,將系統狀態的變化因素關聯到系統安全策略中,并引入iP-可觀測屬性,得到對系統DINI檢查的充分必要條件。最后結合實例給出預設系統的P-可觀測屬性判定算法。下一步將結合自動機模型轉換方法對DINI理論的充分必要條件進行詳細證明。