Google a annoncé la découverte de développements liés au projet KataOS, visant à 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 exécutés sur le micro-noyau seL4, pour lequel une preuve mathématique de fiabilité a été fournie sur les systèmes RISC-V, indiquant que le code est entièrement conforme aux spécifications spécifiées dans le langage formel. Le code du projet est ouvert sous la licence Apache 2.0.
Le système prend en charge les plates-formes basées sur les architectures RISC-V et ARM64. Pour simuler le fonctionnement de seL4 et de l'environnement KataOS au-dessus du matériel, le framework Renode est utilisé pendant le processus de développement. Comme implémentation de référence, le complexe logiciel et matériel Sparrow est proposé, combinant KataOS avec des puces sécurisées basées sur la plateforme OpenTitan. La solution proposée vous permet de combiner un noyau de système d'exploitation logiquement vérifié avec des composants matériels fiables (RoT, Root of Trust), construits à l'aide de la plateforme OpenTitan et de l'architecture RISC-V. En plus du code KataOS, il est prévu d'ouvrir à l'avenir tous les autres composants Sparrow, y compris le composant matériel.
La plate-forme est développée en vue d'une application dans des puces spécialisées conçues pour exécuter des applications d'apprentissage automatique et de traitement d'informations confidentielles, qui nécessitent un niveau particulier de protection et de confirmation de l'absence de pannes. Des exemples de telles applications incluent les systèmes qui manipulent des images de personnes et des enregistrements vocaux. L'utilisation par KataOS de la vérification de la fiabilité garantit que si une partie du système tombe en panne, la panne ne se propagera pas au reste du système et, en particulier, au noyau et aux parties critiques.
L'architecture seL4 se distingue par le déplacement des éléments permettant de gérer les ressources du noyau dans l'espace utilisateur et par l'application des mêmes outils 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 ne fournit que des mécanismes minimaux pour contrôler l'accès à l'espace d'adressage physique, aux interruptions et aux ressources du 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 la forme de tâches au niveau de l'utilisateur. L'accès de ces tâches aux ressources dont dispose le micronoyau est organisé à travers la définition de règles.
Pour une protection supplémentaire, tous les composants, à l'exception du micro-noyau, sont développés nativement dans Rust à l'aide de techniques de programmation sécurisées qui minimisent les erreurs de mémoire entraînant des problèmes tels que l'accès à la mémoire après la libération, les déréférences de pointeurs nuls et les dépassements de tampon. Un chargeur d'applications dans l'environnement seL4, des services système, un framework de développement d'applications, une API d'accès aux appels système, un gestionnaire de processus, un mécanisme d'allocation dynamique de mémoire, etc. ont été écrits en Rust. Pour l'assemblage vérifié, la boîte à outils CAmkES, développée par le projet seL4, est utilisée. Les composants pour CAmkES peuvent également être créés dans Rust.
Rust assure la sécurité de la mémoire au moment de la compilation grâce à la vérification des références, à la propriété des objets et au suivi de la durée de vie des objets (portées), et en évaluant l'exactitude des accès à la mémoire au moment de l'exécution. Rust offre également une protection contre les débordements d'entiers, nécessite que les valeurs des variables soient initialisées avant utilisation, utilise le concept de références et de variables immuables par défaut et propose un typage statique fort pour minimiser les erreurs logiques.
Source: opennet.ru