A Google anunciou a abertura de desenvolvimentos relacionados ao projeto KataOS, que visa criar um sistema operacional seguro para equipamentos embarcados. Os componentes do sistema KataOS são escritos na linguagem Rust e executados sobre o microkernel seL4, para o qual foi fornecida uma prova matemática de confiabilidade em sistemas RISC-V, atestando a conformidade total do código com as especificações definidas em uma linguagem formal. O código do projeto é aberto sob a licença Apache 2.0.
O sistema oferece suporte a plataformas baseadas nas arquiteturas RISC-V e ARM64. Para simular a operação do seL4 e do ambiente KataOS sobre o hardware durante o desenvolvimento, utiliza-se o framework Renode. Como implementação de referência, foi proposto um complexo software-hardware chamado Sparrow, que combina o KataOS com chips seguros baseados na plataforma OpenTitan. A solução proposta permite unir um núcleo de sistema operacional logicamente verificado a componentes de hardware confiáveis (RoT, Root of Trust), construídos utilizando a plataforma OpenTitan e a arquitetura RISC-V. Além do código KataOS, planeja-se abrir todos os demais componentes do Sparrow, incluindo a parte de hardware.
A plataforma está sendo desenvolvida com foco na aplicação em chips especializados, voltados para a execução de aplicativos para aprendizado de máquina e processamento de informações confidenciais, que requerem um nível especial de proteção e garantia de ausência de falhas. Exemplos de tais aplicativos incluem sistemas que manipulam imagens de pessoas e gravações de voz. O uso da verificação de confiabilidade no KataOS garante que, em caso de falha em uma parte do sistema, essa falha não se espalhe para o restante do sistema e, em particular, para o núcleo e partes críticas.
A arquitetura seL4 é notável por mover partes do gerenciamento de recursos do núcleo para o espaço do usuário e aplicar os mesmos meios de separação de acesso a esses recursos como 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, etc.; em vez disso, ele oferece apenas mecanismos mínimos para gerenciar o acesso ao espaço de endereço físico, interrupções e recursos da CPU. Abstrações de alto nível e drivers para interagir com hardware são implementados separadamente sobre o microkernel, na forma de tarefas executadas em nível de usuário. O acesso dessas tarefas aos recursos disponíveis no microkernel é organizado através da definição de regras.
Para proteção adicional, todos os componentes, exceto o microkernel, são inicialmente desenvolvidos na linguagem Rust, utilizando práticas de programação seguras que minimizam erros de manipulação de memória, como o acesso à memória após a liberação, desreferenciamento de ponteiros nulos e estouros de buffer. O carregador de aplicativos no ambiente seL4, serviços do sistema, uma estrutura para desenvolvimento de aplicativos, APIs para acesso a chamadas do sistema, gerenciador de processos, mecanismo de alocação dinâmica de memória, etc., também são escritos em Rust. Para uma construção verificada, é utilizada a ferramenta CAmkES, desenvolvida pelo projeto seL4. Componentes para CAmkES também podem ser criados na linguagem Rust.
O trabalho seguro com a memória em Rust é garantido durante a compilação através da verificação de referências, rastreamento da posse de objetos e consideração do tempo de vida dos objetos (escopos), bem como pela avaliação da correção do acesso à memória durante a execução do código. Rust também oferece meios para proteção contra estouros inteiros, exige a inicialização obrigatória de valores de variáveis antes de seu uso, aplica o conceito de imutabilidade (immutable) para referências e variáveis por padrão e oferece uma forte tipagem estática para minimizar erros lógicos.
Fonte: opennet.ru
