Le projet développant le micro-noyau open source seL4 a reçu le prix ACM Software System Award, décerné chaque année par l'Association for Computing Machinery (ACM), l'organisation internationale la plus reconnue dans le domaine des systèmes informatiques. Ce prix a été attribué pour les réalisations en matière de preuve mathématique de la fiabilité, qui démontre la conformité totale aux spécifications formelles, et reconnaît l'aptitude à être utilisé dans des applications critiques. Le projet seL4 a montré qu'il est possible d'effectuer une vérification formelle complète de la fiabilité et de la sécurité pour des projets de niveau des systèmes d'exploitation industriels, tout en maintenant la performance et la polyvalence.
Le prix ACM Software System Award est décerné chaque année pour le développement de systèmes logiciels ayant eu un impact majeur sur l'industrie, en introduisant de nouveaux concepts ou en révélant de nouveaux domaines d'application commerciale. Le montant du prix est de 35 000 dollars américains. Au cours des années précédentes, les prix ACM ont été attribués aux projets GCC et LLVM, ainsi qu'à leurs fondateurs Richard Stallman et Chris Lattner. Des projets et des technologies tels que UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB et Eclipse ont également été récompensés.
L'architecture du micro-noyau seL4 se distingue par le déplacement des parties de gestion des ressources du noyau dans l'espace utilisateur et l'application pour ces ressources des mêmes moyens de séparation d'accès que pour les ressources utilisateur. Le micro-noyau ne fournit pas d'abstractions haut niveau prêtes à l'emploi pour la gestion des fichiers, des processus, des connexions réseau, etc., mais il fournit uniquement des mécanismes minimaux pour gérer l'accès à l'espace d'adressage physique, aux interruptions et aux ressources du processeur. Les abstractions haut niveau et les pilotes pour interagir avec le matériel sont mis en œuvre séparément au-dessus du micro-noyau sous forme de tâches exécutées au niveau utilisateur. L'accès de ces tâches aux ressources du micro-noyau est organisé par la définition de règles.
Source : opennet.ru
