O Google anunciou o lançamento em código aberto do seu projeto KataOS, que visa criar um sistema operacional seguro para hardware embarcado. Os componentes do sistema KataOS são escritos em Rust e executados sobre o microkernel seL4, que possui uma prova matemática de confiabilidade em sistemas RISC-V, demonstrando total conformidade com as especificações de código definidas na linguagem formal. O código do projeto é de código aberto sob a licença Apache 2.0.
O sistema suporta plataformas baseadas nas arquiteturas RISC-V e ARM64. O framework Renode é utilizado durante o desenvolvimento para simular o seL4 e o ambiente KataOS em execução no hardware. O sistema de hardware e software Sparrow, que combina o KataOS com chips seguros baseados na plataforma OpenTitan, é proposto como uma implementação de referência. Esta solução combina um kernel de sistema operacional logicamente verificado com componentes de hardware confiáveis (RoT, ou Raiz de Confiança) construídos utilizando a plataforma OpenTitan e a arquitetura RISC-V. Além do código KataOS, todos os outros componentes do Sparrow, incluindo o hardware, serão disponibilizados como código aberto.
A plataforma está sendo desenvolvida com foco em seu uso em chips especializados, projetados para executar aplicações de aprendizado de máquina e processamento de dados sensíveis que exigem um nível especial de proteção e verificação de falhas. Exemplos dessas aplicações incluem sistemas que manipulam imagens e gravações de voz de pessoas. O uso da verificação de confiabilidade pelo KataOS garante que, se uma parte do sistema falhar, a falha não se propagará para o restante do sistema, principalmente para o kernel e componentes críticos.
A arquitetura seL4 destaca-se por transferir o gerenciamento de recursos do kernel para o espaço do usuário e pela aplicação dos mesmos mecanismos de controle de acesso para esses recursos que para os recursos do usuário. O micronúcleo não fornece abstrações de alto nível prontas para uso para gerenciar arquivos, processos, conexões de rede e similares; em vez disso, oferece apenas mecanismos mínimos para gerenciar o acesso ao espaço de endereçamento físico, interrupções e recursos do processador. Abstrações de alto nível e drivers para interação com o hardware são implementados separadamente sobre o micronúcleo como tarefas executadas em nível de usuário. O acesso aos recursos do micronúcleo por essas tarefas é organizado por meio da definição de regras.
Para proteção adicional, todos os componentes, exceto o micronúcleo, são inicialmente desenvolvidos em Rust usando técnicas de programação seguras que minimizam erros de memória que podem levar a problemas como acesso à memória após sua liberação, desreferenciamento de ponteiros nulos e estouro de buffer. Rust também é usado para o carregador de aplicativos no ambiente seL4, serviços do sistema, framework de desenvolvimento de aplicativos, API para acesso a chamadas de sistema, gerenciador de processos, mecanismo de alocação dinâmica de memória e outros componentes. O kit de ferramentas CAmkES, desenvolvido pelo projeto seL4, é usado para builds verificados. Componentes para o CAmkES também podem ser escritos em Rust.
Rust garante a segurança da memória em tempo de compilação por meio de verificação de referências, rastreamento de propriedade de objetos e contabilização do tempo de vida (escopo) dos objetos, bem como por meio da avaliação da validade do acesso à memória em tempo de execução. Rust também oferece proteção contra estouros de inteiros, exige a inicialização obrigatória de valores de variáveis antes do uso, implementa o conceito de referências imutáveis e variáveis padrão e oferece tipagem estática forte para minimizar erros lógicos.
Fonte: opennet.ru
