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

以作者查詢圖書館館藏

、以作者查詢臺灣博碩士

、以作者查詢全國書目

、勘誤回報

、線上人數：43

、訪客IP：18.116.40.177

姓名

高永威(Yung-Wei Kao) 查詢紙本館藏

畢業系所

資訊管理學系

論文名稱

以彩色派翠網對 Security-Enhanced Linux 安全政策資訊流進行驗證之研究
(Information Flow Query and Verification for Security Policy of Security-Enhanced Linux Using CPN)

相關論文

★ 應用數位版權管理機制於數位影音光碟內容保護之研究	★ 以應用程式虛擬化技術達成企業軟體版權管理之研究
★ 以IAX2為基礎之網頁電話架構設計	★ 應用機器學習技術協助警察偵辦詐騙案件之研究
★ 擴充防止詐欺及保護隱私功能之帳戶式票務系統研究-以大眾運輸為例	★ 網際網路半結構化資料之蒐集與整合研究
★ 電子商務環境下網路購物幫手之研究	★ 網路安全縱深防護機制之研究
★ 國家寬頻實驗網路上資源預先保留與資源衝突之研究	★ 以樹狀關聯式架構偵測電子郵件病毒之研究
★ 考量地區差異性之隨選視訊系統影片配置研究	★ 不信任區域網路中數位證據保留之研究
★ 入侵偵測系統事件說明暨自動增加偵測規則之整合性輔助系統研發	★ 利用程序追蹤方法關聯分散式入侵偵測系統之入侵警示研究
★ 一種網頁資訊擷取程式之自動化產生技術研發	★ 應用XML/XACML於工作流程管理系統之授權管制研究

檔案

[Endnote RIS 格式]

[Bibtex 格式]

[相關文章]

[文章引用]

[完整記錄]

[館藏目錄]

[檢視]

[下載]

本電子論文使用權限為同意立即開放。
已達開放權限電子全文僅授權使用者為學術研究之目的，進行個人非營利性質之檢索、閱讀、列印。
請遵守中華民國著作權法之相關規定，切勿任意重製、散佈、改作、轉貼、播送，以免觸法。

摘要(中)

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

關鍵字(中)

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

關鍵字(英)

★ security policy
★ information flow
★ SELinux
★ Colored Petri Nets

論文目次

摘要 ……………………………………………………………………………….... I
Abstract ………………………………………………………………………….. II
目錄 …………………………………………………………………………….. III
圖目錄 …………………………………………………………………………… V
表目錄 ……………………………………………………………………….… VII
第一章緒論………………………………………………………………………. 1
1.1 研究動機與背景 ………………………………………………..………... 1
1.2 問題陳述 ……………………………………………………………..…... 3
1.3 研究目的 ……………………………………………………………..…... 4
1.4 研究貢獻 ……………………………………………………………..…... 5
1.5 論文架構 …………………………………………………………..……... 7
第二章相關研究 ………………………………………………………………. 8
2.1 SELinux 安全模型 ……………………………………………………... 8
2.1.1 SELinux MAC 運作機制 …………………………………………... 8
2.1.2 安全上下文 ……………………………………………………... 9
2.2 SELinux 安全政策分析工具文獻 ……………………………………... 10
2.2.1 GOKYO …………………………………………………………... 11
2.2.2 SLAT …………………………………………………………... 12
2.2.3 PAL …………………………………………………………... 13
2.2.4一種以彩色派翠網為基礎的 SELinux 安全政策分析工具 …. 14
2.3 相關研究小結 …………………………………………………..……... 15
第三章系統模型 ……………………………………………………………… 17
3.1 CPN 定義 ………………………………………………………………. 17
3.2 安全政策定義 …………………………………………………………... 19
3.3資訊流定義 ……………………………………………………….…... 20
3.4 安全目標 ……………………………………………………..……... 22
3.5 安全查詢 …...……………………………………………………….…... 24
3.6 本章小結 …...……………………………………………………….…... 26
第四章系統運作與架構設計 ……………………………………………… 27
4.1 如何使用本系統 ………………………………………………………. 27
4.2 系統運作流程 …………………………………………………………... 27
4.3 系統架構設計 …………………………………………………………... 29
第五章 CPN 圖形轉換 ……………………………………………………… 31
5.1 Policy CPN Diagram 轉換 …………………………………………… 32
5.2 Query CPN Diagram 轉換 …………………………………………… 34
5.3 圖形合併 ……………………………………………..…………………. 36
5.4 本張小結 ……………………………………………..…………………. 37
第六章 SELinux 安全政策資訊流驗證範例 …………………………… 38
6.1 網路伺服器相關設定範例 ………………………………………………38
6.2 旁波段網路實作範例 ……………………………………………………40
第七章相關工具比較 ……………………………………………………… 47
第八章結論 …………………………………………………………………… 49
參考文獻 ………………………………………………………………………… 51

參考文獻

