Skip to Main content Skip to Navigation
Conference papers

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

Allan Blanchard 1, 2, * N. Kosmatov 1 M. Lemerre 1 Frédéric Loulergue 3, 2 
* Corresponding author
3 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Léna Le Roy Connect in order to contact the contributor
Submitted on : Wednesday, July 11, 2018 - 11:53:58 AM
Last modification on : Tuesday, September 6, 2022 - 1:27:20 PM
Long-term archiving on: : Friday, October 12, 2018 - 9:35:24 PM


Files produced by the author(s)



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. FMICS 2015 - Formal Methods for Industrial Critical Systems, Jun 2015, Oslo, Norway. pp.15-30, ⟨10.1007/978-3-319-19458-5_2⟩. ⟨cea-01834977⟩



Record views


Files downloads