Paper Info
Title
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor.
Abstract
Virtualization engines play a critical role in many modern software products. In an effort to gain definitive confidence on critical components, our company has invested on the formal verification of the NOVA micro hypervisor, following recent advances in similar academic and industrial operating-system verification projects. There are inherent difficulties in applying formal methods to low-level implementations, and even more under specific constraints arising in commercial software development. In order to deal with these, the chosen approach consists in the splitting of the verification effort by combining the definition of an abstract model of NOVA, the verification of fundamental security properties over this model, and testing the conformance of the model w.r.t. the NOVA implementation. This article reports on our experiences in applying formal methods to verify a hypervisor for commercial purposes. It describes the verification approach, and the security properties under consideration, and reports the results obtained.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_5
Lecture Notes in Computer Science
Field
DocType
Volume
Virtualization,Computer science,Hypervisor,Implementation,Theoretical computer science,Commercial software,Model-based testing,Software,Formal methods,Formal verification
Conference
9995
ISSN
Citations 
PageRank 
0302-9743
2
0.47
References 
Authors
16
10
Name
Order
Citations
PageRank
Hanno Becker142.20
Juan Manuel Crespo21647.25
Jacek Galowicz320.81
Ulrich Hensel48910.50
Yoichi Hirai541.53
César Kunz616710.81
Keiko Nakata721.49
Jorge Luis Sacchini8203.24
Hendrik Tews916116.10
Thomas Tuerk10673.50