SpecCert: Specifying and Verifying Hardware-based Software Enforcement

Abstract : Over time, hardware designs have constantly grown in complexity and modern platforms involve multiple interconnected hardware components. During the last decade, several vulnerability disclosures have proven that trust in hardware can be misplaced. In this article, we give a formal definition of Hardware-based Security Enforcement (HSE) mechanisms, a class of security enforcement mechanisms such that a software component relies on the underlying hardware platform to enforce a security policy. We then model a subset of a x86-based hardware platform specifications and we prove the soundness of a realistic HSE mechanism within this model using Coq, a proof assistant system.
Type de document :
Communication dans un congrès
21st International Symposium on Formal Methods (FM 2016), Nov 2016, Limassol, Cyprus. Springer, 21st International Symposium on Formal Methods (FM 2016). 〈http://fm2016.cs.ucy.ac.cy/〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01361422
Contributeur : Thomas Letan <>
Soumis le : vendredi 25 mai 2018 - 10:09:43
Dernière modification le : vendredi 25 mai 2018 - 12:33:04
Document(s) archivé(s) le : dimanche 26 août 2018 - 13:04:20

Fichier

speccert-fm2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01361422, version 1

Citation

Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin. SpecCert: Specifying and Verifying Hardware-based Software Enforcement. 21st International Symposium on Formal Methods (FM 2016), Nov 2016, Limassol, Cyprus. Springer, 21st International Symposium on Formal Methods (FM 2016). 〈http://fm2016.cs.ucy.ac.cy/〉. 〈hal-01361422〉

Partager

Métriques

Consultations de la notice

1250

Téléchargements de fichiers

31