La Fondation RISC-V a annoncé avoir vérifié comment fonctionne le micro-noyau seL4 dans les systèmes avec l'architecture du jeu d'instructions RISC-V. Dans lequel le processus de vérification est réduit à la preuve mathématique de la fiabilité de seL4, qui indique la pleine conformité avec les spécifications spécifiées dans un langage formel.
Les tests de fiabilité permettent d'utiliser seL4 dans des systèmes critiques basés sur des processeurs RISC-V RV64, ce qui nécessite un niveau de fiabilité plus élevé et ne garantit pas l'échec.
Les développeurs de logiciels fonctionnant sur le noyau seL4 peuvent être totalement sûrs qu'en cas de défaillance d'une partie du système, cette défaillance ne se propage pas au reste du système et, en particulier, à ses parties critiques.
À propos de seL4
L'architecture seL4 est remarquable pour la suppression de parties pour gérer les ressources du noyau dans l'espace utilisateur et utiliser les mêmes méthodes 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 déjà prêt à gérer des fichiers, des processus, des connexions réseau, etc., mais à la place fournit uniquement des mécanismes minimaux pour contrôler l'accès à l'espace d'adressage physique, interruptions et ressources du processeur.
Des abstractions et des contrôleurs de haut niveau pour interagir avec l'ordinateur sont mis en œuvre séparément au-dessus du micro-noyau sous la forme de tâches effectuées au niveau de l'utilisateur.
L'accès de telles tâches aux ressources disponibles dans le micro-noyau est organisé par la définition de règles.
RISC-V fournit un système ouvert et flexible d'instructions machine qui permet de créer des microprocesseurs pour des applications arbitraires, sans nécessiter de déductions et sans imposer de conditions d'utilisation.
RISC-V vous permet de créer des SoC et des processeurs complètement ouverts. Actuellement, sur la base de la spécification RISC-V, plusieurs sociétés et communautés sous diverses licences libres (BSD, MIT, Apache 2.0) développent plusieurs dizaines de variantes de cœurs de microprocesseurs, de SoC et de puces déjà produits.
Le support RISC-V existe depuis la sortie de Glibc 2.27, binutils 2.30, gcc 7 et le noyau Linux 4.15.
À propos du test du micro-noyau seL4
Au départ, le micro-noyau seL4 a été vérifié pour les processeurs ARM 32 bitset plus tard pour les processeurs x86 64 bits.
On observe que la combinaison de l'architecture matérielle ouverte RISC-V avec le micro-noyau ouvert seL4 atteindra un nouveau niveau de sécurité, car les futurs composants matériels peuvent également être entièrement vérifiés, ce qui est impossible à réaliser pour les architectures matérielles propriétaires.
Lorsque nous vérifions seL4, nous devons supposer que le matériel fonctionne correctement (c'est-à-dire comme spécifié). Cela suppose qu'il existe une spécification sans ambiguïté en premier lieu, ce qui n'est pas le cas pour tout le matériel.
Mais même lorsqu'une telle spécification existe et qu'elle est formelle (c'est-à-dire écrite dans un formalisme mathématique qui prend en charge le raisonnement mathématique sur ses propriétés), comment savons-nous qu'elle capture réellement le comportement du matériel?
La réalité est que nous pouvons être à peu près sûrs que ce n’est pas le cas. Le matériel n'est pas différent du logiciel dans la mesure où les deux sont bogués.
Mais avoir un ISA ouvert présente des avantages qui vont au-delà de la gratuité. La première est qu'il permet des implémentations matérielles open source.
Lors de la vérification de seL4, on suppose que l'équipement fonctionne comme indiqué et que la spécification décrit complètement le comportement du système, mais en fait l'équipement n'est pas exempt d'erreurs, ce qui est bien démontré par des problèmes qui surviennent régulièrement dans le mécanisme d'exécution spéculative .
Les plates-formes matérielles ouvertes simplifient l'intégration des changements liés à la sécurité, par exemple, pour bloquer tous les canaux de fuite possibles via des canaux tiers, où il est beaucoup plus efficace de se débarrasser d'un problème par le matériel que d'essayer de trouver des solutions par le logiciel.
Enfin, si vous souhaitez en savoir plus, vous pouvez consulter la note dans le lien suivant
Pour moi, ce processeur est quelque chose qui m'appelle beaucoup. Il ne reste plus qu'à un gros chien informatique à fabriquer un ordinateur que nous pouvons acheter.
La question ARM est quelque chose qui me grince, vous avez déjà vu ce qui s'est passé avec Huawei avec les sanctions. Je suis clair que pour mon RISC-V, c'est une bien meilleure solution à tous les niveaux. Pour le moment, Huawei l'a déjà jeté un œil et peut-être qu'à l'avenir, ils disposeront d'un équipement avec ce micro. Si c'est le cas, il y aura sûrement plus d'entreprises qui l'adopteront et pour moi ce serait l'idéal et surtout que les distributions le supportent et pas seulement ARM comme c'est le cas pour la plupart.
+10