中文參考文獻
[黃嘉欣 2004] 黃嘉欣，一種以彩色派翠網為基礎的 SELinux 安全政策分析工具，國立中央大學資訊管理學系碩士論文，6月，2004
[陳奕明 2006] 陳奕明，孫文駿，可對抗大規模攻擊的安全管控平台，SAICT 2006 (2006)
英文參考文獻
[ARC2002] M. Archer，E. Leonard and M Pradella， Towards a Methodology and tool for the Analysis of Security-Enhanced Linux Security Policies. NRL Memorandum Report NRL/MR/5540-02-8629 (2002)
[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
[FOR1968] Forrester, J.W.，Principles of systems，MIT Press， Cambridge，Massachusetts (1968)
[GUT2003] J.D. Guttman， A.L. Herzog， and J.D. Ramsdell， Information Flow in Operating Systems: Eager Formal Methods. Workshop on Issues in the Theory of Security (WITS'03) (2003)
[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)
[GUT2006] Gery Gutnik and Gal A. Kaminka， Representing Conversations for Scalable Overhearing. JAIR Volume 25 (2006) 349-387
[IRV2003] Cynthia Irvine， David Shifflett， Paul Clark， Timothy Levin， George Dinolt ，MYSEA technology demonstration，Page(s): 10- 12 vol.2 (2003)
[JAE2003] T. Jaeger， R. Sailer， and X. Zhang， Policy Management Using Access Control Spaces. ACM Transactions on Information and System Security (TISSEC)
[JAE2003a] T. Jaeger， R. Sailer， and X. Zhang， Analyzing integrity protection in the SELinux example policy. In Proc. USENIX Security Symposium (2003) 59-74
[JAE2004] T. Jaeger， R. Sailer， and X. Zhang， Resolving Constraint Conflicts， Proceedings of the 2004 ACM Symposium on Access Control Models and Technologies. (2004)
[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
[LOS1998] Peter A. Loscocco， Stephen D. Smalley， Patrick A. Muckelbauer， Ruth C. Taylor， S. Jeff Turner， John F. Farrell.， The Inevitability of Failure: The Flawed Assumption of Security in Modern Computing Environments. Proceedings of the 21st National Information Systems Security Conference (1998) 303-314.
[LOS2001] P.A. Loscocco， and S.D. Smalley， Meeting critical security objectives with Security-Enhanced Linux. In proceedings of the 2001 Ottawa Linux Symposium (2001)
[LOS2001a] P.A. Loscocco， and S.D. Smalley， Integrating Flexible Support for Security Policies into the Linux Operating System. USENIX Annual Technical Conference (2001)
[MCC2004] Bill Mccarty， SELinux NSA’s Open Source Security Enhanced Linux. ISBN: 0-596-00716-7， 256 pages， published by O'Reilly，2004
[SAM2001] Stephen Smalley and Timothy Fraser，A security policy configuration for the Security-Enhanced Linux，2001。 Available from http://www.nsa.gov/SELinux/docs.html
[SAM2003] Stephen Smalley. Configuring the SELinux policy， 2003. Available from http://www.nsa.gov/SELinux/docs.html
[SAR2003] Beata Sarna-Starosta and C. R. Ramakrishnan. Constraint-based model checking of data-independent systems. In Proc. 5th International Conferene on Formal EngineeringMethods (ICFEM)， volume 2885 of Lecture Notes in Computer Science， pages 579–598.Springer-Verlag， 2003.
[SAR2004] B. Sarna-Starosta and S.D. Stoller， Policy Analysis for security-Enhanced Linux. Workshop on Issues in the Theory of Security (WITS) (2004)
[STU2003] Tony Stubblebine， Regular Expression Pocket Reference。ISBN: 0-596-00415-X， 112 pages， published by O'Reilly (2003)
[WAL1996] Kenneth M. Walker， Daniel F. Sterne， M. Lee Badger， Michael J. Petkac， David L. Sherman， and Karen A. Oostendorp. Confining root programs with domain and type enforcement (DTE). In Proc. 6th USENIX UNIX Security Symposium， 1996.
[ZAN2004] G. Zanin and L.V. Mancini， Towards a Formal Model for Security Policies Specification and Validation in the SELinux System. In the Proceeding of SACMAT’04， Yorktown Heights， New York， USA 136-145
相關網站
[Apol] apol_perm_mapping_ver18.txt，http://www.tresys.com/selinux/
selinux_policy_tools.shtml
[CERT] CERT/CC，http://www.cert.org/stats/cert_stats.html
[CPN] CPN Tools， http://wiki.daimi.au.dk/cpntools/cpntools.wiki
[Eth] Ethereal，http://ethereal.com/
[NSA] NSA SELinux， http://www.nsa.gov/selinux/
[TCSEC] TCSEC， http://www.radium.ncsc.mil/tpep/library/rainbow/
5200.28-STD.html
[USC] US-CERT，http://www.us-cert.gov/cas/bulletins/SB2005.html
[XSB] XSB，Available at http://xsb.sourceforge.net/

指導教授

陳奕明(Yi-Ming Chen)

審核日期

2006-7-15

推文