Dernier journée au Fosdem: cette fois-ci le temps se gâte avec l’apparition du vent et de la neige, mais vu la foule présente il est exclu de prendre froid dans les salles !
seL4: Present and Future
Une présentation faite par Skype depuis l’Australie, sur seL4 qui est un micro-noyau issu de la famille des micro-noyaux L4. Il fait parti des micronoyaux les plus avancés actuellement.
Les micro-noyaux
Qu’est-ce qu’un micro-noyau ?
Contrairement aux noyaux monolithiques comme Linux, le but d’un micro-noyau est d’implémenter une partie d’un système d’exploitation en ne faisant fonctionner en ring0 que le strict minimum (ordonnancement, mémoire virtuelle, IPC de base). Le reste (systèmes de fichiers, pile réseau, pilotes de périphériques, …) fonctionne en espace utilisateur sous forme de services.
L’avantage est que comme très peu de code (Minix: environ 6000 lignes) fonctionne en mode privilégié (ring0), le principe de séparation des privilèges est plus facile à mettre en oeuvre.
Il en découle que si un bug se produit dans un service comme un système de fichiers, il suffit de recharger ce service. Idem pour les autres services, ce qui rend l’ensemble plus stable face aux inévitables bugs, qui par exemple sur un système Linux provoquent des kernel panic dont le seul remède consiste à redémarrer le système complet.
Inconvénient: contrairement aux noyaux monolithiques où l’appel à un service (réseau, fs, …) se fait directement au travers d’un syscall, un micro-noyau communique avec ses services à l’aide de messages IPC, ce qui est fatalement un peu plus lent (context-switching, émission/réception des messages, …)
Les premières générations de micro-noyaux comme [Mach](http://en.wikipedia.org/wiki/Mach_(kernel) étaient très lents, mais la seconde génération de micro-noyaux L4 montrent des gains en performance de plusieurs ordres de magnitude.
seL4
C’est quoi ?
seL4 est déclaré comme le micro-noyau le plus performant actuellement, passé en opensource en juillet 2014. Il se destine aux systèmes embarqués où la fiabilité et la sécurité sont les critères les plus importants.
Ce n’est pas un système d’exploitation complet, les services en espace utilisateur comme les pilotes de périphériques ou la pile réseau sont à écrire.
Dire que la sécurité est un critère important n’est pas un vain mot avec seL4, puisque c’est le premier micro-noyau au monde à pouvoir prouver par des preuves formelles mathématiques la confidentialité, l’intégrité et la disponibilité entre le modèle désiré, l’implémentation en C, et enfin le code binaire résultant.
Ce qui signifie qu’on peut formellement assurer que l’implémentation fait bien ce que la spécification décrit.
Au niveau de la sécurité, les buffers overflow, les problèmes avec les variables non-initialisées, les déréférencements de pointeurs NULL, l’injection de code, les ROP, la corruption de la pile d’exécution (stack smashing) peuvent devenir de l’histoire ancienne. Il y a encore du travail, mais ce n’est pas de la science-fiction.
Applications dans le monde réel
seL4 n’est pas un projet resté dans le monde universitaire, voici les applications commerciales:
- Il fait fonctionner l’hélicoptère léger Boeing AH-6.
- Projet HACMS (High-Assurance Cyber Military Systems) du DARPA, dont les applications sont des appareils où la vulnérabilité informatique doit être nulle (véhicules militaires, pacemakers, drones, installations industrielles (systèmes SCADA, …) présentation sur le sujet
- Il est utilisé dans le projet SMACCMPilot qui est un logiciel destiné à piloter les engins autonomes (drones entre autre).
- OKL4 est une version commerciale de L4, dont une déclinaison en hyperviseur léger. En 2012, il est déjà utilisé dans plus de 1.5 milliards de téléphones mobiles au travers des puces Qualcomm.
- Ordinateurs de voiture du groupe Bosch.
- Embarqué dans le SoC (system on a chip) Apple A7 depuis 2013, il est donc présent dans tous les appareils iOS comme les iPhones, iPads ou les Mac. Pour 2015 on parle déjà d’au moins 310 millions d’appareils.
The Secure Enclave uses encrypted memory and includes a hardware random number generator. Its microkernel is based on the L4 family, with modifications by Apple.
Source: ios-security-guide-sept-2014.pdf
J’ai été très étonné de voir que ce type de système est déjà très répandu, le tout dans une relative discrétion.
Avenir
La liste des fonctionnalités prévues est intéressante, et comme c’est opensource vous pouvez contribuer:
- Support 64 bits
- Support multicoeurs
- Création automatique des pilotes à partir des spécifications
- Ajout de nouvelles bibliothèques
- Portage sur des boards ARM
- Service pour la pile réseau, systèmes de fichier
- Support pour Python
A dedicated kernel named TORO
TORO est un système d’exploitation développé en Pascal par un unique développeur.
Son but est de faire tourner un seul applicatif dans un environnement multicoeurs, un peu comme les exokernels, qui sont bien plus petits que les kernel monolithiques (hello Linux) et offrent un accès plus direct au matériel (donc moins de couches d’abstraction)
En clair cela donne:
- Que du ring0 (!!), donc pas de syscalls
- L’application est compilée dans le noyau
- Un modèle mémoire à plat, sans pagination. L’espace mémoire est segmenté en 2: kernel+application / mémoire libre
Partager des ressources comme la mémoire sur un système multicoeurs induit un overhead: des locks (spinlock, …), de nombreux accès au bus mémoire pour voir qui utilise quoi, garder les caches cohérents si un processus se ballade de coeur en coeur, …
Pour éviter cela TORO va dédier des ressources propres à chaque coeur: un processus sera affecté à un coeur, avec son pool mémoire, ses accès disque, son système de fichiers.
C’est l’occasion de découvrir les technologies Intel QuickPath et le pendant AMD HyperTransport
Il est certain que TORO ne sera pas l’OS grand public de demain, mais comme tous les OS développés par curiosité, c’est toujours intéressant de savoir pourquoi certains choix ont été faits, quels ont été les problèmes d’implémentations et autres surprises.
Cloud services on top of uKernel
Cette présentation parle d’un travail en cours sur Genode, qui est une sorte de framework pour développer des systèmes très sécurisés et spécialisés, en mariant l’approche Unix et le principe des micro-noyaux L4.
Info intéressante: selon le présentateur, personne n’est prêt à sacrifier plus de 10% de performance pour plus de sécurité (grsec, pax, …)
Une illustration de l’usage de Genode est faite avec Redis, un KVS très connu. Actuellement ce duo est 40% plus lent que sur Linux, mais surprise, son concurrent OSv explose littéralement Linux.
Je n’ai pas noté les chiffres, mais dans cette présentation relative à Cassandra/OSv les graphiques montrent un gain d’environ 50% sur la plupart des opérations Redis.
OSv vaut le coup d’oeil: pour un applicatif Java qui tourne sur une VM, les couches d’abstractions s’empilent: hyperviseur-OS-Jvm. OSv se propose de réduire ce qui fait doublon dans ces couches, pour plus de performances et une administration simplifiée (plus d’OS, tout se gère directement au travers d’une API rest).
Une présentation relativement courte, mais qui montre encore que les micro-noyaux ont un bel avenir face aux systèmes généralistes comme Linux, autant dans les domaines de niche mais aussi dans les domaines à la mode comme le Cloud.
CAcert et key signing party
Petite pub pour CAcert: je reprends la présentation de cacert.org qui est très claire:
CAcert.org est une Autorité de Certification communautaire qui émet gratuitement des certificats pour tous.
Le but de CAcert est par la sensibilisation et l’éducation de promouvoir la sécurité informatique au travers de la cryptographie, spécialement en mettant à disposition des certificats cryptographiques.
Ces certificats peuvent être utilisés pour chiffrer des courriels et les signer électroniquement, authentifier et habiliter des utilisateurs se connectant sur des sites web ainsi que sécuriser la transmission de données sur internet.
Le processus d’accréditation prend environ 5/10min par accréditeur, et comme j’étais au stand entre midi et deux il n’y avait pas grand monde, j’ai pu obtenir mes 100 points assez rapidement, et donc devenir à mon tour accréditeur.
Pendant la keysigning party il m’a fallu environ 2h pour signer 112 clés sur les 206 initialement prévues, avec environ une centaine de personnes (certaines disposant de plusieurs clés).
Je reste surpris par l’absence totale de femmes durant la keysigning party, tout comme l’an dernier.
Living on Mars: A Beginner’s Guide
Pour finir la journée dans le grand amphi Janson, une conférence sur le projet privé Mars One, qui prévoit d’établir une base permanente sur Mars habitée dès 2024, autant dire demain.
Le choix de la planète Mars par rapport à d’autres astres est expliqué (radiations, température, pression, gravité, durée d’une année, …), ainsi que le coût bien moindre des voyages sans retour des premiers habitants de la colonie martienne.
Je n’ai pas bien perçu le lien avec le logiciel libre “Can we Open Source a society?”, mais certains chiffres sont impressionnants, comme le processus de sélection des 4 premières personnes à partir sur Mars, sur les 200 000 candidats au départ. En passant, le présentateur fait parti des 660 candidats encore en lice.
Avec une première phase dont le coût est estimé à plus de 6 milliards de $, le projet compte se financer avec la télé-réalité (Endeml)*. (qui semble finalement renoncer)
De nombreuses problématiques se posent encore, et le doute plane encore sur la faisabilité du projet.
Cette conférence m’a laissé dubitatif: mettre autant d’argent pour aller pourrir une autre planète, sous forme d’un Truman Show avec le voyeurisme de la télé-réalité ?