Présentation du microkernel seL4 [PDF]

• seL4 est un microkernel d’OS qui exécute le mode noyau avec un minimum de code afin de contrôler les ressources matérielles et de renforcer la sécurité
• Il appartient à la famille des microkernels L4 et est développé depuis le milieu des années 1990
• Il peut fonctionner comme hyperviseur et prend en charge l’exécution d’OS invités comme Linux
• Il s’agit du premier noyau d’OS au monde dont la correction fonctionnelle a été prouvée, avec une preuve mathématique complète au niveau du code
• Il utilise un modèle de sécurité basé sur les capabilities pour un contrôle d’accès fin

Structure de seL4 et fonctions d’hyperviseur

• Noyau monolithique vs microkernel
  • Noyau monolithique (Linux, etc.) : le code noyau est massif, ce qui multiplie les vulnérabilités de sécurité → environ 20 millions de lignes de code (20M SLOC)
  • Microkernel (seL4) : usage d’un code noyau minimal → environ 10 000 lignes de code (10K SLOC)
  • Réduction de la taille du noyau → sécurité renforcée et surface d’attaque réduite
• seL4 remplit le rôle d’hyperviseur
  • Exécution possible d’un OS invité complet comme Linux dans une VM
  • Chaque VM s’exécute indépendamment, sans interférence possible entre elles → forte isolation garantie
  • Appels de procédure protégés (PPC) → communication sécurisée possible entre VM

Vérification et modèle de sécurité de seL4

• Vérification de la correction fonctionnelle
  • seL4 a fait l’objet d’une preuve mathématique de correction fonctionnelle au niveau du code
  • Cela garantit que tous les comportements du noyau respectent la spécification
• Validation de traduction (Translation Validation)
  • Il a été prouvé que le code binaire généré par le compilateur correspond exactement au code C d’origine
  • Exécuté via une chaîne d’outils automatisée
• Vérification des propriétés de sécurité
  • Confidentialité : accès aux données uniquement lorsqu’il est explicitement autorisé
  • Intégrité : modification des données uniquement lorsqu’elle est explicitement autorisée
  • Disponibilité : utilisation des ressources uniquement lorsqu’elle est explicitement autorisée

Modèle de sécurité basé sur les capabilities

• Qu’est-ce qu’une capability ?
  • Un jeton de sécurité accordant un droit d’accès à un objet donné
  • Encode à la fois la référence à l’objet et les droits d’accès
  • Permet un contrôle d’accès granulaire → application du principe du moindre privilège (Principle of Least Privilege, POLA)
• Avantages des capabilities
  • Contrôle d’accès fin → réduction possible des privilèges au minimum
  • Délégation et révocation des droits possibles
  • Modèle de sécurité puissant → supérieur au modèle traditionnel de contrôle d’accès (ACL)
• Résolution du problème du confused deputy
  • Dans les systèmes traditionnels fondés sur les ACL, l’état de sécurité est déterminé par l’identifiant de sécurité du sujet
  • Dans seL4, ce sont les capabilities qui déterminent directement les autorisations de sécurité → contrôle des droits plus clair

Prise en charge des systèmes temps réel et à criticité mixte

• Prise en charge des systèmes temps réel
  • seL4 prend en charge l’ordonnancement basé sur les priorités
  • L’analyse du pire temps d’exécution (WCET) de toutes les opérations du noyau est terminée → garantie de temps réel dur
• Prise en charge des systèmes à criticité mixte (Mixed-Criticality System, MCS)
  • Allocation et isolation des ressources CPU sur la base de contextes d’ordonnancement
  • Contrôle empêchant les tâches de haute priorité de monopoliser le CPU
  • Exécution simultanée possible de tâches critiques et non critiques

Performances et efficacité

• Le microkernel le plus performant
  • N’abaisse pas le niveau de sécurité même lorsque les performances sont critiques
  • Coût minimal des appels système et de l’IPC → plus de 5 fois plus rapide que des systèmes concurrents
• Des performances supérieures aux systèmes concurrents
  • Fiasco.OC : environ 2 fois plus lent que seL4
  • Zircon : environ 9 fois plus lent que seL4
  • CertiKOS : environ 5 fois plus lent que seL4

Applications concrètes et cyber retrofit

• Cas d’usage réels

  • Déployé avec succès dans l’ULB (hélicoptère sans pilote) de Boeing
  • Renforcement de la sécurité et amélioration de la stabilité du système confirmés

• Renforcement progressif de la sécurité des systèmes existants (Incremental Cyber Retrofit)

  • Exécution des systèmes existants dans des VM tout en les modularisant progressivement
  • Renforcement de la sécurité avec dégradation minimale des performances

Conclusion

• seL4 est le microkernel le plus sûr au monde, avec correction fonctionnelle, sécurité et performances démontrées
• Son modèle de sécurité vérifié et sa prise en charge des systèmes à criticité mixte le rendent utilisable de manière pratique dans de nombreux domaines
• Il permet de renforcer la sécurité et d’améliorer les performances des systèmes existants → un microkernel innovant qui équilibre sécurité et performance