基于管道的 TCB擴展模型

廖建華,趙 勇,沈昌祥

(1.北京大學(xué)信息科學(xué)技術(shù)學(xué)院,北京 100871;2.北京工業(yè)大學(xué)計算機學(xué)院,北京 100124;3.中國科學(xué)院軟件研究所信息安全國家重點實驗室,北京 100049)

基于管道的 TCB擴展模型

廖建華1,3,趙 勇2,沈昌祥2

(1.北京大學(xué)信息科學(xué)技術(shù)學(xué)院,北京 100871;2.北京工業(yè)大學(xué)計算機學(xué)院,北京 100124;3.中國科學(xué)院軟件研究所信息安全國家重點實驗室,北京 100049)

為解決當前系統(tǒng)環(huán)境中應(yīng)用安全與系統(tǒng)安全互相獨立而存在的問題,提出了安全管道和TCB擴展的概念,給出了安全管道的形式化描述,并抽象出一種基于安全管道的 TCB擴展模型,說明如何利用 TCB擴展構(gòu)建安全機制間的信息交互機制,以實現(xiàn)不同安全機制之間的統(tǒng)一.通過對 TCB擴展模型的安全性分析,進一步說明了模型的科學(xué)性和現(xiàn)實可行性.

TCB擴展;安全管道;應(yīng)用安全機制;系統(tǒng)安全機制

當前,信息系統(tǒng)安全主要由應(yīng)用安全和操作系統(tǒng)安全[1-3]組成.從概念上講,這些安全機制都屬于TCB的一部分,但是如果沒有從系統(tǒng)整體安全的出發(fā)點考慮,各安全機制之間缺乏協(xié)調(diào)一致性,則容易導(dǎo)致如下問題:其一,操作系統(tǒng)安全機制運行于系統(tǒng)層,具有安全性強、不易被旁路的優(yōu)點,而應(yīng)用系統(tǒng)安全機制面向應(yīng)用,具有應(yīng)用的語義,能實施細粒度的訪問控制.但是如果兩者互相獨立,則不僅不能充分發(fā)揮各自的優(yōu)勢,還有存在安全威脅的可能.應(yīng)用安全做的再完善,如果沒有操作系統(tǒng)安全的支撐,也存在被“抄底”的危險;其二,應(yīng)用安全和操作系統(tǒng)安全都擁有各自獨立的安全策略,多種安全機制共存且缺乏協(xié)調(diào)機制的結(jié)果必然導(dǎo)致其間的相互干擾和沖突,甚至影響信息系統(tǒng)的正常運行.應(yīng)用系統(tǒng)安全與操作系統(tǒng)安全相互獨立,用戶對資源的訪問請求在安全機制之間傳遞過程中存在應(yīng)用語義缺失的問題.

為了解決上述問題,本文提出一種基于安全管道的 TCB擴展模型.采用積極防御全面防護的思想[4],以應(yīng)用系統(tǒng)的安全防護為目標,構(gòu)建與應(yīng)用安全需求一致的系統(tǒng) TCB,TCB由底層往上逐層擴展.通過安全管道將各層安全機制連接成一個有機的整體,避免 TCB內(nèi)部安全機制的重疊以及減少其間的相互沖突,最終形成滿足安全需求的系統(tǒng) TCB.

1 相關(guān)工作

應(yīng)用層安全機制與操作系統(tǒng)安全機制一致性問題的相關(guān)研究可以從考察當前廣泛使用的 Windows系列操作系統(tǒng)入手,安全子系統(tǒng)是 Windows系列操作系統(tǒng)安全的基礎(chǔ)[5-8],除了包括操作系統(tǒng)基本的安全機制之外,也為應(yīng)用系統(tǒng)提供一些安全服務(wù)接口,如 Windows Filtering Platform(WFP).在 Windows 7中,可以通過這套 WFPAPI集將Windows防火墻功能嵌入到所開發(fā)的應(yīng)用系統(tǒng)中.但是這并沒有很好解決應(yīng)用和系統(tǒng)安全的一致性問題,因為沒有對應(yīng)用進程的認證,也沒有為應(yīng)用提供操作系統(tǒng)級的訪問控制支撐,所以應(yīng)用和系統(tǒng)安全機制還是相對獨立,其間的沖突依然存在.

