SpecCert: Specifying and Verifying Hardware-based Software Enforcement - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

SpecCert: Specifying and Verifying Hardware-based Software Enforcement

Résumé

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

Dates et versions

hal-01361422 , version 1 (25-05-2018)

Identifiants

Citer

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. ⟨10.1007/978-3-319-48989-6_30⟩. ⟨hal-01361422⟩
310 Consultations
184 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More