Introdução ao microkernel seL4 [PDF]

• seL4 é um microkernel de SO que executa em modo kernel com o mínimo de código, controlando recursos de hardware e reforçando a segurança
• Pertence à família de microkernels L4 e vem sendo desenvolvido desde meados dos anos 1990
• Pode operar como hipervisor, permitindo executar sistemas convidados como Linux
• É o primeiro kernel de SO do mundo com correção funcional comprovada, com a prova matemática concluída no nível do código
• Usa um modelo de segurança baseado em Capability para controle de acesso granular

Estrutura do seL4 e recursos de hipervisor

• Kernel monolítico vs. microkernel
  • Kernel monolítico (Linux etc.): o código do kernel é enorme e tem muitas vulnerabilidades de segurança → cerca de 20 milhões de linhas de código (20M SLOC)
  • Microkernel (seL4): usa o mínimo de código de kernel → cerca de 10 mil linhas de código (10K SLOC)
  • Redução do tamanho do kernel → mais segurança e menor superfície de ataque
• O seL4 atua como hipervisor
  • É possível executar um sistema convidado completo, como Linux, em uma VM
  • Cada VM roda de forma independente, sem interferência mútua → forte garantia de isolamento
  • Chamadas de procedimento protegidas (PPC) → comunicação segura entre VMs

Verificação e modelo de segurança do seL4

• Verificação de correção funcional
  • O seL4 provou matematicamente, no nível do código, que suas funções estão corretas
  • Garante que todo o comportamento do kernel segue a especificação
• Validação de tradução (Translation Validation)
  • Comprova que o código binário gerado pelo compilador corresponde exatamente ao código C original
  • Executado por meio de uma cadeia de ferramentas automatizada
• Verificação de propriedades de segurança
  • Confidencialidade: os dados só podem ser acessados quando isso for explicitamente permitido
  • Integridade: os dados só podem ser modificados quando isso for explicitamente permitido
  • Disponibilidade: os recursos só podem ser usados quando isso for explicitamente permitido

Modelo de segurança baseado em Capability

• O que é Capability?
  • Um token de segurança que concede permissão de acesso a um objeto específico
  • Codifica junto a referência ao objeto e os direitos de acesso
  • Permite controle de acesso detalhado → aplicação do princípio do menor privilégio (Principle of Least Privilege, POLA)
• Vantagens de Capability
  • Controle de acesso granular → é possível minimizar privilégios
  • Permite delegação e revogação de permissões
  • Modelo de segurança robusto → superior ao modelo tradicional de controle de acesso (ACL)
• Resolução do problema do confused deputy
  • Em sistemas tradicionais baseados em ACL, o estado de segurança é determinado pelo ID de segurança do sujeito
  • No seL4, a Capability determina diretamente as permissões de segurança → controle de permissões mais claro

Suporte a sistemas de tempo real e sistemas de criticidade mista

• Suporte a sistemas de tempo real
  • O seL4 oferece escalonamento baseado em prioridade
  • A análise do pior tempo de execução (WCET) de todas as operações do kernel já foi concluída → garantia de tempo real rígido
• Suporte a sistemas de criticidade mista (Mixed-Criticality System, MCS)
  • Alocação e isolamento de recursos de CPU com base em contextos de escalonamento
  • Controla para que tarefas de alta prioridade não monopolizem a CPU
  • Permite executar simultaneamente tarefas críticas e não críticas

Desempenho e eficiência

• O microkernel de mais alto desempenho
  • Não reduz a segurança mesmo quando o desempenho é essencial
  • O custo de chamadas de sistema e IPC é minimizado → mais de 5 vezes mais rápido que sistemas concorrentes
• Desempenho superior em relação a sistemas concorrentes
  • Fiasco.OC: cerca de 2 vezes mais lento que o seL4
  • Zircon: cerca de 9 vezes mais lento que o seL4
  • CertiKOS: cerca de 5 vezes mais lento que o seL4

Aplicação no mundo real e cyber retrofit

• Casos de uso reais

  • Foi aplicado com sucesso no ULB (helicóptero não tripulado) da Boeing
  • Foi confirmado o reforço da segurança e o aumento da estabilidade do sistema

• Reforço gradual de segurança em sistemas existentes (Incremental Cyber Retrofit)

  • Executa sistemas existentes em VMs enquanto os modulariza gradualmente
  • Reforça a segurança e minimiza a perda de desempenho

Conclusão

• O seL4 é o microkernel mais seguro do mundo, com correção funcional, segurança e desempenho comprovados
• Com um modelo de segurança verificado e suporte a sistemas de criticidade mista, pode ser usado de forma prática em diversas áreas
• É possível reforçar a segurança e melhorar o desempenho de sistemas existentes → um microkernel inovador que equilibra segurança e desempenho