SELinux[9]是當前安全操作系統(tǒng)的代表.在 SELinux中,每個對象(程序、文件、進程等)都擁有一個Security Context(安全上下文),也就是對象的安全標簽,上面記錄著這個對象所具有的安全權(quán)限,并可以通過制定安全策略來定義這些對象所具有的權(quán)限.SELinux運行在操作系統(tǒng)層,通過配置安全策略可以實現(xiàn)對應(yīng)用系統(tǒng)的控制和保護,在一定程度上實現(xiàn)對應(yīng)用安全的支撐.但是由于沒有相應(yīng)的機制將應(yīng)用相關(guān)的語義傳遞給 SElinux,因此無法實現(xiàn)細粒度的安全支撐.

文章在此提出一種基于管道的 TCB擴展模型,以實現(xiàn)安全機制間的協(xié)調(diào).

2 基于管道的 TCB擴展模型

2.1 模型設(shè)計思路

分析當前大多數(shù)重要應(yīng)用系統(tǒng),其安全機制即系統(tǒng) TCB主要由操作系統(tǒng)訪問控制和應(yīng)用系統(tǒng)訪問控制組成(如圖 1所示).TCB擴展模型要實現(xiàn)不同安全機制間的協(xié)調(diào)一致,包括訪問請求信息的傳遞和策略同步等,因此需要引入一種不同安全機制實體間的專有信息交互機制,用于實現(xiàn) TCB的擴展,模型主要關(guān)注 TCB擴展以及擴展的原則.

2.2 模型安全目標

TCB擴展模型是為了構(gòu)建安全實體間的安全管道,具體安全目標如下:

1)保證安全實體的可信.可信是安全的保證,因此,TCB擴展首先要做到的就是驗證上層安全機制實體的可信.

2)協(xié)調(diào)安全機制間的接口.原始的訪問請求信息需要以安全管道的格式交互,因此安全機制間需要一致的接口,接口的格式需要根據(jù)實際需求由上下層安全機制通過 TCB擴展協(xié)議協(xié)商確定.

3)安全機制間的安全交互.通過安全管道傳遞的訪問請求信息涉及到對一些重要敏感信息的訪問,因此保證訪問請求信息的機密性和完整性顯得尤為重要.

2.3 模型描述

2.3.1 TCB擴展模型的組成元素

定義 1 基本變量

S表示主體類型的集合,Su∈S、Sl∈S分別表示上下層安全機制相關(guān)的主體集合;O表示客體類型的集合,Ou∈O、Ol∈O分別表示上下層安全機制相關(guān)的客體集合;P表示安全策略類型的集合,Pu∈P、Pl∈P分別表示上下層安全機制相關(guān)的策略集合;A={r,w,rw,e}表示訪問行為集合,分別表示只讀、只寫、讀寫和執(zhí)行;R=S×O×A表示訪問請求類型的集合,Ru=(Su×Ou×A)∈ R、Rl=(Sl×Ol×A)∈ R分別表示上下層訪問請求集合;D={yes,no,error}表示判斷結(jié)果;C表示訪問控制類型的集合,Cu∈C、Cl∈C分別表示上下層訪問控制機制集合.fac∈Cu:Ru×Pu→D×Rl為訪問控制函數(shù),表示對訪問請求的判斷并生成下層安全機制的請求.

定義 2 安全機制定義

M=C×P表示安全機制類型的集合,是訪問控制和安全策略的總和,mu=(Cu,Pu)∈M表示上層安全機制,ml=(Cl,Pl)∈M表示下層安全機制.{m1=(C1,P1),m2=(C2,P2),…,mn=(Cn,Pn)}?M表示系統(tǒng)各層安全機制.

2.3.2 安全管道定義

安全管道是指為實現(xiàn)安全目標而構(gòu)建的 TCB內(nèi)部安全實體間的專有信息交互機制.下面分別從安全管道的交互內(nèi)容、輸入/輸出接口、傳輸方式等方面進行定義.

定義 3 安全機制間交互的內(nèi)容

圖1 應(yīng)用安全體系Fig.1 Architecture of application security

