Using formal methods for security in the Xenon project

This paper reports on the Xenon project's use of formal methods. Xenon is a higher-assurance secure hypervisor based on re-engineering the Xen open-source hypervisor. The Xenon project used formal specifications both for assurance and as guides for security re-engineering. We formally modeled the fundamental definition of security, the hyper-call interface behavior, and the internal modular design. We used 3 formalisms: CSP, Z, and Circus for this work. Circus is a combination of Standard Z, CSP, with its semantics given in Hoare and He's unifying theories of programming. Circus is suited for both event-based and state-based modeling. In this extended abstract, we report our experiences with using these formalisms for assurance.