Organisation RISC-V Foundation concernant la vérification du fonctionnement du micro-noyau sur des systèmes avec une architecture de jeu d'instructions RISC-V. La vérification se résume à de la fiabilité du seL4, qui témoigne de la conformité totale avec les spécifications établies dans un langage formel. La preuve de fiabilité seL4 dans des systèmes critiques basés sur les processeurs RISC-V RV64, qui nécessitent un niveau de fiabilité accru et garantissent l'absence de pannes. Les développeurs de logiciels fonctionnant au-dessus du noyau seL4 peuvent être pleinement assurés que, en cas de défaillance d'une partie du système, cette défaillance ne se propagera pas au reste du système et, en particulier, à ses parties critiques.
À l'origine, le micro-noyau seL4 a été vérifié pour des processeurs ARM 32 bits, puis pour des processeurs x86 64 bits. On note que la combinaison de l'architecture matérielle ouverte RISC-V avec le micro-noyau ouvert seL4 permettra d'atteindre un nouveau niveau de sécurité, car les composants matériels pourraient également être entièrement vérifiés à l'avenir, ce qui n'est pas réalisable pour les architectures matérielles propriétaires.
Lors de la vérification de seL4, il est supposé que le matériel fonctionne comme annoncé et que la spécification décrit complètement le comportement du système, mais en réalité, le matériel n'est pas exempt d'erreurs, comme le montrent bien les problèmes récurrents liés au mécanisme d'exécution spéculative des instructions. Les plateformes matérielles ouvertes facilitent l'intégration des changements liés à la sécurité — par exemple, pour bloquer tous les canaux potentiels de fuite par des canaux latéraux, où il est beaucoup plus efficace de résoudre le problème au niveau matériel plutôt que de chercher des solutions logicielles.
Rappelons que l'architecture seL4 la délocalisation des parties pour la gestion des ressources du noyau dans l'espace utilisateur et l'application des mêmes moyens de séparation 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. Il ne propose que des mécanismes minimaux pour gérer l'accès à l'espace d'adresses physiques, aux interruptions et aux ressources du processeur. Les abstractions de haut niveau et les pilotes pour interagir avec le matériel sont mis en œuvre séparément au-dessus du micro-noyau sous la forme de tâches exécutées au niveau utilisateur. L'accès de ces tâches aux ressources disponibles auprès du micro-noyau est organisé par la définition de règles.
RISC-V fournit un système d'instructions machine ouvert et flexible, permettant de créer des microprocesseurs pour des applications variées, sans nécessiter de redevances et sans imposer de conditions d'utilisation. RISC-V permet de créer des SoC et des processeurs entièrement ouverts. Actuellement, des dizaines d'options de noyaux de microprocesseurs, SoC et de puces déjà produites sont basées sur la spécification RISC-V, par différentes entreprises et communautés sous diverses licences gratuites (BSD, MIT, Apache 2.0). Le support de RISC-V est présent depuis les versions de Glibc 2.27, binutils 2.30, gcc 7 et du noyau Linux 4.15.
Source : opennet.ru
