Le travail sur la vérification formelle mathématique de la fiabilité et de la sécurité du fonctionnement du micro-noyau seL4 sur les systèmes avec une architecture de jeu d'instructions AArch64 est terminé. La vérification se résume à une preuve mathématique de la correction du fonctionnement de seL4, qui témoigne de la conformité complète aux spécifications définies dans un langage formel. La preuve de fiabilité permet d'utiliser seL4 dans des systèmes critiques basés sur des processeurs ARM64, nécessitant un niveau de sécurité élevé et garantissant l'absence de pannes.
À l'origine, le micro-noyau seL4 a été vérifié pour les processeurs ARM 32 bits, puis pour les processeurs 64 bits x86 et RISC-V. La vérification garantit que, en cas de défaillance dans une partie du système, cette défaillance ne se propagera pas au reste du système et à ses parties critiques. Dans le cadre de la sécurité, la vérification confirme que le noyau assure un niveau d'isolation adéquat des applications, ne leur permet pas d'accéder à des informations sans autorisation et garantit qu'en cas de compromission d'applications secondaires, l'attaque ne se propagera pas aux applications critiques.
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
