隨著資訊時代的來臨，網際網路快速的發展，使得資訊安全日漸重要，其中在Unix Like 中，Linux 更是日漸受到重視，然而，Linux 本身存在著某些先天上的不足，例如僅能以uid、gid、other 等來控制存取權限，無法達到RBAC(Role Based Access Control)的功能。有鑑於此，許多加強原有Linux安全機制之軟體因而產生，如SELinux (Security- Enhanced Linux) 、 LIDS(Linux Intrusion Detection System)等，其中又以美國NSA所發展之SELinux更為受到注目。然而，SELinux 的安全政策(security policy)設定相當複雜，因此所衍生出許多相關研究，本論文主旨即在探討由使用者自行制定的規則是否符合安全目標。論文中將介紹此方法的流程，以正規理論基礎Color-Petri Net(CPN)方法，並使用CPN工具來驗證是否符合安全目標。

[1] Archer, M.; Leonard, E.; Pradella, M., “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
[2] Archer, M.; Leonard, E.; Pradella, M.,”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
[3] Beata Sarna-Starosta,”Policy Analysis for Security-Enhanced Linux”, 2004 Feberuary
[4] Hitachi software’s selinux site http://www.selinux.hitachi-sk.co.jp/index.html
[5] Joshua D. Guttman, Amy L. Herzog, and John D. Ramsdell. SLAT: Information flow in Security Enhanced Linux, 2003. Included in the SLAT distribution, available from http://www.nsa.gov/SELinux.
[6] LIDS, http://www.lids.org/
[7] NSA selinux, http://www.nsa.gov/selinux/
[8] Trent Jaeger Reiner Sailer Xiaolan Zhang, IBM T. J. Watson Research Center Hawthorne, NY 10532 USA, Analyzing Integrity Protection in the SELinux Example Policy
[9] Tresys Technology ,http://www.tresys.com/
[10]R. Spencer, S. Smalley, P. Loscocco, M. Hibler, D. Andersen, and J. Lepreau. The Flask　security architecture: System support for diverse security policies. In Proc. of the Eighth　USENIX Security Symposium, pages 123~139, Aug. 1999.
[11]Policy Analysis for Security-Enhanced Linux_Beata Sarna-Starosta Scott D. Stoller, Feb.2004.
[12]XSB. Available at http://xsb.sourceforge.net/.
[13]MYSEA technology demonstration, Irvine, C.; Shifflett, D.; Clark, P.; Levin, T.; Dinolt, G. Page(s): 10- 12 vol.2
[14]A Software Architecture to support Misuse Intrusion Detection.;Sandeep Kumar,Eugene H. Spafford.
[15] Simulation Report Reuse and High Level Languages; CS599, Fall 1999 Kam Wing Lo
[16] A Software Development Cost Estimation Model for Higher Level Language
Environments; Jeanette N. Morgan Peeples
[17] Kurt Jensen, “Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol 1：Basic Concepts,” Monographs in Theoretical Computer Science, Spring-Verlag, 1992.
[18]Peter A. Loscocco and Stephen D. Smalley. Meeting critical security objectives withSecurity-Enhanced Linux. In Proceedings of the 2001 Ottawa Linux Symposium, 2001.Available from http://www.nsa.gov/SELinux/docs.html.
[19]Peter Loscocco and Stephen Smalley. Integrating flexible support for security policiesinto the Linux operating system. In Proc. FREENIX Track of the 2001 USENIX AnnualTechnical Conference, 2001. Available from http://www.nsa.gov/SELinux/docs.html.
[20]Stephen Smalley and Timothy Fraser. A security policy configuration for the Security-Enhanced Linux, 2001. Available from http://www.nsa.gov/SELinux/docs.html
[21]Stephen Smalley. Configuring the SELinux policy, 2003. Available from
http://www.nsa.gov/SELinux/docs.html
[22]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.
[23] Joshua D. Guttman, Amy L. Herzog, and John D. Ramsdell. Information flow in
operating systems: Eager formal methods. In Proc. 2003 Workshop on Issues in the
Theory of Security (WITS), 2003.
[24] Joshua D. Guttman, Amy L. Herzog, and John D. Ramsdell. SLAT: Information flow in Security Enhanced Linux, 2003. Included in the SLAT distribution, available from http://www.nsa.gov/SELinux.
[25] Beata Sarna-Starosta and C. R. Ramakrishnan. Constraint-based model checking ofdata-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.
[26] Lawrence Snyder. On the synthesis and analysis of protection systems. In Proc. SixthACM Symposium on Operating Systems Principles (SOSP), pages 141–150. ACM Press,1977.
[27] P. Loscocco. Private communication. NRL, Nov. 2001.
[28] Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies; Myla Archer Elizabeth Leonard
[29] P. Loscocco and S. Smalley. Integrating exible support for security policies into the Linux operating system. Technical report, National Security Agency, Jan. 2, 2001.
[30] S. Smalley and T. Fraser. A security policy con_guration for Security-Enhanced Linux.Technical report, National Security Agency, Jan. 2, 2001.