為了實現(xiàn)安全機制間的一致性,安全管道還需要傳遞與訪問請求相關(guān)的附加信息,用 E表示,可以將應(yīng)用相關(guān)的主體信息作為附加信息通過安全管道傳遞到下層安全機制.I表示安全機制間交互的信息,Iu→l=R×E表示上層到下層的訪問請求,Il→u=D表示下層返回的訪問決策信息.

定義 4 安全管道接口

分別用 Hin和 Hout表示輸入輸出接口,則有 Hio=Hin×Hout表示安全管道接口,用 Ich表示在安全管道中傳遞的信息.可得 Hout:I→Ich表示輸出接口對信息的封裝,Hin:Ich→I表示輸入接口對信息進行解封裝,則有:?i∈I?(?hin∈ Hin∧?hout∈Hout∧i=hout(hin(i)))表示通過管道輸入接口進入安全管道的信息能原封不動地從安全管道的輸出接口輸出,以此保證傳輸信息的一致性.

定義 5 安全管道的安全傳輸機制

安全管道需要保證傳輸信息的完整性和機密性,用 Hsec表示信息保護機制,在此采用密碼機制對信息進行安全保護,在傳遞前對信息進行加密處理,到達對端再解密,用 Ienc表示加密后的信息,Henc:Ich→Ienc表示對信息加密處理,Hdec:Ienc→Ich表示對信息解密處理,則有 Hsec=Henc×Hdec,管道傳輸信息的安全可以通過如下公式保證:

定義 6 安全管道協(xié)商機制

定義 3～5構(gòu)成的安全管道的基本屬性需要通過協(xié)商機制協(xié)商確定.用 N表示協(xié)商機制.Ninfo:Mu×Ml→I表示依據(jù)上下層安全機制協(xié)商需要通過管道傳遞的內(nèi)容;Nio:Mu×Ml×I→Hio表示接口協(xié)商;Nsec:Mu×Ml×I×Hio→Hsec表示協(xié)商管道信息安全傳輸機制.且有 N=Ninfo×Nio×Nsec.

定義 7 安全管道

定義 3～6的內(nèi)容共同構(gòu)成了安全管道的基本要素,現(xiàn)在給出安全管道的形式化定義,即 H=I×Hio×Hsec×N.hl?u∈H表示安全機制 ml、mu之間的安全管道.

2.3.3 安全管道的性質(zhì)上節(jié)給出了安全管道的形式化定義,現(xiàn)在結(jié)合安全管道所具有的屬性,分析安全管道所具有的性質(zhì).性質(zhì) 1 傳遞豐富的訪問請求信息.由定義 3可知,I=R×D×E表示安全管道除了可傳遞原始的訪問請求信息 R×D外,還可以根據(jù)安全的需要傳遞附加信息 E.

性質(zhì) 2 保證傳輸信息的安全.安全管道的 Hsec屬性能保證傳遞信息的完整性和機密性,從邏輯上形成一個封閉的管道.

性質(zhì) 3 訪問請求傳遞的單向性.由定義 3 Iu→l=R×E,Il→u=D可知,訪問請求信息只能由上層安全機制單向請求下層安全機制.

2.3.4 TCB擴展步驟

TCB擴展的目標是要構(gòu)建安全機制之間符合安全需求的管道,因此,其擴展過程要充分結(jié)合安全管道的屬性而展開.擴展步驟作為 TCB擴展模型的一部分需要進行更具體的描述.

TCB管道擴展可以分為 4個步驟.

步驟 1 可信認證 TCB擴展首先須保證安全機制的可信 可以通過完整性驗證機制保證,定義認證函數(shù)為 fcert:M→{true,false}.

步驟 2 協(xié)商交互內(nèi)容 函數(shù) fnegoinfo∈Ninfo:Ml×Mu→I用于協(xié)商需要通過安全管道交互的內(nèi)容,比如在下層安全機制缺少應(yīng)用相關(guān)的主體信息的情況下,可通過管道傳遞相應(yīng)的主體信息.

步驟 3 協(xié)商管道接口 管道信息以何種方式傳遞也是需要在管道構(gòu)建之初協(xié)商確定的,函數(shù) fnegoio∈Nio:I→Hio用以協(xié)商管道接口.

