Giorgio Zanin
ABSTRACT
This paper presents a formal model, called SELAC, for analyzing an arbitrary security policy configuration for the SELinux system. A security policy for SELinux is complex and large: it is made by many configuration rules that refer to the access control sub-models implemented in the system. Among the rules composing a security policy configuration, many relationships occur and it is extremely difficult to understand their overall effects in the system. Our aim is to define semantics for the constructs of the SELinux configuration language and to model the relationships occurring among sets of configuration rules. Finally, we develop an algorithm based upon SELAC, which can verify whether, given an arbitrary security policy configuration, a given subject can access a given object in a given mode.
- Anderson, J.P. 1972. Computer Security Technology Planning Study. ESD-TR-73-51, Vol 1, Hanscom AFB, Mass.Google Scholar
- Boebert, W. E. and Kain, R. Y. 1985. A practical alternative to hierarchical integrity policies. In Proceedings of the 8th National Computer Security Conference (Gaithersburg, Md.).Google Scholar
- Badger, L., Sterne, D. F., Sherman, D. L., Walker, K. M. and Haghighat, S. A. 1995. Practical Domain and Type Enforcement for Unix. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, Calif, May). Google ScholarDigital Library
- Badger, L., Sterne, D. F., Sherman, D. L., Walker, K. M. and Haghighat, S. A. 1995. A Domain and Type Enforcement Unix Prototype. In Proceedings of the 5th USENIX UNIX Security Symposium (Salt Lake City, Utah, June). Google ScholarDigital Library
- Ferraiolo, D. and Kuhn, R. 1992. Role-based access controls. In 15th NIST-NCSC National Computer Security Conference, Baltimore, MD, Oct 13-16, pp 554--563.Google Scholar
- Jaeger, T., Sailer, R., and Zhang, X. 2003. Analyzing Integrity Protection in the SELinux Example Policy. In Proceedings of the 12th Usenix Security Symposium (Washington, August). Google ScholarDigital Library
- Jaeger, T., Zhang, X. and Edwards, A. 2003. Policy management using access control spaces. In ACM Transactions on Information and System Security (TISSEC), Volume 6, Issue 3 (August), pp. 327--364. Google ScholarDigital Library
- Kuhn, D. R. 1997. Mutual exclusion of roles as a means of implementing separation of duty in role-based access control systems. In Proceedings of the 2 nd ACM Role-Based Access Control Workshop. Fairfax, Virginia (USA), November 06-07, 1997, p. 23--30. Google ScholarDigital Library
- Loscocco, P. A. and Smalley, S. D. 2001. Integrating flexible support for security policies into the Linux operating system. NSA Technical Report, Feb. Google ScholarDigital Library
- Loscocco, P. A. and Smalley, S. D. 2001. Meeting critical security objectives with Security-Enhanced Linux. In Proceedings of the 2001 Ottawa Linux Symposium, JulyGoogle Scholar
- Nyanchama, M. and Osborn, S. 1999. The role graph model and conflict of interest. ACM Trans Inf. Syst. Sec. 2, 1 (Feb.). Google ScholarDigital Library
- O'Brien, R. and Rogers, C. 1991. Developing Applications on LOCK. In Proceedings of the 14 th National Computer Security Conference, Washinghton DC, Oct., pp 147--156.Google Scholar
- Sandhu, R. 1998. Role-Based Access Control. Advances in Computer Science, vol 46, Academic Press.Google Scholar
- National Security Agency. Security-Enhanced Linux (SELinux). http://www.nsa.gov/selinux.Google Scholar
- Smalley, S. D. 2002. Configuring the SELinux Policy. Nai Labs Report #02-007, June.Google Scholar
- Spencer, R., Smalley, S. D., Loscocco, P., Hibler, M., Andersen, D. and Lepreau, J. 1999. The Flask Security Architecture: System support for diverse security policies. In Proceedings of the 8th USENIX Security Symposium, Aug, pp 123--139. Google ScholarDigital Library
- Simon, R. and Zurko, M. E. 1997. Mutual exclusion of roles as a means of implementing separation of duty in role-based access control systems. In Proceedings of the10th IEEE Computer Security Foundations Workshop (June). Rockport, Massachusetts. Google ScholarDigital Library
- http://www.nsa.gov/selinux/list-archive/0302/3864.cfmGoogle Scholar
- http://www.tresys.com/selinux/selinux_policy_tools.htmlGoogle Scholar
- http://www.nsa.gov/selinux/list-archive/0312/6084.cfmGoogle Scholar
Index Terms
- Towards a formal model for security policies specification and validation in the selinux system
Recommendations
A logical specification and analysis for SELinux MLS policy
The SELinux mandatory access control (MAC) policy has recently added a multilevel security (MLS) model which is able to express a fine granularity of control over a subject's access rights. The problem is that the richness of the SELinux MLS model makes ...
Formal specification and management of security policies with collective group obligations
Obligations are an essential element of security policies since they enable the specification of many security requirements such as availability, privacy, usage control and data protection. In everyday life, the fulfillment of obligations is often the ...
Formal specification and validation of security policies
FPS'11: Proceedings of the 4th Canada-France MITACS conference on Foundations and Practice of SecurityWe propose a formal framework for the specification and validation of security policies. To model a secured system, the evolution of security information in the system is described by transitions triggered by authorization requests and the policy is ...
Comments