H2Lab présente ces travaux sur Camelot-OS à la plénière SecurEval
H2Lab est intervenu le 7 avril 2026 à la plénière du projet PEPR SecurEval pour présenter ses travaux sur Camelot-OS et son noyau Sentry, menés dans le cadre de la conception d’un OS sécurisé pour microcontrôleurs.
Camelot-OS, un OS Open-Source sécurisé
Camelot-OS s’appuie sur les résultats du projet Wookey (ANSSI, 2017-2021), poursuivis dans une réécriture orientée usage professionnel (Outpost-OS, Ledger, 2021-2025), avant de devenir un projet Open-Source porté par H2Lab depuis 2025.
Il cible les architectures ARMv7-M et ARMv8-M, avec un support RISC-V (RV32I) en cours de développement, et vise en priorité les équipements OT sécurisés : systèmes cyber-physiques, distribués ou basse consommation, avec un support temps réel initié (RMA, domaines).
Sentry face à SecurEval : protéger le noyau contre les fautes
Après un rapide retour sur les premiers travaux effectués dans le cadre du projet Wookey de l’ANSSI puis chez Ledger sur Outpost-OS, H2Lab présente les évolutions apportés dans les travaux autours des codes défensifs, avec le soutien des équipes du CEA-LSL.
Les travaux menés dans le cadre de SecurEval portent sur deux axes complémentaires :
Protection anti-fautes par le compilateur
- Duplication de comparaisons, redondance de calculs, distance de Hamming, typage fort
- Injection de code défensif sur les chemins critiques
- Analyse de la conformité du code généré et de son impact SWaP
- Évaluation des capacités d’un compilateur certifié (CompCert) pour cet usage
Vérification des protections par l’outillage et l’analyse
- Génération d’assertions défensives (e-acsl)
- Validation de la présence et de la conformité des protections post-compilation (Binsec)
- Évaluation de la résistance des solutions face à des modèles de fautes réalistes (Lazart)
- Comparaison de la couverture et de la complémentarité des outils
Surveiller le matériel pour compenser ses limites
Au-delà de la protection logicielle, une approche mixte HW/SW vise à compenser les limitations de la protection matérielle : détection du glitch RDP (cas du bootloader Wookey), détection de la corruption des registres MPU, et réaction à ces fautes (verrouillage, effacement, etc.). Ces travaux cherchent à déterminer les faiblesses de la vérification logicielle des états matériels et à évaluer la faisabilité de cette approche sur divers composants critiques (MPU, RTC, etc.).
Vous pouvez retrouver le support de présentation complet au format PDF : H2Lab & Camelot-OS - Plénière SecurEval 2026.
Le projet Camelot-OS est accessible via son site web et ses dépôts Github
#SecurEval #PEPRCybersécurité #CamelotOS #Sentry #H2Lab #SécuritéMatérielle #ProtectionAntiFautes #CEA #Frama-C #Binsec