(北京工業大學 計算機學院，北京100124)
摘 要：安全域隔離技術是構造可信系統的基本技術之一。本文運用可信計算的思想，在現有的安全域隔離模型的基礎上,定義了安全域間信任關系，提出了域間可信通信的可信管道機制，給出了安全域可信隔離模型的可信性狀態，構建并形式化描述了基于DTE策略的安全域可信隔離模型，提供了驗證模型可信的形式化分析方法，為安全域的可信隔離技術的實現和驗證奠定了基礎。
關鍵字：安全域可信隔離；可信管道；形式化
中圖分類號：TP309 文獻標識碼：A 文章編號：
A Security Domain Trusted Separation Model Based on DTE Policy
Chen Yinjing, Cai Mian,Si Limin, Guo Ying
（School of Computer, Beijing University of Technology , Beijing 100124, China）
Abstract Security domain isolated technology is one basic technologies of constructing a credible system. In this paper, it uses the idea of trusted computing. Base on the existing security domain isolated model, it defines the trusted relationship between the security domain, puts forward the believable pipe mechanism of reliable communication between the domain, gives the credibility state of credible isolation model of security domain, constructs and formal describes the security domain credible isolation model based on the strategy of DTE, provides a formal analysis method of validate credible model, laids the foundation for the implementation and verification of believable isolation technology of security domain.
Key words security domain trusted separation; assured pipeline; formalization.
1 引言
可信計算的基本思想是：首先構建一個信任根，再建立一條信任鏈，從信任根開始到硬件平臺，到操作系統，再到應用，一級認證一級，一級信任一級，把這種信任擴展到整個計算機系統，從而確保整個計算機系統可信[1]。信任鏈傳遞到應用層時，不同的應用程序具有不同的信任度，應用程序之間不做任何隔離的通信會使得信任度產生衰減，因此將不同信任度的程序隔離到不同安全域中對可信系統具有重要意義[2]。
DTE(domain and type enforcement)[3]以及其前身TE(type enforcement)[4]作為有效實施細粒度強制訪問控制的安全策略機制，自提出后已經被廣泛的應用于多個系統和產品中進行安全配置[5，6，7]。安全域隔離技術作為構建可信系統的基本要求之一，是操作系統核心強制執行的一種訪問控制機制，特點是通過嚴格的隔離阻止安全域內部和外部主體非授權地訪問被保護資源，從而實現保密性、完整性、最小特權等安全保護[8,9]。文獻[8]給出安全域隔離模型，但在可信系統構建中，要運用可信計算理論，構建安全域可信隔離模型，研究安全域間的信任關系和域間可信通信問題。
本文的研究基于TCG[10]和ISO/IEC[11]對可信的定義，認為在操作系統運行中的一個實體可信，那么該實體有預期的輸入、輸出以及動作序列。在實現其預期目標時，嚴格地按照預期進行，并得到預期結果。
本文基于可信計算的思想，采用Z形式規范語言，在借鑒安全域隔離模型[8]的基礎上，定義并分析了安全域間信任關系及其性質，提出域間可信通信的通信機制，構建了安全域可信隔離模型，并給出了對安全域可信隔離模型進行形式化分析驗證方法。
2 安全域可信隔離模型
文獻[8]使用Z形式規范語言定義了系統狀態，將DTE策略進行形式化建模，分析了域間信息流，給出安全域隔離模型。本文借鑒其對系統狀態的定義，分析域間信任關系及其性質，提供了域間可信通信的通信機制，得出系統可信狀態。
2.1可信隔離模型初始狀態
域隔離模型的基本要求就是對安全域進行合理的劃分[8]。TCSEC[13]中的域是指主體能夠訪問的客體的集合。安全域隔離模型根據DTE策略通過對主體賦予域標簽實現域的劃分。為了實現細粒度隔離，域中主體權限必須遵守最小特權原則，使得各個域中的主體僅具有實現任務的最小特權。
模型的初始狀態就是對基于DTE策略的安全域模型系統狀態的描述。本文借鑒文獻[8]，將系統的狀態抽象為進程、輸入、輸出、安全域、動作序列、型、主體與域的分配關系及訪問控制列表。下面采用Z語言對系統狀態進行描述。
安全域可信隔離模型初始狀態描述如圖1，稱為模式InitState。
在該模型中，狀態變量包括進程、輸入序列、輸出序列、安全域、動作序列和型，分別定義為：Processes 、Inputs、Outputs、Domains、Actions、Types。主體與域的分配關系表示為：process-domain，主體是指激活的進程，每個進程都有其預期的輸入序列、輸出序列以及動作序列。每個進程可以在域之間進行切換，切換行為是通過調用域入口函數實現的，包括自動切換auto和強制切換enforce。域間的訪問控制許可表：DDT，其中DCT::=auto| enforce,表示進程在進行域間切換時的轉換關系。主體對客體的訪問控制許可表：PPT，其中DTAM::=PRaccess| PWaccess，是主體對客體的訪問模式，包括讀訪問模式和寫訪問模式，并且有PRaccess = { r,x,l,d }，即文件讀(r)、文件執行(x)、目錄讀(l)、目錄執行(d); PWaccess = { w,a,c }，即文件寫(w)、文件追加(a)、目錄寫(c)。PDI是進程對特定域進行輸入的許可表，其中輸入序列必須是預期的。
2.2安全域間信任關系
本節從信任的角度來討論域間通信行為的可信性，即通過分析兩個域間的輸入、輸出及動作序列是否符合主客體的預期，來判斷域間通信行為是否可信。下面給出安全域間信任關系的定義:
定義1：當兩個域U、V滿足：
①V對U進行的操作已經得到授權，并且嚴格執行預期操作；
②V對U進行的操作未得到授權，但該操作并不影響U的輸出，稱域U信任域V。
即對于任意兩個可信域dt和ds，以及任意的兩個進程Pds和Pdt,其中Pds是ds中的進程,Pdt是dt中進程。Pds對Pdt進行訪問操作，操作有如下兩種可能：1Pds對Pdt進行的操作是預期的，即其訪問請求已經獲得授權，若以寫模式進行訪問，其輸入序列是嚴格按照預期的執行；2Pds對Pdt的訪問是非預期，即其訪問行為未獲授權，或者已經獲得授權，但其輸入序列未嚴格按照預期執行。在這兩種情況下，無論Pds對Pdt的訪問行為是預期還是非預期，即使由于Pds的輸入導致Pdt的動作序列與預期不一致，只要Pdt的輸出序列和預期一致，也認為域dt信任ds。用Trust表示系統中兩個域間的信任關系，若dt信任ds，則表示成：Trust(dt,ds) 。
用二元組Trust (U，V)來表示域U信任域V的信任關系，用R表示這類二元組的集合，定義信任關系的對稱性為：
任意的三個域ds、dt、dz,若ds及dt滿足信任關系的對稱性，且dt信任dz，則有ds信任dz，即域ds和dz滿足域間信任關系的傳遞性，表示為H-Trust( ds,dz )。
2.3域間通信機制
在考慮安全域可信隔離的同時，為了使隔離的安全域不受到彼此非預期的影響，要考慮域間通信的問題。本文采用可信管道的域間通信機制，保證信息流動的可信性。
定義4：可信管道是域和域間可信通信的通道。
不同于文獻[1]將可信管道定義為型與型之間傳遞信息的通道，輸入輸出為型，本文定義的可信管道是域與域之間傳遞信息的通道，輸入輸出為域。
將可信管道引入后，隔離模型的狀態需要包含可信管道的集合。所以隔離模型的狀態由T-InitState擴充為模式P-State，如圖5。
可信管道用P-State的謂詞部分描述，由五元組序列組成，該序列中任意相鄰的兩個五元組相鄰的兩個項是相同的，當該序列中五元組個數大于1，即表示可信管道穿過幾個隔離域，當該序列中五元組個數為1，即表示可信管道只在自身域中。
為保證在可信管道中流動的信息可信，可信管道必須具有可控性、屏蔽性、可用性和可認證性�？煽匦员ＷC可信管道的建立以及撤銷都是可控的；屏蔽性保證管道內中的任何事件與管道外界環境都是相互屏蔽的，即管道外的環境無法影響到管道內部數據流動，管道內的事件也無法影響管道外部環境；可用性保證可信管道始終能被有效進程使用；可認證性保證在管道兩端的接收者能夠相互驗證對方身份。因此，為了管道中流動信息的安全性，可信管道必須保證在其中流動的數據具有：機密性、完整性、可驗證性。
在可信管道中的信息流分為兩類：一類是經過授權的信息流；一類是未經過授權的信息流。對于未授權的信息流，它的輸出端須是信任輸入端的。從域U到域V的信息流使用Stream(U，V)表示。
系統中任意兩個進行通信的域ds、dt滿足信任關系Trust(ds,dt)，或滿足H-Trust(ds,dt)，且ds到dt的信息流都經過可信管道，則該安全域可信隔離模型可信。
3 模型可信證明
狀態機模型的證明包括兩類：①證明系統初始狀態的可信性；②對狀態轉化進行可信性證明。當系統初始狀態可信并且狀態轉化過程可信，該模型就是可信的。定理證明器Z/EVES作為對Z形式模型進行驗證的重要工具，為驗證Z形式模型的內在一致性提供了重要途徑。初始狀態可信定理和狀態轉換可信定理可參考Z/EVES自動完成[13]。
3.1初始狀態可信
3.2狀態轉換可信
在建立可信系統之后，必須證明系統中的任何操作都不會改變系統的可信性。表達式為：可信狀
定理的證明可通過Z/EVES工具得出證明結果。
驗證時應該涵蓋所有影響系統狀態的操作，如：客體的創建和刪除，主客客體訪問控制關系的增刪改等。
上面兩類證明可以驗證系統的操作都是可信的，確�？尚畔到y始終處于可信狀態。
4 結論
安全域隔離機制是實現可信系統的關鍵技術。DTE策略作為一種靈活、細粒度的強制訪問控制機制，已經被廣泛應用于系統的安全配置中。本文借鑒了安全域隔離模型，對DTE策略進行形式化描述，運用可信思想，分析研究安全域間通信時的信任關系及其性質，為域間通信提供安全可靠的可信管道機制，從而得出系統處于可信狀態的形式定義。在此基礎上，采用Z/EVES形式驗證工具，提供了驗證系統是否可信的定理證明形式分析方法。本文提供了可信系統的安全域可信隔離形式模型，解決了可信系統可信隔離策略的形式化建模問題，為可信系統可信隔離技術的實現和驗證奠定了基礎，對可信系統的研究和實現做了鋪墊。
參考文獻 (References)
[1]沈昌祥.信息安全綜述[J].中國科學，2007，第37卷，第2期:129-150.
Shen ChangXiang. Information Security Review [J]. Science in China, vol.37, no.2,pp.129-150, 2007 .
[2]黃強.基于可信計算的終端安全體系結構研究[D].海軍工程大學,武漢,2007.
Huang Qiang.Secure Architecture of Terminal Based on Trusted Computing[D]. Naval university of Engineering , wuhan, 2007.
[3] R O’Brien. C Rogers. Developing Applications On lock [C]. The National Computer Security Conf, Washington, 1991.
[4] W E Boebert, R Y Kain. A practical Alternative to Hierarchical Integrity Policies [C].The National Computer Security Conf, Gaithersburg, Maryland, 1985.
[5] Lee Badger, Daniel F Sterne, David L Sherman, et al. A Domain and Type Enforcement Unix prototype [C].The 5th USENIX UNIX Security Symposium, Salt Lake City, 1995
[6] National Security Agency. Security-Enhanced Linux [OL] . http://www.nsa.gov/selinux, 2007.
[7] Serge E Hallyn, Phil Kearns. Tools to Administer Domain and Type Enforcement [C]. The 15th Conf on Systems Administration (LISA 2001) , San Diego, California, 2001.
[8] 卿斯漢.基于DTE策略的安全域隔離Z形式模型[J].計算機研究與發展,2007,(11):1881-1888.
Qing Sihan. A Security Domain Separation Z Model Based on DTE Policy [J].Journal of Computer Research and Development, 2007, 44(11):1881-1888.
[9] Marshall D Abrams, Michael V Joyce. Trusted System Concepts [J] .Computers and Security, 1995, 14(1): 45-56.
[10] Trusted Computing Group .TCG Specification Architecture Overview, Version1.2 [OL].http://www. Trusted_computinggroup.org,.2003.
[11] International Standard ISO /IEC 15408[S]. 2001.
[12] M Saaltink. The Z/EVES System [C]·In: ZUM’97 the Z Formal Specification Notation, LNCS 1212·Berlin: Springer,1997:72-85.
[13] Department of Defense Computer Security Center. DOD5200. 28-STD.Department of Defense Trusted Computer system Evaluation Criteria [S], USA: DOD December 1985.
作者簡介：
陳銀鏡，1985年生，女，廣西百色人，北京工業大學碩士研究生，主要研究方向為信息安全、可信計算。
