O Google anunciou a descoberta de desenvolvimentos relacionados ao projeto KataOS, que visa criar um sistema operacional seguro para hardware embarcado. Os componentes do sistema KataOS são escritos em Rust e executados no microkernel seL4, para o qual uma prova matemática de confiabilidade foi fornecida em sistemas RISC-V, indicando que o código está em total conformidade com as especificações especificadas na linguagem formal. O código do projeto está aberto sob a licença Apache 2.0.
O sistema oferece suporte para plataformas baseadas nas arquiteturas RISC-V e ARM64. Para simular o funcionamento do seL4 e do ambiente KataOS no hardware, o framework Renode é utilizado durante o processo de desenvolvimento. Como implementação de referência, é proposto o complexo de software e hardware Sparrow, combinando KataOS com chips seguros baseados na plataforma OpenTitan. A solução proposta permite combinar um kernel de sistema operacional verificado logicamente com componentes de hardware confiáveis (RoT, Root of Trust), construídos usando a plataforma OpenTitan e a arquitetura RISC-V. Além do código KataOS, está planejado abrir todos os outros componentes do Sparrow, incluindo o componente de hardware, no futuro.
A plataforma está sendo desenvolvida pensando na aplicação em chips especializados projetados para rodar aplicações de aprendizado de máquina e processamento de informações confidenciais, que exigem nível especial de proteção e confirmação de ausência de falhas. Exemplos de tais aplicações incluem sistemas que manipulam imagens de pessoas e gravações de voz. O uso da verificação de confiabilidade pelo KataOS garante que, se uma parte do sistema falhar, a falha não se espalhará para o resto do sistema e, em particular, para o kernel e partes críticas.
A arquitetura seL4 é notável por mover partes para gerenciar recursos do kernel para o espaço do usuário e aplicar as mesmas ferramentas de controle de acesso para esses recursos e para recursos do usuário. O microkernel não fornece abstrações de alto nível prontas para gerenciar arquivos, processos, conexões de rede e similares; em vez disso, ele fornece apenas mecanismos mínimos para controlar o acesso ao espaço de endereço físico, interrupções e recursos do processador. Abstrações e drivers de alto nível para interação com o hardware são implementados separadamente no microkernel na forma de tarefas no nível do usuário. O acesso de tais tarefas aos recursos disponíveis ao microkernel é organizado através da definição de regras.
Para proteção adicional, todos os componentes, exceto o microkernel, são desenvolvidos nativamente em Rust usando técnicas de programação seguras que minimizam erros de memória que levam a problemas como acesso à memória após liberação, desreferências de ponteiro nulo e saturação de buffer. Um carregador de aplicativos no ambiente seL4, serviços de sistema, uma estrutura para desenvolvimento de aplicativos, uma API para acessar chamadas de sistema, um gerenciador de processos, um mecanismo para alocação dinâmica de memória, etc. Para a montagem verificada, é utilizado o kit de ferramentas CAmkES, desenvolvido pelo projeto seL4. Componentes para CAmkES também podem ser criados em Rust.
Rust reforça a segurança da memória em tempo de compilação por meio de verificação de referência, propriedade de objeto e rastreamento de vida útil do objeto (escopos) e avaliando a correção dos acessos à memória em tempo de execução. Rust também fornece proteção contra estouros de inteiros, requer que os valores das variáveis sejam inicializados antes do uso, usa o conceito de referências e variáveis imutáveis por padrão e oferece tipagem estática forte para minimizar erros lógicos.
Fonte: opennet.ru