Présentation du microkernel seL4 [PDF]
(sel4.systems)- seL4 est un microkernel OS destiné aux systèmes embarqués et cyber-physiques où la sécurité et la sûreté sont critiques ; il isole et multiplexe les ressources matérielles, mais ne constitue pas un OS généraliste complet
- En réduisant le code en mode noyau à environ 10 kSLOC, il diminue la TCB et la surface d’attaque, tout en repoussant les services OS comme le système de fichiers, le réseau et les pilotes en mode utilisateur
- C’est le premier noyau OS au monde à disposer d’une vérification formelle au niveau du code, et dans un système correctement configuré, le noyau garantit même des propriétés de sécurité comme la confidentialité, l’intégrité et la disponibilité
- Il combine contrôle d’accès fondé sur les capabilities, analyse WCET, prise en charge des systèmes temps réel à criticité mixte et fonctions d’hyperviseur pour offrir à la fois isolation fine et garanties temps réel
- L’API de seL4 est de très bas niveau, ce qui rend difficile la construction directe de systèmes complexes ; lorsqu’une architecture statique convient, utiliser un framework comme Microkit est une approche réaliste
Ce que couvre seL4
- seL4 est un microkernel, c’est-à-dire le cœur bas niveau d’un système d’exploitation
- L’OS contrôle le matériel et les ressources dans le mode noyau, qui dispose de privilèges d’exécution plus élevés sur le processeur
- Les applications s’exécutent en mode utilisateur et n’accèdent au matériel que selon les modalités autorisées par l’OS
- Un microkernel est le cœur d’un OS qui minimise le code exécuté avec de hauts privilèges
- seL4 appartient à la famille des microkernels L4, dont l’histoire remonte au milieu des années 1990
- seL4 n’a aucun lien avec seLinux
- seL4 n’est pas un OS complet, mais un noyau bas niveau qui multiplexe et isole les ressources matérielles de manière sûre
- Les services OS classiques comme le système de fichiers, la pile réseau ou les pilotes de périphériques ne se trouvent pas dans le noyau
- Ces services doivent être fournis par des programmes en mode utilisateur
Architecture microkernel et réduction de la surface d’attaque
- Les noyaux monolithiques comme Linux fournissent des services OS tels que le stockage de fichiers ou le réseau sous forme de code en mode noyau
- Le code en mode noyau peut accéder sans restriction aux ressources système ; ainsi, si un bug mène à une élévation de privilèges ou à l’exécution de code arbitraire, c’est l’ensemble du système qui peut être compromis
- Le noyau Linux représente environ 20 MSLOC, et l’on estime qu’il peut contenir des dizaines de milliers de bugs
- Un microkernel bien conçu comme seL4 ramène le code en mode noyau à environ 10 kSLOC
- C’est trois ordres de grandeur de moins que le noyau Linux
- Quand la TCB diminue, la surface d’attaque diminue aussi
- La plupart des services OS sortent du noyau, et le microkernel agit comme une fine couche autour du matériel
- Les fonctions essentielles fournies sont l’isolation entre programmes et un mécanisme d’appel sûr
- Les services ne s’exécutent pas dans le noyau, mais comme des programmes en mode utilisateur dans des sandboxes séparées
- Une étude ayant analysé des cas connus de compromission Linux jugés critiques a montré qu’une architecture microkernel pouvait en éliminer complètement 29 % et en atténuer 55 % supplémentaires au point qu’ils ne seraient plus classés comme critiques
PPC, capabilities et contrôle fin des privilèges
- seL4 fournit un mécanisme d’appel de procédure protégé (PPC)
- Pour des raisons historiques, le terme IPC reste utilisé, mais cette terminologie peut induire en erreur et mener à de mauvaises conceptions
- Le PPC permet à un programme d’appeler en toute sécurité une fonction d’un autre programme situé dans une autre sandbox
- Le microkernel transmet les entrées et les sorties lors d’un PPC et impose l’interface
- Une fonction distante ne peut être appelée que via un point d’entrée exporté
- Seuls les clients explicitement autorisés ayant reçu la capability appropriée peuvent l’appeler
- Une capability est un jeton d’accès qui permet d’accéder à une ressource précise du système
- Elle permet de contrôler avec une très grande finesse qui peut accéder à quelle ressource
- Elle prend en charge le principe du moindre privilège, ou POLA
- Les mécanismes de contrôle d’accès des systèmes dominants comme Linux ou Windows ne permettent pas d’atteindre ce niveau de moindre privilège
- seL4 est le seul OS au monde à être à la fois fondé sur les capabilities et formellement vérifié ; cette combinaison permet de défendre l’idée qu’il s’agit de l’OS le plus sûr au monde
Vérification formelle et garanties de sécurité
- seL4 fournit des preuves formelles, mathématiques et vérifiées par machine de la correction de son implémentation
- Ces preuves signifient, dans un sens très fort par rapport à la spécification, que le noyau est « sans bug »
- seL4 est le premier noyau OS au monde à disposer de telles preuves au niveau du code
- Au-delà de la correction d’implémentation, seL4 fournit aussi des preuves supplémentaires concernant l’application des politiques de sécurité
- Dans un système basé sur seL4 correctement configuré, le noyau garantit la confidentialité, l’intégrité et la disponibilité
- La chaîne de vérification constitue l’élément distinctif central de seL4
- Pour qu’un noyau serve de base de confiance dans des systèmes critiques pour la sécurité ou la sûreté, de fortes garanties sur l’implémentation et sur les propriétés de sécurité sont nécessaires
Temps réel et systèmes à criticité mixte
- seL4 est un noyau OS ayant fait l’objet d’une analyse complète et solide du WCET (temps d’exécution dans le pire des cas)
- Si le noyau est correctement configuré, toutes les opérations noyau ont une borne temporelle
- Et cette borne est connue
- Ces caractéristiques sont une condition préalable à la construction de systèmes temps réel stricts
- Il s’agit de systèmes où le fait de ne pas réagir à un événement dans un délai strictement limité peut avoir des conséquences catastrophiques
- seL4 prend aussi en charge les systèmes temps réel à criticité mixte (MCS)
- Ils visent des environnements où il faut garantir les propriétés temporelles d’activités importantes, même lorsque du code moins fiable s’exécute sur la même plateforme
- Contrairement au partitionnement strict et peu flexible du temps et de l’espace utilisé par les OS MCS traditionnels, seL4 propose un modèle plus souple qui préserve l’utilisation des ressources
Utiliser seL4 comme hyperviseur
- seL4 est à la fois un microkernel et un hyperviseur
- Il permet d’exécuter des machines virtuelles au-dessus de seL4
- À l’intérieur de ces machines virtuelles, il est possible d’exécuter un OS invité classique comme Linux
- Les invités et les applications peuvent communiquer entre eux selon les canaux de communication imposés par seL4
- Ils peuvent aussi communiquer avec des applications natives
- Une VM Linux peut être utilisée pour fournir des services système
- Dans une configuration d’exemple, des services comme le réseau et le stockage sont fournis par plusieurs instances Linux exécutées dans des VM séparées
Comment construire un système sur seL4
- L’API de seL4 est de très bas niveau, même par rapport à d’autres microkernels
- Elle ne fournit que les abstractions minimales nécessaires à la gestion sûre du matériel
- seL4 est comparé à un « langage assembleur des systèmes d’exploitation »
- Construire directement des systèmes complexes sur seL4 n’est pas une approche adaptée
- Un framework de plus haut niveau doit permettre de se concentrer sur le code métier des services, tout en automatisant la complexité matérielle et l’intégration système
- seL4 dispose de trois grands frameworks open source pour les composants
- Microkit : simplifie l’API seL4 avec un petit nombre d’abstractions centrées sur les domaines de protection, et fournit un SDK qui assemble modules compilés séparément et binaire noyau pour produire une image amorçable
- CAmkES : prédécesseur de Microkit et framework de composants pour systèmes à architecture statique, mais sans SDK, ce qui rend le processus de build plus contraignant et plus coûteux en overhead
- Genode : prend en charge plusieurs microkernels et offre de nombreux services et pilotes pour les plateformes x86 ; il n’impose pas d’architecture statique, mais ne permet pas de tirer parti de toutes les fonctions de sécurité et de sûreté de seL4 et ne bénéficie pas des mêmes garanties
- Tant qu’une architecture système statique correspond aux besoins, Microkit est recommandé pour construire des systèmes sur seL4
- Une architecture statique est un modèle dans lequel l’ensemble des modules et leur structure de communication sont définis au moment de la configuration du système
- Ce modèle est considéré comme adapté aux besoins de la plupart des systèmes embarqués, y compris les systèmes cyber-physiques complexes comme ceux de l’automobile et de l’aéronautique
1 commentaires
Avis sur Hacker News
seL4 lui-même est une vieille histoire, mais je me demande si de nouvelles couches ou composants formellement vérifiés ont été ajoutés au-delà du microkernel
Par ailleurs, il semble aussi y avoir des gens qui, dès qu’ils voient le mot « preuve », subissent une surcharge émotionnelle et cessent de réfléchir. La vérification formelle n’est ni une panacée qui résout le problème infini de l’informatique sûre, ni une méthode pour produire des logiciels parfaitement irréprochables
Si je comprends bien, c’est une preuve que certaines exigences sont satisfaites dans certaines conditions, et ces exigences comme ces conditions peuvent être assez étroites ; cela ne dit rien sur les fonctionnalités et conditions hors spécification. Est-ce à peu près correct ?
En pratique, je me demande aussi ce qu’un spécialiste de la sécurité attend lorsqu’il voit un « logiciel formellement vérifié ». Il me semble que l’information clé ici est de savoir quelle spécification seL4 satisfait
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
Le suivi des issues contient aussi plusieurs bugs liés à la mémoire
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Fait intéressant, la PR qui corrige le « register clobbering » en mémoire n’a pas le label bug, donc elle n’apparaît pas quand on filtre sur « bug ». Avant, je pensais que, grâce aux preuves, seL4 était immunisé contre ce genre de problème ; après avoir vu cela, j’en suis venu à considérer que les preuves ne sont pas aussi exhaustives que ce que la communauté a fini par croire. Malgré tout, seL4 reste un logiciel très impressionnant
Pour répondre à la question, la spécification que satisfait seL4 est publiée sur GitHub
https://github.com/seL4/l4v
Le scheduling à criticité mixte fournit un accès au temps CPU fondé sur des capabilities, des limites supérieures d’exécution des threads, la garantie de priorité et d’accès aux ressources pour les tâches de haute criticité, ainsi que des « passive servers » qui tournent avec du temps de scheduling donné par l’appelant
Microkit est une couche d’abstraction vérifiée qui rend beaucoup plus simple la construction de systèmes réels au-dessus de seL4, et le Device Driver Framework est un ensemble de gabarits de pilotes de périphériques, d’implémentations de plans de contrôle/données, et d’outils d’écriture de pilotes et de virtualisation de périphériques pour les E/S haute performance sur seL4
La vérification formelle peut garantir que certaines exigences valent dans certaines conditions. En général, il est exact que ces exigences et conditions peuvent être étroites, mais seL4 lui-même dispose de nombreuses preuves couvrant un large éventail de propriétés que l’on peut attendre d’un kernel, et ces garanties tiennent même sous des hypothèses très faibles. On ne suppose même pas l’exactitude du compilateur C : il existe un outil séparé qui examine la sortie du compilateur et prouve que le binaire compilé se comporte conformément à la sémantique C requise
Parmi les exigences satisfaites par seL4 figure le fait que le code binaire du kernel seL4 implémente exactement le comportement décrit dans la spécification abstraite, et rien de plus. Il n’y a pas de dépassements de tampon, de fuites mémoire, d’erreurs de pointeurs, de déréférencements de pointeurs nuls, de comportement indéfini du code C, ni d’arrêt du kernel autrement que par les méthodes explicites énumérées dans la spécification
La spécification et le binaire seL4 satisfont aussi des propriétés de sécurité d’intégrité et de confidentialité. L’intégrité signifie qu’un processus n’a absolument aucun moyen de modifier des données pour lesquelles il n’a pas de permission explicite, et la confidentialité signifie qu’il ne peut lire d’aucune manière des données non autorisées. Il est même montré qu’il n’est pas possible d’inférer indirectement des données via certains canaux auxiliaires. Au-delà de la sécurité, des garanties de temps d’exécution au pire cas attendu et des propriétés de scheduling sont également satisfaites
Le travail actuel va plutôt vers LionsOS, qui vise une adoption plus large : https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
Cela utilise beaucoup de programmation au niveau des types pour suivre les ressources, l’accès au matériel et les capabilities au moment de la compilation. Découvrir et déboguer les problèmes à l’exécution est tellement pénible que c’est une tentative de faire remonter une partie des garanties du kernel sous-jacent vers le compilateur
J’aime les hôtes microkernel qui exécutent des kernels monolithiques invités ; sur mes serveurs, je fais donc tourner seL4 comme couche de sécurité et de sauvegarde pour des VM FreeBSD, à l’intérieur desquelles j’utilise des jails pour une renderfarm, un cluster BEAM et Jenkins
Ce qui est dommage, c’est l’absence de port ARM pour le threading et le kernel interne aux processus de DragonFlyBSD, c’est-à-dire pour sa conception de kernel hybride. Mon rêve serait de faire tourner OpenMoonRay plus efficacement sur un Ampere Altra à 128 cœurs
Désormais, le débat pour ou contre les microkernels semble perdre beaucoup de son sens. Le seul moyen d’accéder à des services privilégiés de façon rapide, efficace et sûre, ce sont les mesures d’atténuation matérielles, et ce que le logiciel peut faire a des limites
C’est un peu comme la différence entre le 80286 et le 80386. Le second a ajouté une véritable prise en charge matérielle du multitâche que le premier n’avait pas. Depuis, les mécanismes de protection au niveau matériel, comme ceux qui ont rendu possibles les hyperviseurs, n’ont cessé de se multiplier
Apple, en particulier, ajoute dans ses SoC de nombreuses fonctions qui protègent le kernel, les pilotes et les composants au niveau de la puce, et qui imposent les privilèges lors de l’utilisation des threads en cours d’exécution et des pointeurs. https://support.apple.com/guide/security/operating-system-in...
Cela ne veut pas dire qu’un OS ne peut pas être compromis, mais c’est beaucoup plus efficace qu’une stratégie consistant à gérer les privilèges uniquement par logiciel. En exploitant ce type de fonctions, ou des fonctions similaires, la structure du kernel ne semble plus vraiment si importante ; je me demande si je me trompe
Il y a aussi beaucoup à apprendre de systèmes micro/hybrides plus composables. Par exemple, Plan 9 est un excellent système hybride qui expose tous les objets du système à l’espace utilisateur via un protocole unique, 9P. C’est un hybride parce que certaines parties, comme IP ou TLS, résident dans le kernel afin d’éviter le surcoût des appels système
Un autre aspect intéressant de sa conception est que les pilotes internes au kernel sont, pour l’essentiel, des formes minimales qui ne servent que d’interface 9P vers la logique matérielle. Cela permet de transformer des objets machine comme des pointeurs ou des enregistrements en fichiers navigables, de protéger ces fichiers avec les permissions Unix standard, et de répartir facilement des composants sur plusieurs machines via le réseau. Résultat : la logique des pilotes peut être repoussée en toute sécurité vers des programmes en espace utilisateur
9P est transparent vis-à-vis du réseau et de l’architecture, si bien que des machines Arm, x86, mips, etc. peuvent travailler ensemble directement. Revenir de Plan 9 à Linux/Unix ou Windows est triste et frustrant. Leur flexibilité est presque du niveau de la roche magmatique, et les fonctionnalités y sont ajoutées au moyen d’une multitude de protocoles incompatibles entre eux qui font pourtant la même chose : exposer des fichiers/objets
D’un point de vue d’ingénierie pratique, les kernels monolithiques étaient plus rapides, plus simples et disposaient de plus de ressources, tandis que la sécurité était ce que C permettait : du best effort et une multitude de bugs. Beaucoup de matériel a été introduit pour atténuer ce bazar. Mais avec SeL4, la confiance dans l’isolation entre processus et dans l’absence d’exploits de niveau root est très élevée, si bien qu’en théorie un coprocesseur de sécurité pourrait ne pas être nécessaire. La co-conception matériel/logiciel est donc importante
Cela dit, l’équipe SeL4 a elle aussi dû consacrer beaucoup de ressources d’ingénierie à éliminer les canaux auxiliaires du matériel. Le monde réel ne se soucie pas des simulations physiques, donc le matériel a lui aussi des défauts
L’avantage d’un microkernel, ici, est qu’il est assez petit pour être traité par la vérification formelle. La preuve elle-même fait dix fois la taille du kernel. Les changements de contexte de SeL4 sont d’un ordre de grandeur plus rapides que ceux de Linux, donc l’impact sur les performances devrait être négligeable. Mais si l’on pouvait vérifier comme par magie un kernel monolithique de plusieurs millions de lignes, l’absence de changement de contexte resterait plus rapide. En pratique, l’équipe SeL4 a tenté de déplacer l’ordonnanceur en espace utilisateur, mais le coût en performances était trop élevé ; elle l’a donc laissé dans le kernel et l’a ajouté à la charge de preuve
Le rôle principal du matériel est plutôt d’améliorer l’efficacité. Par exemple, les microkernels actuels utilisent déjà bien du matériel comme la MMU, ce qui les rend assez robustes. Ensuite, la petite base de calcul de confiance d’un microkernel apporte de la fiabilité au kernel, et le kernel et le matériel forment ensemble une base solide
Au final, c’est une question de jusqu’où l’on autorise le matériel à « tricher », mais globalement les microkernels exploitent mieux les fonctions de protection. Sinon, on peut aussi regarder du côté des exokernels
https://genode.org/index
C’est un système d’exploitation avec prise en charge de seL4
J’ai déjà fait une présentation sur seL4 dans un chapitre OWASP local. Je ne sais pas si je pourrais retrouver les supports
Ce projet est vraiment très bien conçu, mais j’hésite à le voir comme un substitut à Linux, surtout pour l’informatique généraliste. Cela ne veut pas dire pour autant que les microkernels sont globalement mauvais pour un usage généraliste. RedoxOS semble avoir fait quelques progrès récemment et utilise un microkernel écrit en Rust
Cela dit, si Redox réussit, ce sera déjà une belle avancée. seL4 pousse ces caractéristiques encore plus loin. Ses mérites techniques sont excellents, mais il ne semble pas avoir eu jusqu’ici, ni probablement avoir à l’avenir, ce qu’il faut pour devenir « la prochaine grande tendance ». Si l’on met de côté les considérations politiques, je pense que les microkernels réussiront, et qu’ils le devraient
Pour que seL4 soit réellement utile, il faut beaucoup de choses au-dessus. Heureusement, beaucoup de travail open source a aussi été mené sur cette partie, et la situation est bien meilleure qu’il y a quelques années
Pour les scénarios statiques, il y a LionsOS[0], déjà assez utilisable
Pour les scénarios dynamiques, il y a Provably Secure, General-Purpose Operating System[1], mais c’est encore à un stade précoce
On peut trouver les deux sur la page Projects de trustworthy systems[2], liée depuis le site de seL4
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
Je me demande si, pour que les garanties de sécurité soient valables, l’OS qui tourne au-dessus de ce kernel doit lui aussi être formellement vérifié
Bien sûr, le kernel seul n’est pas très utile, donc la conception des pilotes, serveurs de système de fichiers et autres services qui s’exécutent au-dessus du kernel reste importante
Il faut aussi noter que la plupart des autres systèmes, y compris Linux, sont défectueux à un niveau fondamental, tandis que seL4 permet réellement de construire des systèmes sûrs et fiables
On peut ainsi exécuter un kernel Linux à côté d’un processus à haute sécurité, tout en ayant la garantie qu’ils restent isolés l’un de l’autre, sauf pour les IPC autorisés
Mais il y a des limites. Il faut désactiver le DMA, et n’utiliser que des pilotes eux aussi formellement vérifiés
Il est aussi important de noter que le kernel multicœur de seL4 n’est pas encore vérifié
Le microkernel Helios de Drew DeVault vaut aussi le détour. Il serait basé sur seL4
https://ares-os.org/docs/helios/
À l’université de Karlsruhe, L4 était populaire. Je ne l’ai jamais examiné en détail, mais cela ressemblait à un projet surtout intéressé par la mise à l’épreuve d’idées théoriques plutôt que par la création de quelque chose de pratiquement utile.
C’était il y a 20 ans et, à mes yeux, cela n’a pas beaucoup changé aujourd’hui. Une recherche rapide montre qu’il semble y avoir eu des tentatives de construire des OS par-dessus, mais elles paraissent plus proches de preuves de concept que d’un usage réel.
« Les livraisons d’OKL4 dépassaient 1,5 milliard d’unités début 2012, principalement des puces de modem sans fil Qualcomm. Parmi les autres déploiements figurent des systèmes d’infodivertissement automobile. »
« Les processeurs Apple A-series à partir de l’A7 contiennent un coprocesseur Secure Enclave exécutant un système d’exploitation L4 ; cet OS est sepOS, basé sur le noyau L4-embedded développé au NICTA en 2006. En conséquence, L4 est présent sur tous les appareils Apple modernes, y compris les Mac équipés d’Apple silicon. »
Rittinghaus, un ancien étudiant de Bellosa, participe à Unikraft[0], qui a été présenté plusieurs fois sur HN, et utilise la technologie des unikernels.
[0] https://unikraft.org/
« Le Secure Enclave Processor exécute une version du microkernel L4 personnalisée par Apple. »
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
À mon avis, le noyau L4Re fait aussi partie d’Elektrobit Safe Linux.
Pour mon mémoire de fin d’études, j’ai créé un OS basé sur Pistachio. J’ai toujours pensé que, si j’avais étudié à Karlsruhe, je me serais probablement orienté vers la recherche sur les OS.
J’avais moi aussi des idées de conception de système d’exploitation, et les capabilities que j’envisageais utilisaient les mêmes fonctions d’interposition et de délégation que seL4. Il y a d’autres avantages que ceux mentionnés. Par exemple, on peut utiliser des capabilities proxy pour appliquer des filtres à l’audio ou mettre en œuvre la transparence réseau.
Je pensais que les fonctionnalités temps réel pouvaient être autorisées sous forme d’implémentation optionnelle. Mon idée relevait davantage d’une spécification que d’une implémentation unique.
Une autre fonctionnalité que je voulais était que tous les programmes se comportent de manière déterministe, à l’exception des entrées/sorties. Sans entrées/sorties, il est impossible de connaître la date/l’heure ou le temps d’exécution du programme, ni de vérifier les fonctionnalités du processeur. Si une fonctionnalité non prise en charge par le matériel est utilisée, le système d’exploitation peut toutefois l’émuler.
Pour réaliser cela, je pensais combiner support matériel et support logiciel. Le document contient une note sur les attaques contre les capabilities implémentées en matériel, mais comme je n’ai pas le document de référence, je ne sais pas si cette attaque s’applique aussi à l’approche que j’avais en tête.
Du point de vue de la sécurité, cela semble présenter le même échec que KVM dans le noyau Linux. Si l’hyperviseur est en ring 0, il existe un risque de s’échapper d’une VM vers une autre VM, voire vers l’hôte lui-même.
Je me demande comment ce risque est atténué.
Le VMM ne possède pas plus de capabilities que la VM elle-même ; une évasion de VM n’a donc pas d’intérêt, sauf au sens académique.
Voir les pages 8 à 10 du PDF original.