A case study on formal verification of the anaxagoros hypervisor paging system with frama-C - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

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

Résumé

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.
Fichier principal
Vignette du fichier
bkll_fmics_2015.pdf (283.34 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

cea-01834977 , version 1 (11-07-2018)

Identifiants

Citer

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⟩
127 Consultations
723 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More