Le projet développant le micro-noyau ouvert seL4 a reçu le ACM Software System Award, décerné chaque année par l'Association for Computing Machinery (ACM), l'organisation internationale la plus faisant autorité dans le domaine des systèmes informatiques. Le prix est décerné pour les réalisations dans le domaine de la preuve mathématique de la fiabilité de fonctionnement, qui démontrent la pleine conformité aux spécifications spécifiées dans un langage formel et reconnaissent la disponibilité pour une utilisation dans des applications critiques. Le projet seL4 a montré qu'il est non seulement possible de vérifier formellement la fiabilité et la sécurité des conceptions industrielles au niveau des systèmes d'exploitation, mais également d'y parvenir sans compromettre les performances et la polyvalence.
L'ACM Software System Award est décerné chaque année pour reconnaître le développement de systèmes logiciels qui ont eu un impact déterminant sur l'industrie, en introduisant de nouveaux concepts ou en ouvrant de nouveaux domaines d'application commerciale. Le montant de la récompense est de 35 XNUMX dollars américains. Au cours des dernières années, des prix ACM ont été décernés aux projets GCC et LLVM ainsi qu'à leurs fondateurs Richard Stallman et Chris Latner. Le prix a également récompensé 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. .
L'architecture du micronoyau seL4 se distingue par le déplacement des pièces permettant de gérer les ressources du noyau dans l'espace utilisateur et par l'utilisation des mêmes outils de contrôle d'accès pour ces ressources que pour les ressources utilisateur. Le micro-noyau ne fournit pas d'abstractions de haut niveau prêtes à l'emploi pour la gestion des fichiers, des processus, des connexions réseau, etc. ; au lieu de cela, il ne fournit que des mécanismes minimaux pour contrôler l'accès à l'espace d'adressage physique, aux interruptions et aux ressources du processeur. Les abstractions de haut niveau et les pilotes pour interagir avec le matériel sont implémentés séparément au-dessus du micro-noyau sous la forme de tâches au niveau de l'utilisateur. L'accès de ces tâches aux ressources dont dispose le micronoyau est organisé à travers la définition de règles.
Source: opennet.ru