HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Specifying and Verifying Hardware-based Security Enforcement Mechanisms

Abstract : In this thesis, we consider a class of security enforcement mechanisms we called Hardware-based Security Enforcement (HSE). In such mechanisms, some trusted software components rely on the underlying hardware architecture to constrain the execution of untrusted software components with respect to targeted security policies. For instance, an operating system which configures page tables to isolate userland applications implements a HSE mechanism. For a HSE mechanism to correctly enforce a targeted security policy, it requires both hardware and trusted software components to play their parts. During the past decades, several vulnerability disclosures have defeated HSE mechanisms. We focus on the vulnerabilities that are the result of errors at the specification level, rather than implementation errors. In some critical vulnerabilities, the attacker makes a legitimate use of one hardware component to circumvent the HSE mechanism provided by another one. For instance, cache poisoning attacks leverage inconsistencies between cache and DRAM’s access control mechanisms. We call this class of attacks, where an attacker leverages inconsistencies in hardware specifications, compositional attacks. Our goal is to explore approaches to specify and verify HSE mechanisms using formal methods that would benefit both hardware designers and software developers. Firstly, a formal specification of HSE mechanisms can be leveraged as a foundation for a systematic approach to verify hardware specifications, in the hope of uncovering potential compositional attacks ahead of time. Secondly, it provides unambiguous specifications to software developers, in the form of a list of requirements.
Document type :
Complete list of metadata

Cited literature [146 references]  Display  Hide  Download

Contributor : Abes Star :  Contact
Submitted on : Wednesday, May 27, 2020 - 12:49:12 PM
Last modification on : Friday, July 10, 2020 - 4:07:37 PM


Files produced by the author(s)


  • HAL Id : tel-01989940, version 2


Thomas Letan. Specifying and Verifying Hardware-based Security Enforcement Mechanisms. Hardware Architecture [cs.AR]. CentraleSupélec, 2018. English. ⟨NNT : 2018CSUP0002⟩. ⟨tel-01989940v2⟩



Record views


Files downloads