ePrints

Formal methods for security in the Xenon hypervisor

Lookup NU author(s): Dr Leo Freitas

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

Abstract

This paper reports on the Xenon project’s use of formal methods. Xenon is a higher-assurance secure hypervi- sor based on re-engineering the Xen open-source hypervisor. The Xenon project used formal specifications both for assur- ance and as guides for security re-engineering. We formally modelled the fundamental definition of security, the hyper- call 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 seman- tics given in Hoare and He’s unifying theories of program- ming. Circus is suited for both event-based and state-based modelling. Here, we report our experiences to date with using these formalisms for assurance.

Publication metadata

Author(s): Freitas L, McDermott J

Publication type: Article

Publication status: Published

Journal: International Journal on Software Tools Technology Transfer

Year: 2011

Volume: 13

Issue: 5

Pages: 463-489

Print publication date: 01/10/2011

ISSN (print): 1433-2779

ISSN (electronic): 1433-2787

Publisher: Springer

URL: http://dx.doi.org/10.1007/s10009-011-0195-9

DOI: 10.1007/s10009-011-0195-9

Altmetrics

Share