步驟 4 協(xié)商通信安全機制 由安全管道的定義可知,安全交互是安全管道的一個基本屬性,函數(shù)fnegosec∈ Nsec:Ml×Mu→Hsec用以協(xié)商通信安全機制.

圖2 TCB擴展步驟Fig.2 Steps of TCB extension

定義 8 TCB擴展

擴展函數(shù) ftcbext:M×M→H表示通過 TCB擴展構(gòu)建安全機制之間的安全管道,有

定義 9 系統(tǒng) TCB

由定義 2可知,對于安全機制可分為 n層的系統(tǒng),Ms={m1,m2,…,mn}?M,在此定義的 TCB是安全機制加上通過 TCB擴展而得到的安全管道構(gòu)成,則有

2.3.5 TCB擴展規(guī)則

規(guī)則 1 安全機制可信規(guī)則 TCB擴展在構(gòu)建安全管道之前,需要對上層安全機制進行可信驗證,通過層層可信驗證,能保證最終擴展形成的系統(tǒng) TCB整體的安全可信.

規(guī)則 2 自下而上擴展規(guī)則 由于系統(tǒng)安全機制具有層次性的特點,因此,TCB擴展模型需遵從自下而上的擴展規(guī)則.

規(guī)則 3 主體一致性規(guī)則 由定義 1可知訪問請求 R=S×O×A,通常情況下,客體和操作行為是與當前上下文相關(guān)的,底層訪問控制機制能獲取得到,但是主體信息通常會發(fā)生變化,應(yīng)用層主體信息往往無法傳遞到操作系統(tǒng)安全機制層.因此,我們在TCB擴展時需遵守主體一致性規(guī)則,保證每層都能實施準確的訪問控制.

以上描述的安全管道的定義、TCB擴展步驟和擴展規(guī)則共同構(gòu)成了 TCB的擴展模型.

3 模型安全性分析

定理 1 經(jīng) TCB擴展模型擴展而得的系統(tǒng) TCB是可信的.

證明:由定義 9可知,系統(tǒng) TCB可以定義為:TCB={m1,h1?2,m2,…,mn-1,hn-1?n,mn},要證明系統(tǒng)TCB是可信的,需要證明系統(tǒng) TCB內(nèi)部各元素是可信的.

首先證明 TCB內(nèi)安全機制是可信的,由模型的步驟 1可知,TCB內(nèi)部的所有安全機制 Ms={m1,m2,…,mn}?M在擴展過程中都有 fcert(mi)=true,i∈{1,2,…,n}保證,因此,TCB內(nèi)部安全機制是可信的.

現(xiàn)在證明 TCB內(nèi)安全管道是可信的,由定義 8可知,hi?i+1=ftcbext(mi,mi+1),i∈{1,2,…,n},再由上文證明的 Ms={m1,m2,…,mn}?M是可信的,且擴展函數(shù)是可信的,可得 hi?i+1,i∈{1,2,…,n}是可信的.

因此,由以上 2點可得經(jīng)擴展后得到的系統(tǒng) TCB是可信的.定理 1得證.

定理 2 TCB擴展模型實現(xiàn)應(yīng)用語義的全程傳遞.

證明:定理的證明轉(zhuǎn)化為證明與應(yīng)用相關(guān)的訪問請求信息 r能無歧義地傳遞到系統(tǒng) TCB各層.現(xiàn)假設(shè)系統(tǒng) TCB從下往上可以分為 n層,即 Ms={m1,m2,…,mn},采用本文提出的擴展模型將此 n層安全機制擴展形成有機的系統(tǒng) TCB,可認為最上層的訪問請求是與應(yīng)用相關(guān)的,具有應(yīng)用的語義,則定理命題可表示為

首先證明 r∈ Rn-1,由 TCB擴展模型規(guī)則 3,可知 r∈ In,由定義 4可知 In=In-1,則有 r∈ In-1?r∈Rn-1.同理,可證明 r∈ Rn-2,…,r∈ R1.

定理 2得證.

定義 10 問請求可信通路

