lthms.xyz/research.org -rw-r--r-- 2.9 KiB View raw
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
---
title: "lthms’ Research"
category: research

bg_color: "#f9f8f4"
font_color: "#0a0a0a"
primary_color: "#437087;"
code_bg_color: "#deeaef"
feature_img: "/img/freespec_feature.jpg"
credit: "A blueprint from <a
href=\"https://www.flickr.com/photos/internetarchivebookimages/14780705985/in/photolist-ou6hS9-ou6E73-oxTmga-ovR82t-oeCyCt-ovVgb9-ou5R5Y-oeC1zR-ow65cU-ovV4fA-ovV7ZQ-oeCh8d-oeCFuq-oeCkUG-ovUKEq-oeDeb9-oeCr2s-ow8H8M-ou6ShW-oeCHkZ-ovQS4H-oeD2TF-ow7YWn-ou6nnG-oxTGdV\">a
book from 1910</a>, Public Domain"
---

I am a formal methods researcher with a focus on proving the correctness of
complex systems with respect to realistic security policies.

* Publications

** PhD. Thesis

- Specifying and Verifying Hardware-based Security Enforcement Mechanisms ::
  Supervised by [[https://guillaume.hiet.fr][Guillaume Hiet]] and [[https://github.com/chifflier][Pierre Chifflier]], directed by [[http://www.rennes.supelec.fr/ren/perso/lme/home_page_v3.2/english.html][Ludovic
     Mé]]. Defended in October 2018. [[https://hal.inria.fr/tel-01989940/document][<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.

** Peer-reviewed Conferences

- Modular Verification of Program with Effects and Effect Handlers in Coq ::
  /22nd International Symposium on Formal Methods/ (FM 2018), with [[http://yann.regis-gianas.org/][Yann
     Régis-Gianas]], [[https://github.com/chifflier][Pierre Chifflier]] and [[https://guillaume.hiet.fr][Guillaume Hiet]].  [[https://hal.inria.fr/hal-01799712/document][<PDF>]]
- SpecCert: Specifying and Verifying Hardware-based Security Enforcement Mechanisms ::
  /21st International Symposium on Formal Methods/ (FM 2016), with [[https://github.com/chifflier][Pierre
     Chifflier]], [[https://guillaume.hiet.fr][Guillaume Hiet]] and [[https://pneron.github.io/][Pierre Néron]]. [[https://hal.inria.fr/hal-01361422/document][<PDF>]]