Home page of Philippe Thierry¶
About myself…¶
- GPG public key:
- FCDD F6D7 27B4 4BCD 06FF 1A32 C89D 5712 DF94 5F6F
If you have question on the bellowing content, mail me on info [at] reseau-libre [dot] net
PhD thesis¶
Projects¶
The Wookey project¶
The USB bus has been a growing subject of research in recent years. More specifically, securing the USB stack (and hence the USB hosts and devices) started to draw interest from the academic community since major and massively exploitable flaws have been revealed with the BadUSB threat [1].
The work presented in this project takes place in the design initiatives that have emerged to thwart such attacks, targetting the USB device security. The security model is based on both hardware and software primitives designed to bring in-depth security.
Hardware security relies on an extractable token embedding a secure element. This token is meant to provide a pre-boot authentication feature as well as a secure storage area for the sensitive master keys of WooKey user data encryption.
Software security relies on a microkernel that enforces privilege separation, memory isolation, W⊕X principle, stack and heap anti-smashing techniques. The most sensitive parts are implemented with a safe language (SPARK/Ada).
The secure update mechanism over USB is based on the DFU (Device Firmware Update) protocol. It also uses the pre-boot user authentication feature to strengthen the security of the platform. Firmware integrity and authenticity are based on state of the art cryptography.
| [1] | BadUSB-On accessories that turn evil, Karsten Nohl and Jakob Lell, Black Hat USA, 2014 |
The EwoK secured micro-kernel¶
EwoK microkernel is a part of the Wookey project. It targets micro-controllers and embedded systems. It aims to bring an efficient hardening of embedded devices with a reduced impact on the device performances.
EwoK has been designed to host complex drivers in userspace. Unlike most of other microkernels, the goal is to support complex software stacks (ISO7816, etc.) as well as high performance (USB, SDIO, CRYP) drivers. This makes EwoK valuable for multiple use cases, including high speed and security targeted devices.
Security properties
EwoK supports the following properties:
- Strict memory partitioning
- Strict partitioning of physical resources (devices, etc.)
- Fixed permissions management, set at compile time and easily verifiable
- Kernel Random Number Generation support (based on TRNG HW on STM32)
- Stack smashing protection (SSP) in both kernel and userspace tasks
- Userspace Heap/Stack smashing protection
- Proved W^X memory mappings
- Strict temporal separation between declarative phase and execution phase
- Fully userspace and partitioned drivers execution (including ISR execution)
- Written in a safe language (Ada), with various proven components using SPARK
List of published papers¶
WooKey: Designing a Trusted and Efficient USB Device¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | ACSAC |
| Year | 2019 |
| Speakers |
|
Wookey: The USB battlefront warrior¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | Embedded recipes |
| Year | 2018 |
| Speakers |
|
Wookey: USB Devices strikes back¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | SSTIC |
| Year | 2018 |
First paper about the Wookey project (see project part), describing the general Wookey project architecture.
KVM: focus sur l’implémentation d’un hyperviseur dans Linux¶
| Paper infos | |
|---|---|
| Authors |
|
| Journal | GNU/Linux Magazine France HS 87 |
| Year | 2016 |
A framework for a secure embedded filtering connector for multi-criticality systronic systems¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | ETFA |
| Year | 2013 |
Thesis paper on military vehicle on-board secure and real-time gateway architecture.
Relaxing Mixed-Criticality Scheduling Strictness for Task Sets Scheduled with FP¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | ECRTS |
| Year | 2012 |
Thesis paper about mixed-criticality and criticality reduction state detection.
Toward the integration of GRSecurity in embedded Android operating system¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | ELCE |
| Year | 2011 |
First attempt to include high level of hardening on Android kernel, some months before SEAndroid was made public.
Real-time scheduling analysis for ARINC-based virtualized systems¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | MAPSP |
| Year | 2011 |
Thesis paper on highly constraints TDM+EDF based hierarchical scheduling.
Toward a predictable and secure data cache algorithm: a cross-layer approach¶
| Paper infos | |
|---|---|
| Authors |
|
| Conference | ISPS |
| Year | 2011 |
Thesis paper on the impact of the cache algorithms and the various way to include security constraints in the cache controller behavior.
List of published courses¶
Introduction to embedded system security¶
| Course infos | |
|---|---|
| Authors |
|
| Language | FR |
| Year | 2018-2019 |
| School | Telecom SudParis, Ecole Polytechnique Executive Education |
| License | none |
Embedded security course, including hardware design security constraints, from tempest problematics to firmware protection and secure boot in embedded systems.
Android: Architecture et évolution des fonctions de contrôle d’accès¶
| Course infos | |
|---|---|
| Authors |
|
| Language | FR |
| Year | 2016-2017 |
| School | Telecom SudParis, ESIEE |
| License | Creative Commons license (see the license description) |
Course on the historical design of Android and its impact on the overall OS security, how SEAndroid and TrustZone gave some new security improvements and how the residual security threats are still a problem.
This course is no more maintained since 2017.
Introducing the Linux kernel architecture¶
| Course infos | |
|---|---|
| Authors |
|
| Language | FR/EN |
| Year | 2010 |
| School | ECE Paris |
| License | Creative Commons license (see the license description) |
Course about how to understand the Linux kernel internals and how to write a device driver on a Linux 2.6.x or 3.x. This course is no more maintained since 2010.
Les outils gnu pour la production: formation initiale aux outils de production et études de cas réels¶
| Course infos | |
|---|---|
| Authors |
|
| Language | FR |
| Year | 2010 |
| School | none |
| Thanks |
|
| License | Creative Commons license (see the license description) |
This course is an introduction to the autoconf/autotools and Makefile production tools. This course is no more maintained since 2010.
List of published patents¶
Equipement de sécurité de cloisonnement entre des premier et second domaines, comportant un composant de contrôle¶
| patent infos | |
|---|---|
| Applicant | Thales Communications & Security |
| Iventors |
|
| publication | INPI FR 13 03075 |
| Year | 2013 |
Equipement de sécurité de cloisonnement entre des premier et second domaines, augmenté d’une fonctionnalité d’audit¶
| patent infos | |
|---|---|
| Applicant | Thales Communications & Security |
| Iventors |
|
| publication | INPI FR 13 03074 |
| Year | 2013 |
Appareil informatique comportant un environnement d’exécution et un compartiment réservé avec une redirection vers ledit compartiment de requêtes entre l’environnement d’exécution et un dispositif externe, et système informatique comportant un tel appareil informatique¶
| patent infos | |
|---|---|
| Applicant | Thales Communications & Security |
| Iventors | J.M Lacroix, P. Thierry, O. Cazade |
| publication | INPI FR 13 00146 |
| Year | 2013 |
For images copyright, please see footnote [2] and [3]
References
| [2] | The Debian Open Use Logo(s) are Copyright (c) 1999 Software in the Public Interest, Inc., and are released under the terms of the GNU Lesser General Public License, version 3 or any later version (https://www.gnu.org/licenses/lgpl-3.0.en.html) |
| [3] | The URL image is a Wikimedia image, licensed under the Creative Common license (https://creativecommons.org/licenses/by/3.0/deed.en) |