Google anunciou o lanzamento de código aberto do seu proxecto KataOS, que ten como obxectivo crear un sistema operativo seguro para hardware integrado. Os compoñentes do sistema KataOS están escritos en Rust e execútanse sobre o microkernel seL4, que ten unha proba de fiabilidade matemática en sistemas RISC-V, demostrando o cumprimento total das especificacións de código definidas na linguaxe formal. O código do proxecto é de código aberto baixo a licenza Apache 2.0.
O sistema admite plataformas baseadas nas arquitecturas RISC-V e ARM64. A estrutura Renode úsase durante o desenvolvemento para simular seL4 e o entorno KataOS que se executa en hardware. O sistema de hardware e software Sparrow, que combina KataOS con chips seguros baseados na plataforma OpenTitan, proponse como implementación de referencia. Esta solución combina un núcleo do sistema operativo loxicamente verificado con compoñentes de hardware fiables (RoT ou Root of Trust) construídos coa plataforma OpenTitan e a arquitectura RISC-V. Ademais do código KataOS, está previsto que todos os demais compoñentes de Sparrow, incluído o hardware, sexan de código aberto.
A plataforma está a ser desenvolvida tendo en conta o seu uso en chips especializados deseñados para executar aplicacións de aprendizaxe automática e procesamento de datos sensibles que requiren un nivel especial de protección e verificación de fallos. Exemplos destas aplicacións inclúen sistemas que manipulan imaxes humanas e gravacións de voz. O uso da verificación de fiabilidade de KataOS garante que, se unha parte do sistema falla, non se propagará ao resto do sistema, especialmente ao núcleo e aos compoñentes críticos.
A arquitectura seL4 destaca polo seu traslado da xestión de recursos do núcleo ao espazo de usuario e a aplicación dos mesmos mecanismos de control de acceso para estes recursos que para os recursos de usuario. O micronúcleo non proporciona abstraccións de alto nivel predefinidas para xestionar ficheiros, procesos, conexións de rede e similares; en cambio, só proporciona mecanismos mínimos para xestionar o acceso ao espazo de enderezos físicos, interrupcións e recursos do procesador. As abstraccións de alto nivel e os controladores para interactuar co hardware impleméntanse por separado enriba do micronúcleo como tarefas que se executan a nivel de usuario. O acceso aos recursos do micronúcleo por parte destas tarefas organízase mediante a definición de regras.
Para unha protección adicional, todos os compoñentes, agás o microkernel, desenvólvense inicialmente en Rust empregando técnicas de programación seguras que minimizan os erros de memoria que poden levar a problemas como o acceso á memoria despois de que se libere, a desreferencia de punteiros nulos e as sobrecargas do búfer. Rust tamén se usa para o cargador de aplicacións no entorno seL4, os servizos do sistema, o marco de desenvolvemento de aplicacións, a API para acceder ás chamadas do sistema, o xestor de procesos, o mecanismo de asignación dinámica de memoria e outros compoñentes. O kit de ferramentas CAmkES, desenvolvido polo proxecto seL4, úsase para compilacións verificadas. Os compoñentes para CAmkES tamén se poden escribir en Rust.
Rust garante a seguridade da memoria no tempo de compilación mediante a comprobación de referencias, o seguimento da propiedade dos obxectos e a contabilidade do tempo de vida do obxecto (alcance), así como mediante a avaliación da validez do acceso á memoria en tempo de execución. Rust tamén proporciona protección contra desbordamentos de enteiros, require a inicialización obrigatoria dos valores das variables antes do seu uso, implementa o concepto de referencias inmutables e variables predeterminadas e ofrece unha forte tipificación estática para minimizar os erros lóxicos.
Fonte: opennet.ru
