Analysis of virtual machine system policies

ABSTRACT

The recent emergence of mandatory access (MAC) enforcement for virtual machine monitors (VMMs) presents an opportunity to enforce a security goal over all its virtual machines (VMs). However, these VMs also have MAC enforcement, so to determine whether the overall system (VM-system) is secure requires an evaluation of whether this combination of MAC policies, as a whole, complies with a given security goal. Previous MAC policy analyses either consider a single policy at a time or do not represent the interaction between different policy layers (VMM and VM). We observe that we can analyze the VMM policy and the labels used for communications between VMs to create an inter-VM flow graph that we use to identify safe, unsafe, and ambiguous VM interactions. A VM with only safe interactions is compliant with the goal, a VM with any unsafe interaction violates the goal. For a VM with ambiguous interactions we analyze its local MAC policy to determine whether it is compliant or not with the goal. We used this observation to develop an analytical model of a VM-system, and evaluate if it is compliant with a security goal. We implemented the model and an evaluation tool in Prolog. We evaluate our implementation by checking whether a VM-system running XSM/Flask policy at the VMM layer and SELinux policies at the VM layer satisfies a given integrity goal. This work is the first step toward developing layered, multi-policy analyses.

REFERENCES

• 1: Stefan Berger , Ramón Cáceres , Kenneth A. Goldman , Ronald Perez , Reiner Sailer , Leendert van Doorn, vTPM: virtualizing the trusted platform module, Proceedings of the 15th conference on USENIX Security Symposium, July 31-August 04, 2006, Vancouver, B.C., Canada
• 2: E. Bertino , B. Catania , E. Ferrari , P. Perlasca, A System to Specify and Manage Multipolicy Access Control Models, Proceedings of the 3rd International Workshop on Policies for Distributed Systems and Networks (POLICY'02), p.116, June 05-07, 2002
• 3: K. J. Biba. Integrity Considerations for Secure Computer Systems. Technical Report MTR-3153, MITRE, April 1977.
• 4: W. E. Boebert and R. Y. Kain. A Practical Alternative to Hierarchical Integrity Policies. In Proceedings of the 8th National Computer Security Conference, 1985.
• 5: G. Coker. Xen Security Modules (XSM). http://www.xen.org/files/xensummit_4/xsm-summit-041707_Coker.pdf. Computer Science Department of the Stony Brook University. XSB: Logic Programming and Deductive Database system for Unix and Windows.
• 6: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 7: R. P. Goldberg, Architecture of virtual machines, Proceedings of the June 4-8, 1973, national computer conference and exposition, June 04-08, 1973, New York, New York [doi>10.1145/1499586.1499669]
• 8: Joshua D. Guttman , Amy L. Herzog , John D. Ramsdell , Clement W. Skorupka, Verifying information flow goals in security-enhanced Linux, Journal of Computer Security, v.13 n.1, p.115-134, January 2005
• 9: Boniface Hicks , Sandra Rueda , Luke St.Clair , Trent Jaeger , Patrick McDaniel, A logical specification and analysis for SELinux MLS policy, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France [doi>10.1145/1266840.1266854]
• 10: T. Jaeger, K. Butler, D. H. King, S. Hallyn, J. Latten, and X. Zhang. Leveraging IPsec for Mandatory Access Control Across Systems. In Proceedings of the Second International Conference on Security and Privacy in Communication Networks, Aug. 2006.
• 11: Sushil Jajodia , Pierangela Samarati , V. S. Subrahmanian , Eliza Bertino, A unified framework for enforcing multiple access control policies, Proceedings of the 1997 ACM SIGMOD international conference on Management of data, p.474-485, May 11-15, 1997, Tucson, Arizona, United States
• 12: Samuel T. King , George W. Dunlap , Peter M. Chen, Operating system support for virtual machines, Proceedings of the annual conference on USENIX Annual Technical Conference, p.6-6, June 09-14, 2003, San Antonio, Texas
• 13: M. Koch , L. V. Mancini , F. Parisi-Presicce, On the specification and evolution of access control policies, Proceedings of the sixth ACM symposium on Access control models and technologies, p.121-130, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373280]
• 14: Derek Gordon Murray , Grzegorz Milos , Steven Hand, Improving Xen security through disaggregation, Proceedings of the fourth ACM SIGPLAN/SIGOPS international conference on Virtual execution environments, March 05-07, 2008, Seattle, WA, USA [doi>10.1145/1346256.1346278]
• 15: NetLabel - Explicit labeled networking for Linux. http://www.nsa.gov/selinux.
• 16: Security-enhanced Linux. http://www.nsa.gov/selinux.
• 17: Gerald J. Popek , Robert P. Goldberg, Formal requirements for virtualizable third generation architectures, Communications of the ACM, v.17 n.7, p.412-421, July 1974 [doi>10.1145/361011.361073]
• 18: Sandra Rueda , Dave King , Trent Jaeger, Verifying compliance of trusted programs, Proceedings of the 17th conference on Security symposium, p.321-334, July 28-August 01, 2008, San Jose, CA
• 19: Reiner Sailer , Trent Jaeger , Enriquillo Valdez , Ramon Caceres , Ronald Perez , Stefan Berger , John Linwood Griffin , Leendert van Doorn, Building a MAC-Based Security Architecture for the Xen Open-Source Hypervisor, Proceedings of the 21st Annual Computer Security Applications Conference, p.276-285, December 05-09, 2005 [doi>10.1109/CSAC.2005.13]
• 20: B. Sarna-Starosta and S. Stoller. Policy Analysis for Security-Enhanced Linux. In Proceedings of the 2004 Workshop on Issues in the Theory of Security (WITS), pages 1--12, April 2004.
• 21: U. Shankar, T. Jaeger, and R. Sailer. Toward Automated Information-Flow Integrity Verification for Security-Critical Applications. In Proceedings of the 2006 ISOC Networked and Distributed Systems Security Symposium, February 2006.
• 22: S. Smalley, C. Vance, and W. Salamon. Implementing SELinux as a Linux Security Module. Technical Report 01-043, NAI Labs, 2001.
• 23: Ray Spencer , Stephen Smalley , Peter Loscocco , Mike Hibler , David Andersen , Jay Lepreau, The flask security architecture: system support for diverse security policies, Proceedings of the 8th conference on USENIX Security Symposium, p.11-11, August 23-26, 1999, Washington, D.C.
• 24: Sun Microsystems. Trusted solaris operating environment - a technical overview. http://www.sun.com.
• 25: Tresys. Policy management server. Tresys. SETools - Policy Analysis Tools for SELinux. Available at http://oss.tresys.com/projects/setools.
• 26: C. Vance, T. Miller, and R. Dekelbaum. Security-Enhanced Darwin: Porting SELinux to Mac OS X. In Proceedings of the Third Annual Security Enhanced Linux Symposium, Baltimore, MD, USA, March 2007.
• 27: H. Vijayakumar, S. Rueda, and T. Jaeger. Semantics of XSM/Flask Policies. Technical Report NAS-TR-0108-2009, SIIS Lab. Pennsylvania State University., 2009.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection

General Terms:
Security

Keywords:
policy analysis, selinux, virtual machines, xen security modules (xsm)