以彩色派翠網對 Security-Enhanced Linux 安全政策資訊流進行驗證之研究

Information Flow Query and Verification for Security Policy of Security-Enhanced Linux Using CPN

高永威(Yung-Wei Kao)

指導教授 ： 陳奕明

國立中央大學/管理學院/資訊管理學系/碩士(2006年)

摘要

本論文提出一套使用 CPN (Coloured Petri Net) 的方法來分析 SELinux (Security-Enhanced Linux) 中安全政策的資訊流。資訊流是系統中主體與受體之間的資訊交換。而一般的存取控制也就是對於各種類型資訊流的控管。SELinux 的存取控制機制是基於其安全政策，代表著系統中所有允許的資訊流都會定義在此安全政策之中。一個標準的 SELinux 安全政策就包含了二十多萬行的規則。因此，對於政策管理者而言，如何確定所制定的政策真的有符合事先定義的安全目標，將是一個重大的挑戰。為了解決此問題，本研究提出一套正規的資訊流模型來描述 SELinux 安全政策，並且提出一套 Query 語言來幫助管理者表示他所期望 / 不期望的資訊流。我們開發了一套方法將 SELinux 安全政策轉換成 Policy CPN Diagram，並且將安全目標轉換成 Query CPN Diagram。為了達到自動化的分析，我們開發了一套工具，名為 SELAnalyzer，可以驗證 SELinux 安全政策是否滿足安全目標。最後，我們比較相關的研究並且提出一個旁波段網路的範例來說明如何使用我們的工具。

關鍵字

SELinux ； 彩色派翠網 ； 資訊流 ； 安全政策

並列摘要

This paper presents a Colored Petri Nets (CPN) approach to analyze the information flow in the policy file of Security-Enhanced Linux (SELinux). The SELinux access control decisions are based on a security policy file that contains several thousands of security rules. It becomes a challenge for policy administrator to determine whether the modification of the security policy file conforms to the pre-specified security goals. To address this issue, this paper proposes a formal information flow model for SELinux security policy file, and presents a simple query language to help administrators to express the expected/unexpected information flow. We developed a method to transform the SELinux policy and security goal into Policy CPN Diagram and Query CPN Diagram. A tool named SEAnalyzer that can automatically verify the SELinux policy has been developed and two application examples of this tool will be presented in the context.

並列關鍵字

security policy ； information flow ； SELinux ； Colored Petri Nets

參考文獻

[黃嘉欣 2004] 黃嘉欣，一種以彩色派翠網為基礎的 SELinux 安全政策分析工具，國立中央大學資訊管理學系碩士論文，6月，2004

[ARC2003] M. Archer，E. Leonard and M Pradella，Modeling security-enhanced Linux policy specifications for analysis，DARPA Information Survivability Conference and Exposition， 2003. Proceedings ， Volume: 2，22-24 April 2003 Pages:164 – 169 vol.2

[ARC2003a] M. Archer，E. Leonard and M Pradella，Analyzing security-enhanced Linux policy specifications，Policies for Distributed Systems and Networks， 2003. Proceedings. POLICY 2003. IEEE 4th International Workshop on ， 4-6 June 2003 Pages:158 – 169

[GUT2005] J.D. Guttman， A.L. Herzog， and J.D. Ramsdell， SLAT: Information Flow Analysis in Security Enhanced Linux. Included in the SLAT distribution， available from http://www.nsa.gov/SELinux (2005)

[JEN1992] Kurt Jensen: Coloured Petri Nets. Basic Concepts， Analysis Methods and Practical Use， Vol. 1：Basic Concepts. In EATCS Monographs on Theoretical Computer Science， Spring-Verlag (1992) 1-234