seL4 est le seul micronoyau au monde qui a été formellement prouvé, en 2009, conforme à ses spécifications, sans bogue, et donc sûr, si configuré correctement.
Un micronoyau est le noyau minimal nécessaire à un système d’exploitation, ne fournissant que les services de base comme le contrôle de l’accès à l’espace mémoire, les interruptions et le temps processeur.
Contrairement à Linux, MacOS ou Windows, il ne cherche pas à fournir des abstractions de haut niveau comme des fichiers, des processus ou des sockets : un micronoyau a pour but de déporter le plus de code possible hors du noyau et dans l’espace utilisateur, à la fois pour des raisons de sécurité, et pour être indépendant de toute politique.
Sel4, qui est en code source ouvert, est largement exploité pour des systèmes militaires et des systèmes embarqués.
Aujourd’hui, pour soutenir l’écosystème, une fondation est établie, et les candidatures des membres sont ouvertes.
La fondation, une organisation à but non lucratif établie par Data61, la branche spécialisée en numérique de l’agence australienne pour la science CSIRO, est hébergée par la Linux Foundation, et ses organes, ses politiques et son fonctionnement sont calqués sur cette dernière.
La fondation, dont les membres fondateurs incluent Cog Systems, DornerWorks, Ghost Locomotion, HENSOLDT Cyber et UNSW Sydney, a pour but d’accélérer le développement de seL4 et des technologies liées, et d’être l’organisation globale, indépendante et neutre en charge du financement et du pilotage des futures évolutions du micronoyau.