< Retour au sommaire
Présentation d'un OS sécurisé basé sur un micro-kernel développé en C et Rust
Philippe Thierry le
Lieu: bât 862, Salles 24-25
Suivre en visio
Abstract
As part of the evolution of its security products, Ledger is working, in
preparation for new generations of products, on the implementation of an
industrial-grade secure OS for the co-processors surrounding the Secure
Element. Until now, the operating systems analyzed as part of a first state of
the art have never been able to correspond to all of the security,
maintainability, and portability requirements that Ledger seeks to achieve in
order to ensure high quality in its future products, when also including
simplicity and licensing constraints.
The requirements relating to both code quality and implementation methodologies
(fault resilience, detection of corruption in the execution chain, strict best
practices on the use of types and semantics) have made it possible to conclude
that there was no open-source OS (or one with an adequate commercial model for
us) carrying all of these properties. Failing that, it was decided to implement
such an operating system from scratch, and to make it an Open-Source system
under OSS license (TBD : Apache 2.0?). Preliminary specification work began
before the summer and implementation began in August. The goal here is to take
into account from the design of the OS all the issues that are often costly or
even impossible to apply afterward:
- security architecture
- formal proof and demonstration of correction
- general threat model