Formal methods for security in the Xenon hypervisor

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 modelled the fundamental definition of security, the hypercall interface behaviour, and the internal modular design. We used three 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 modelling. Here, we report our experiences to date with using these formalisms for assurance.