I am a formal methods researcher with a focus on proving the correctness of complex systems with respect to realistic security policies.
- Specifying and Verifying Hardware-based Security Enforcement Mechanisms
- Supervised by Guillaume Hiet and Pierre Chifflier, directed by Ludovic Mé. Defended in October 2018. <PDF>
In this thesis, we consider a class of security enforcement mechanismswe 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 operatingsystem which configures page tables to isolate userland applicationsimplements a HSE mechanism.
During the past decades, several vulnerability disclosures have defeated HSE mechanisms. We focus on vulnerabilities that are the result of errors at the specification level, rather than implementation errors. 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 mechanismscan be leveraged as a foundation for a systematic approach to verifyhardware 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.
- Modular Verification of Program with Effects and Effect Handlers in Coq
- 22nd International Symposium on Formal Methods (FM 2018), with Yann Régis-Gianas, Pierre Chifflier and Guillaume Hiet. <PDF>
- SpecCert: Specifying and Verifying Hardware-based Security Enforcement Mechanisms
- 21st International Symposium on Formal Methods (FM 2016), with Pierre Chifflier, Guillaume Hiet and Pierre Néron. <PDF>