Google divulgou o código fonte do projeto KataOS

Kata OS

KataOS, um sistema operacional orientado à segurança de hardware embarcado.

Foi divulgada a notícia de que O Google anunciou o lançamento do código-fonte do desenvolvimentos relacionados ao projeto Kata OS, cujo objetivo é criar um sistema operacional seguro para hardware embarcado.

O sistema fornece suporte para plataformas baseadas em arquiteturas RISC-V e ARM64. Para simular o funcionamento do seL4 e do ambiente KataOS no hardware durante o desenvolvimento, é utilizado o framework Renode.

Como implementação de referência, é proposto o complexo de software e hardware Sparrow, que combina o KataOS com chips seguros baseados na plataforma OpenTitan. A solução proposta hÉ possível combinar um kernel sistema operacional verificado logicamente com componentes de hardware Root of Trust (RoT) 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.

Como base para este novo sistema operacional, escolhemos o seL4 como o microkernel porque ele coloca a segurança na frente e no centro; é matematicamente comprovado como seguro, com garantia de confidencialidade, integridade e disponibilidade. Por meio da estrutura seL4 CAmkES, também podemos fornecer componentes de sistema definidos estaticamente e analisáveis. O KataOS fornece uma plataforma segura verificável que protege a privacidade do usuário porque é logicamente impossível que os aplicativos violem as proteções de segurança do hardware do kernel e os componentes do sistema seguro verificáveis.

A plataforma está sendo desenvolvida com chips em mente especialmente projetado para executar aplicativos de privacidade e aprendizado de máquina que requerem um nível específico de proteção e garantem que não haja falhas. Sistemas que manipulam imagens de pessoas e gravações de voz são dados como exemplo de tais aplicações. 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 resto do sistema e, em particular, para o kernel e partes críticas.

A arquitetura seL4 se destaca em partes móveis para gerenciar recursos do kernel no espaço do usuário e aplique os mesmos controles de acesso para esses recursos e para os recursos do usuário.

O microkernel não fornece abstrações de alto nível pronto para usar para gerenciar arquivos, processos, conexões de rede e similares, mas 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 de alto nível e drivers para interagir com o hardware são implementados separadamente em cima do microkernel na forma de tarefas de nível de usuário. O acesso de tais tarefas aos recursos disponíveis no microkernel é organizado por meio da definição de regras.

Para proteção extra, todos os componentes, exceto o microkernel, são inicialmente desenvolvidos em Rust usando técnicas de programação seguras que minimizam erros ao trabalhar com memória, levando a problemas como acessar uma área de memória após liberá-la, desreferenciar ponteiros nulos e estouro de buffer.

O carregador de aplicativos no ambiente seL4, serviços do sistema, uma estrutura de desenvolvimento de aplicativos, uma API para acessar chamadas do sistema, um gerenciador de processos, um mecanismo de alocação dinâmica de memória, etc. eles são escritos em Rust. Para a montagem verificada, é utilizado o kit de ferramentas CAmkES desenvolvido pelo projeto seL4. Componentes para CAmkES também podem ser criados em Rust.

A segurança da memória é fornecida no Rust em tempo de compilação verificando referências, rastreando a propriedade do objeto e o tempo de vida do objeto (escopo), bem como avaliando a correção do acesso à memória durante a execução do código. Rust também fornece proteção contra estouro de inteiros, requer que as variáveis ​​sejam inicializadas antes do uso, reforça o conceito de variáveis ​​e referências imutáveis ​​por padrão e fornece tipagem estática forte para minimizar erros de lógica.

Finalmente, para os interessados, deve saber que os componentes do sistema KataOS são escritos em Rust e executados no microkernel seL4, para o qual é fornecida uma prova matemática de confiabilidade em sistemas RISC-V, indicando que o código atende totalmente às especificações especificado na linguagem formal.

O código do projeto está aberto sob a licença Apache 2.0, você pode consultar mais detalhes sobre ele no link a seguir


Seja o primeiro a comentar

Deixe um comentário

Seu endereço de email não será publicado. Campos obrigatórios são marcados com *

*

*

  1. Responsável pelos dados: Miguel Ángel Gatón
  2. Finalidade dos dados: Controle de SPAM, gerenciamento de comentários.
  3. Legitimação: Seu consentimento
  4. Comunicação de dados: Os dados não serão comunicados a terceiros, exceto por obrigação legal.
  5. Armazenamento de dados: banco de dados hospedado pela Occentus Networks (UE)
  6. Direitos: A qualquer momento você pode limitar, recuperar e excluir suas informações.