Google anunciou o descubrimento de desenvolvementos relacionados co proxecto KataOS, destinado a crear un sistema operativo seguro para hardware integrado. Os compoñentes do sistema KataOS están escritos en Rust e execútanse sobre o micronúcleo seL4, para o que se proporciona unha proba matemática de fiabilidade nos sistemas RISC-V, que indica o cumprimento total do código coas especificacións especificadas na linguaxe formal. O código do proxecto está aberto baixo a licenza Apache 2.0.
O sistema ofrece soporte para plataformas baseadas en arquitecturas RISC-V e ARM64. Para simular o funcionamento de seL4 e do ambiente KataOS enriba do hardware, úsase o marco Renode durante o desenvolvemento. Como implementación de referencia, proponse o sistema de hardware e software Sparrow, que combina KataOS con chips seguros baseados na plataforma OpenTitan. A solución proposta permite combinar un núcleo de sistema operativo loxicamente verificado con compoñentes de hardware fiables (RoT, Root of Trust) construídos mediante a plataforma OpenTitan e a arquitectura RISC-V. Ademais do código KataOS, está previsto abrir todos os outros compoñentes de Sparrow, incluído o de hardware, no futuro.
A plataforma está a ser desenvolvida pensando en chips especialmente deseñados para executar aplicacións de aprendizaxe automática e privacidade que requiren un nivel específico de protección e garantía de que non haxa fallos. Os sistemas que manipulan imaxes de persoas e gravacións de voz son un exemplo deste tipo de aplicacións. O uso da verificación de fiabilidade en KataOS garante que, en caso de falla nunha parte do sistema, esta falla non se estenda ao resto do sistema e, en particular, ao núcleo e ás partes críticas.
A arquitectura seL4 destaca por mover partes para xestionar os recursos do núcleo no espazo do usuario e aplicar os mesmos controis de acceso para tales recursos que para os recursos do usuario. O micronúcleo non ofrece abstraccións de alto nivel listas para xestionar ficheiros, procesos, conexións de rede e similares, senón que ofrece só mecanismos mínimos para controlar 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 impléntanse por separado encima do micronúcleo en forma de tarefas a nivel de usuario. O acceso destas tarefas aos recursos dos que dispón o micronúcleo organízase mediante a definición de regras.
Para unha protección adicional, todos os compoñentes excepto o micronúcleo desenvólvense inicialmente en Rust utilizando técnicas de programación seguras que minimizan os erros ao traballar coa memoria, o que provoca problemas como acceder a unha área de memoria despois de liberarse, desreferenciar os punteiros nulos e exceder o búfer. O cargador de aplicacións no contorno seL4, os servizos do sistema, un marco de desenvolvemento de aplicacións, unha API para acceder ás chamadas do sistema, un xestor de procesos, un mecanismo de asignación de memoria dinámica, etc. están escritos en Rust. Para a montaxe verificada utilízase o kit de ferramentas CAmkES desenvolvido polo proxecto seL4. Tamén se poden crear compoñentes para CAmkES en Rust.
A seguridade da memoria ofrécese en Rust no momento da compilación mediante a comprobación de referencias, o seguimento da propiedade do obxecto e a súa vida útil (alcance), así como a través da avaliación da corrección do acceso á memoria durante a execución do código. Rust tamén ofrece protección contra os desbordamentos de números enteiros, require que as variables se inicialicen antes do seu uso, aplica o concepto de referencias e variables inmutables por defecto e ofrece unha forte escritura estática para minimizar os erros lóxicos.
Fonte: opennet.ru