La société Google a annoncé l'ouverture des travaux liés au projet KataOS, qui vise à créer un système d'exploitation sécurisé pour le matériel embarqué. Les composants du système KataOS sont écrits en Rust et fonctionnent au-dessus du micro-noyau seL4, pour lequel une preuve mathématique de fiabilité a été fournie sur les systèmes RISC-V, attestant de la conformité totale du code aux spécifications établies dans un langage formel. Le code du projet est ouvert sous la licence Apache 2.0.
Le système prend en charge les plateformes basées sur les architectures RISC-V et ARM64. Pour simuler le fonctionnement de seL4 et de l'environnement KataOS sur le matériel durant le processus de développement, le framework Renode est utilisé. Comme mise en œuvre de référence, un complexe matériel et logiciel appelé Sparrow est proposé, combinant KataOS avec des puces sécurisées basées sur la plateforme OpenTitan. La solution proposée permet de combiner un noyau d'exploitation logiquement vérifié avec des composants matériels digne de confiance (RoT, Root of Trust) construits à l'aide de la plateforme OpenTitan et de l'architecture RISC-V. En plus du code de KataOS, il est prévu d'ouvrir par la suite tous les autres composants de Sparrow, y compris la composante matérielle.
La plateforme est développée en tenant compte de son utilisation dans des puces spécialisées conçues pour exécuter des applications d'apprentissage automatique et de traitement d'informations sensibles, qui nécessitent un niveau de protection particulier et une confirmation de l'absence de défaillances. Comme exemple de telles applications, on cite des systèmes qui manipulent des images de personnes et des enregistrements vocaux. L'utilisation de vérification de fiabilité dans KataOS garantit qu'en cas de défaillance dans une partie du système, cette défaillance ne se propagera pas au reste du système, notamment au noyau et aux parties critiques.
L'architecture seL4 se distingue par le déplacement des parties de gestion des ressources du noyau vers l'espace utilisateur, tout en utilisant 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 prêtes à l'emploi pour la gestion des fichiers, des processus, des connexions réseau, etc., mais se limite à fournir des mécanismes minimaux pour contrôler l'accès à l'espace d'adressage physique, aux interruptions et aux ressources processeur. Les abstractions de haut niveau et les pilotes pour l'interaction avec le matériel sont implémentés séparément au-dessus du micro-noyau sous la forme de tâches s'exécutant 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.
Pour une protection supplémentaire, tous les composants autres que le micro-noyau sont initialement développés en langage Rust en utilisant des techniques de programmation sûres, visant à minimiser les erreurs de gestion de la mémoire, conduisant à des problèmes tels que l'accès à une zone de mémoire après sa libération, la déréférenciation de pointeurs nuls et le dépassement de tampon. En Rust ont notamment été écrits le chargeur d'applications dans l'environnement seL4, les services système, le framework pour le développement d'applications, l'API pour accéder aux appels système, le gestionnaire de processus, le mécanisme de distribution dynamique de la mémoire, etc. Pour la construction vérifiée, l'outil CAmkES, développé par le projet seL4, est utilisé. Les composants pour CAmkES peuvent également être créés en langage Rust.
La gestion sécurisée de la mémoire est assurée en Rust lors de la compilation par la vérification des références, le suivi de la propriété des objets et la prise en compte de la durée de vie des objets (portée), ainsi que par l'évaluation de la validité de l'accès à la mémoire pendant l'exécution du code. Rust fournit également des moyens de se protéger contre les débordements d'entiers, exigeant l'initialisation obligatoire des variables avant leur utilisation, appliquant le concept d'immuabilité (immutable) des références et des variables par défaut, et offrant une forte typage statique pour minimiser les erreurs logiques.
Source : opennet.ru
