SpecCert: Specifying and Verifying Hardware-based Security 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.
Liste complète des métadonnées

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01356690
Contributor : Thomas Letan <>
Submitted on : Monday, September 5, 2016 - 4:34:36 PM
Last modification on : Thursday, February 7, 2019 - 3:25:49 PM
Document(s) archivé(s) le : Tuesday, December 6, 2016 - 2:04:50 PM

File

speccert-fm2016.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01356690, version 1

Citation

Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin. SpecCert: Specifying and Verifying Hardware-based Security Enforcement. [Technical Report] CentraleSupélec; Agence Nationale de Sécurité des Systèmes d’Information. 2016, pp.20. ⟨hal-01356690⟩

Share

Metrics

Record views

1689

Files downloads

396