L'entreprise Google a présenté un système matériel et logiciel nommé Open Se Cura, conçu pour simplifier la création de puces sécurisées destinées à des tâches liées à l'apprentissage automatique et à l'intelligence artificielle. Le projet comprend un système d'exploitation, CantripOS, et un matériel basé sur la plateforme OpenTitan et un cœur de processeur utilisant l'architecture RISC-V. Pendant le développement, Open Se Cura et CantripOS ont été connus sous les noms de Sparrow et KataOS, mais pour éviter toute confusion avec d'autres projets, les produits finaux ont été renommés. Les travaux du projet, y compris le code source des services systèmes et les schémas RTL (Register Transfer Level), sont diffusés sous la licence Apache 2.0.
Le système d'exploitation CantripOS est basé sur le micro-noyau seL4, sur lequel s'exécute un environnement système écrit en Rust. Pour les systèmes RISC-V, une preuve mathématique de fiabilité a été fournie pour le micro-noyau seL4, attestant de la conformité complète du code aux spécifications définies dans un langage formel. L'architecture seL4 se distingue par le déplacement de certaines parties de la gestion des ressources du noyau dans l'espace utilisateur et par l'application des mêmes moyens 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 offre uniquement des mécanismes minimaux pour gérer l'accès à l'espace d'adresses physiques, aux interruptions et aux ressources 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 forme de tâches exécutées au niveau utilisateur. L'accès de ces tâches aux ressources disponibles du micro-noyau est organisé par la définition de règles.
Tous les composants du système d'exploitation, à l'exception du micro-noyau, sont initialement écrits en Rust en utilisant des techniques de programmation sûres, minimisant les erreurs liées à la gestion de la mémoire. En Rust, parmi d'autres éléments, le chargeur d'applications dans l'environnement seL4, les services système, le cadre de développement d'applications, l'API d'accès aux appels système, le gestionnaire de processus et le mécanisme de répartition dynamique de la mémoire ont été écrits.
Pour une compilation vérifiée, l'outil CAmkES, développé par le projet seL4, est utilisé. Pour le développement d'applications finales pouvant être chargées dynamiquement par les services système, il est proposé d'utiliser le SDK AmbiML, et pour l'exécution des modèles d'apprentissage automatique, l'outil IREE (Intermediate Representation Execution Environment) est recommandé. Les composants en Rust et les services système ont été développés en utilisant les cadres Cantrip.
Les domaines d'application de la plateforme comprennent des puces spécialisées nécessitant un niveau de protection particulier et la garantie de l'absence de défaillances. Par exemple, la plateforme peut être utilisée dans des produits d'apprentissage automatique liés au traitement d'informations confidentielles, comme les systèmes de reconnaissance faciale et de traitement des enregistrements vocaux. La combinaison d'un noyau d'exploitation logiquement vérifié avec des composants matériels dignes de confiance (RoT, Root of Trust) garantit qu'en cas de défaillance d'une partie du système, cette défaillance ne se propage pas au reste du système, en particulier au noyau et aux parties critiques.
Outre Google, la création d'outils et d'éléments d'infrastructure a impliqué l'organisation à but non lucratif lowRISC, qui supervise le développement d'un microprocesseur libre basé sur l'architecture RISC-V, ainsi que les entreprises Antmicro et VeriSilicon. Le processeur développé par l'organisation lowRISC a été utilisé comme noyau pour la construction de composants matériels dignes de confiance (RoT, Root of Trust). L'entreprise Antmicro a fourni au projet le simulateur Renode, permettant de tester CantripOS et le micro-noyau seL4 sans matériel réel. L'entreprise VeriSilicon a partagé son expérience dans la création de puces et le développement de BSP (Board Support Package).
Source : opennet.ru
