A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C

Blanchard Allan 1, * Nikolai Kosmatov 1 Matthieu Lemerre 1 Frédéric Loulergue 2, 3, 4
* Auteur correspondant
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
4 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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 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.
Type de document :
Communication dans un congrès
International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Jun 2015, Oslo, Norway. Springer, 2015, 〈http://fmics2015.org〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01140271
Contributeur : Frédéric Loulergue <>
Soumis le : mercredi 8 avril 2015 - 11:26:10
Dernière modification le : mardi 17 avril 2018 - 11:24:12

Identifiants

  • HAL Id : hal-01140271, version 1

Citation

Blanchard Allan, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue. A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C. International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Jun 2015, Oslo, Norway. Springer, 2015, 〈http://fmics2015.org〉. 〈hal-01140271〉

Partager

Métriques

Consultations de la notice

323