所謂訪問請求可信通路是指資源訪問請求能無差別的由發(fā)起端傳遞到最終的請求執(zhí)行端,包含訪問請求信息的完整性和機密性 2層含義.

定理 3 TCB擴展模型能構(gòu)建資源訪問請求的可信通路.

證明:訪問請求信息的安全威脅主要體現(xiàn)在安全機制間傳遞過程中,由定義 5可知

由此可得,安全管道的安全通信屬性可以保證信息在管道傳遞過程中的安全.

定理 3得證.

以上給出了 TCB擴展模型的 3個安全定理,以 2.2節(jié)提出的 TCB擴展的安全目標作為依據(jù)進行對照分析可知,我們提出的擴展模型可以實現(xiàn)其預(yù)定的安全目標.

4 結(jié)束語

本文針對當前系統(tǒng)安全機制間互相獨立、存在沖突等問題,提出通過 TCB擴展解決此類問題的一般方法,即基于安全管道的 TCB擴展模型.對擴展模型的論證分析說明了模型的科學(xué)性和現(xiàn)實可行性.本文給出的擴展模型只是說明TCB擴展的一般步驟,至于 TCB擴展模型所涉及到的用于構(gòu)建安全管道的幾個協(xié)議,需要更深入的研究.本文所針對的無論是應(yīng)用層還是系統(tǒng)層的安全機制都可自主修改.對于安全機制無法修改的情況,如何實施 TCB的擴展也是下一步需要研究的內(nèi)容.

[1]MOHAN C.Survey of recent operating systems research,designs and implementations[J].ACM SIGOPS Operating Systems Review,1978,12(1):53-89.

[2]KRISTAL T P,SCOTT A B.Efficient access control for distributed hierarchical file systems[C]∥Proceedings of the 22nd IEEE/13th NASA Goddard Conference on Mass Storage Systems and Technologies.Washington DC,USA:IEEE Computer Society,2005:253-260.

[3]卿斯?jié)h,劉文清,溫紅子.操作系統(tǒng)安全[M].北京:清華大學(xué)出版社,2004:234-256.

[4]沈昌祥.構(gòu)建積極防御綜合防范的防護體系[J].信息安全與通信保密,2004,41(5):18-20.SHEN Chang-xiang.Build up protection system of active defense and comprehensive on-guard[J].China Information Security,2004,41(5):18-20.(in Chinese)

[5]PHILLIPS L.Windows Vista security:first impressions[J].Information Security Tech Report,2006,11(4):176-185.

[6]MICHAEL H,STEVE L.Inside the Windows security push[J].IEEE Security and Privacy,2003,1(1):57-61.

[7]NIK O.Overview of Windows NT security subsystem[J].Sys Admin,1998,7(7):8-16.

[8]BOB R.Inside Windows NT security[J].Windows/DOS Developer's Journal,1993,4(4):6-19.

[9]MICK B.Paranoid penguin:introduction to SE Linux[J].Linux Journal,2007,2007(154):1-15.

(責任編輯 張 蕾)

Channel-Based TCB Extension Model

LIAO Jian-hua1,3,ZHAO Yong2,SHEN Chang-xiang2
(1.School of Electronics Engineering and Computer Science,Peking University,Beijing 100871,China;2.College of Computer Science,Beijing University of Technology,Beijing 100124,China;3.State Key Laboratory of Information Security,Institute of Software,Chinese Academy of Sciences,Beijing 100049,China)

To solve the problems derived from isolation of application security mechanism and operation system security mechanism,firstly,the concept of security channel and TCB extension was p roposed,and then formal description of security channelwasgiven.By practices,a TCB extension modelwhich based on security channel was obtained.This model could be used to explain how to build security channel between different security mechanisms in order to achieve uniform and eliminate conflicts of those security mechanisms.Finally the theory and practicality of thismodel with security analysis and engineering implementation were proven.

TCB extension;security channel;application security mechanism;operation system security mechanism

TP 309

A

0254-0037(2010)05-0592-05

2009-12-10.

國家“八六三”計劃資助項目(2009AA 01Z437);國家“九七三”計劃資助項目(2007CB311100);信息安全國家重點實驗室開放課題.

廖建華(1978—),男,江西寧都人,博士研究生.