Xenon Formal Security Policy Model
John McDermott, James Kirby, Myong H. Kang, Bruce Montrose · 2007
Xenon is a high-assurance virtual machine monitor based on the Xen open-source hypervisor. We model the Xenon high-assurance virtual machine monitor's security policy as a conditional non-interference policy, using an event-based paradigm and the Communicating Sequential Processes (CSP) formalism. Our single model formally describes not only the separation of information flow but also the sharing. We also present our strategy for showing correspondence between this model and the Xenon interface.