A case study on formal verification of the anaxagoros hypervisor paging system with frama-C

Allan Blanchard; N. Kosmatov; M. Lemerre; Frédéric Loulergue

A case study on formal verification of the anaxagoros hypervisor paging system with frama-C

Allan Blanchard ^{1, 2, *} N. Kosmatov ¹ M. Lemerre ¹ Frédéric Loulergue ^{3, 2}

* Corresponding author

1 DILS - Département Ingénierie Logiciels et Systèmes

2 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans

3 PI.R2 - Design, study and implementation of languages for proofs and programs

Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes

Abstract : Cloud hypervisors are critical software whose formal verification can increase our confidence in the reliability and security of the cloud. This work presents a case study on formal verification of the virtual memory system of the cloud hypervisor Anaxagoros, a microkernel designed for resource isolation and protection. The code under verification is specified and proven in the Frama-C software verification framework, mostly using automatic theorem proving. The remaining properties are interactively proven with the Coq proof assistant. We describe in detail selected aspects of the case study, including parallel execution and counting references to pages, and discuss some lessons learned, benefits and limitations of our approach.

Keywords : C (programming language) Artificial intelligence Formal methods Interactive proofs Specifications Software reliability Formal verification Frama-C Cloud hypervisor Verification Theorem proving Deductive verification Concurrency deductive verification interactive proof cloud hypervisor Frama-C specification concurrency

Document type :

Conference papers

Domain :

Computer Science [cs]

Complete list of metadatas

Cited literature [2 references] Display Hide Download

https://hal-cea.archives-ouvertes.fr/cea-01834977
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 11:53:58 AM
Last modification on : Thursday, February 7, 2019 - 4:50:45 PM
Long-term archiving on : Friday, October 12, 2018 - 9:35:24 PM

bkll_fmics_2015.pdf

Files produced by the author(s)

A case study on formal verification of the anaxagoros hypervisor paging system with frama-C

File

Identifiers

Collections

Citation

Export

Metrics

111

142

Contact

A case study on formal verification of the anaxagoros hypervisor paging system with frama-C

File

Identifiers

Collections

Citation

Export

Share

Metrics

111

142

Contact