Developer Summit 2009/Abstracts/Jaeger Virt
Anslysis of Flask Policies in VM Systems
With the introduction of the Xen Security Modules with support for Flask MAC policies, we are presented with the opportunity to enforce mandatory policies comprehensively over all virtual machines. A question is whether the combination of SELinux policies in the VMs and the XSM/Flask policy in the VMM ensure comprehensive enforcement of a consistent view of security. At Penn State University, we are developing a policy analysis tool for VM systems that infers a system security goal from the relationships among VMs and determines whether the Flask and SELinux policies comply with that goal. In this talk, we will present the design of this analysis and demonstrate how to use the tool to identify and resolve policy specifications that conflict with the security goal. The key feature of the tool design is that we consider interactions between VMs without considering the internal VM policies. Only if we cannot prove that all inter-VM accesses are safe do we examine that VM's SELinux policy. We can show a demonstration of the system on real XSM/Flask and SELinux VM policies.