Deductive Verification of a Hypervisor Model

Vlad Rusu 1 Gilles Grimaud 2 Michaël Hauspie 2 François Serman 2
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : We propose a deductive-verification approach for proving partial-correctness and invariance properties on arbitrary transition systems, and demonstrate it on a security hypervisor model for machine code. Regarding partial correctness, we generalise the recently-introduced formalism of Reachability Logic, currently used as a language-parametric program logic, to arbitrary transition systems. We propose a sound and relatively-complete proof system for the resulting logic. The soundness of the proof system is formally established in the Coq proof assistant, and the mechanised proof provides us with a generic Reachability-Logic prover within Coq for transition-system specifications. The relative completeness of the proof system, although theoretical in nature, also has a practical value, as it induces a proof strategy that is guaranteed to prove all valid formulas on a given transition system. The strategy reduces partial-correctness verification to invariant verification; for the latter we propose an incremental technique in order to deal with the case-explosion problem. All these various techniques were instrumental in enabling us to deal with a nontrivial case study: proving that a Coq model of a security hypervisor meets its expected requirements, expressed as invariants and partial-correctness properties, within reasonable time and effort limits. We also report on some experiments with a C+ARM assembly implementation of our hypervisor in order to confirm the fact that it introduces a limited amount of execution-time overhead to operating-system calls.
Type de document :
Pré-publication, Document de travail
(27 pages). 2017
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger
Contributeur : Pal Dream <>
Soumis le : mardi 17 octobre 2017 - 12:27:13
Dernière modification le : mardi 3 juillet 2018 - 11:23:40
Document(s) archivé(s) le : jeudi 18 janvier 2018 - 13:58:48


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01614509, version 2


Vlad Rusu, Gilles Grimaud, Michaël Hauspie, François Serman. Deductive Verification of a Hypervisor Model. (27 pages). 2017. 〈hal-01614509v2〉



Consultations de la notice


Téléchargements de fichiers