Introdução ao microkernel seL4 [PDF]
(sel4.systems)- seL4 é um microkernel de SO voltado a sistemas embarcados e ciberfísicos em que segurança e safety são cruciais, isolando e multiplexando recursos de hardware, mas não sendo um SO de uso geral completo
- Reduz o código em modo kernel para cerca de 10 kSLOC, diminuindo a TCB e a superfície de ataque, enquanto empurra serviços de SO como sistema de arquivos, rede e drivers para o modo usuário
- É o primeiro kernel de SO do mundo com verificação formal em nível de código e, em sistemas configurados corretamente, o kernel garante até propriedades de segurança como confidencialidade, integridade e disponibilidade
- Combina controle de acesso baseado em capability, análise de WCET, suporte a sistemas de tempo real de criticidade mista e funções de hipervisor para tratar ao mesmo tempo de isolamento fino e tempo real
- A API do seL4 é de nível muito baixo, então é difícil construir sistemas complexos diretamente, e quando uma arquitetura estática faz sentido, usar frameworks como o Microkit é a abordagem mais realista
Escopo do seL4
- seL4 é um microkernel, a parte central de baixo nível de um sistema operacional
- O SO controla o hardware e os recursos no modo kernel, o modo de execução de maior privilégio do processador
- As aplicações rodam em modo usuário e só acessam o hardware das formas permitidas pelo SO
- Um microkernel é o núcleo do SO que minimiza o código executado com altos privilégios
- O seL4 pertence à família de microkernels L4, cuja origem remonta até meados da década de 1990
- O seL4 não tem relação com o seLinux
- O seL4 não é um SO completo, mas um kernel de baixo nível que multiplexa e isola recursos de hardware com segurança
- Serviços comuns de SO, como sistema de arquivos, pilha de rede e drivers de dispositivo, não ficam dentro do kernel
- Esses serviços precisam ser fornecidos como programas em modo usuário
Estrutura de microkernel e redução da superfície de ataque
- Kernels monolíticos como o Linux fornecem serviços de SO, como armazenamento de arquivos e rede, como código em modo kernel
- Como o código em modo kernel pode acessar os recursos do sistema sem restrições, bugs que levem a escalonamento de privilégio ou execução arbitrária de código podem comprometer o sistema inteiro
- O kernel Linux tem cerca de 20 MSLOC, e estima-se que possa conter dezenas de milhares de bugs
- Microkernels bem projetados como o seL4 reduzem o código em modo kernel para algo em torno de 10 kSLOC
- Isso o torna três ordens de grandeza menor que o kernel Linux
- Com a redução da TCB, a superfície de ataque também diminui
- A maior parte dos serviços do SO sai de dentro do kernel, e o microkernel passa a agir como uma camada fina em torno do hardware
- As funções centrais oferecidas são isolamento entre programas e um mecanismo seguro de chamadas
- Os serviços deixam de rodar dentro do kernel e passam a ser programas em modo usuário executados em sandboxes separadas
- Em um estudo que analisou casos conhecidos de comprometimento crítico no Linux, a arquitetura de microkernel conseguiu eliminar completamente 29% deles e mitigar mais 55% a ponto de não serem mais classificados como críticos
PPC, capability e controle fino de permissões
- O seL4 fornece um mecanismo de PPC (protected procedure call)
- Por razões históricas, o termo IPC ainda permanece, mas essa expressão pode gerar mal-entendidos e levar a designs ruins
- O PPC permite que um programa chame com segurança a função de outro programa em uma sandbox diferente
- O microkernel transporta entrada e saída no PPC e impõe a interface
- Funções remotas só podem ser chamadas pelos pontos de entrada exportados
- Apenas clientes explicitamente autorizados, que tenham recebido a capability apropriada, podem fazer chamadas
- Uma capability é um token de acesso que permite acessar um recurso específico do sistema
- Ela permite controlar com grande granularidade quais entidades podem acessar quais recursos
- Dá suporte ao princípio do menor privilégio, ou POLA
- Os mecanismos de controle de acesso usados em sistemas convencionais como Linux e Windows não permitem atingir esse nível de menor privilégio
- O seL4 é o único SO do mundo que combina modelo baseado em capability com verificação formal, e essa combinação é vista como base para a afirmação defensável de que ele é o SO mais seguro do mundo
Verificação formal e garantias de segurança
- O seL4 fornece provas formais, matemáticas e verificadas por máquina da correção da implementação
- Essas provas significam que, em um sentido muito forte em relação à especificação, o kernel é “livre de bugs”
- O seL4 é o primeiro kernel de SO do mundo com esse tipo de prova em nível de código
- Além da correção da implementação, o seL4 também fornece provas adicionais de imposição de segurança
- Em sistemas baseados em seL4 configurados corretamente, o kernel garante confidencialidade, integridade e disponibilidade
- A cadeia de verificação é o principal diferencial do seL4
- Em sistemas críticos de segurança e safety, o kernel só pode servir como base de confiança se houver fortes garantias tanto sobre a implementação quanto sobre as propriedades de segurança
Tempo real e sistemas de criticidade mista
- O seL4 é um kernel de SO submetido a uma análise completa e sólida de WCET (worst-case execution time)
- Quando o kernel é configurado adequadamente, todas as operações do kernel têm limite temporal
- E esse limite é conhecido
- Essas propriedades são pré-requisitos para construir sistemas hard real-time
- Voltados a sistemas em que falhar em responder a um evento dentro de um tempo estritamente limitado pode ser catastrófico
- O seL4 também oferece suporte a MCS (mixed-criticality systems)
- Voltados a ambientes em que é preciso garantir a temporalidade de atividades importantes mesmo quando código menos confiável roda na mesma plataforma
- Ao contrário do particionamento rígido e pouco flexível de tempo e espaço usado por SOs tradicionais de MCS, o seL4 oferece um modelo flexível que preserva o aproveitamento de recursos
Usando o seL4 como hipervisor
- O seL4 é ao mesmo tempo um microkernel e um hipervisor
- É possível rodar máquinas virtuais sobre o seL4
- Dentro dessas máquinas virtuais, é possível executar sistemas convidados comuns como Linux
- Guests e aplicações podem se comunicar entre si conforme os canais de comunicação impostos pelo seL4
- Também é possível se comunicar com aplicações nativas
- Uma VM Linux pode ser usada como meio de fornecer serviços ao sistema
- Em uma configuração de exemplo, serviços como rede e armazenamento são obtidos a partir de várias instâncias Linux executadas em VMs separadas
Como construir sistemas sobre o seL4
- A API do seL4 é de nível muito baixo, mesmo em comparação com outros microkernels
- Ela oferece apenas as abstrações mínimas necessárias para gerenciar o hardware com segurança
- O seL4 é comparado a uma “linguagem assembly dos sistemas operacionais”
- Não é adequado construir sistemas complexos diretamente sobre o seL4
- Frameworks de mais alto nível devem permitir focar no código de implementação dos serviços e automatizar a complexidade do hardware e a integração do sistema
- O ecossistema do seL4 tem três principais frameworks open source de componentes
- Microkit: simplifica a API do seL4 com um pequeno conjunto de abstrações centradas em protection domains e fornece um SDK que integra módulos compilados separadamente e o binário do kernel para gerar imagens inicializáveis
- CAmkES: é o predecessor do Microkit e um framework de componentes para sistemas de arquitetura estática, mas sem SDK, com processo de build mais incômodo e maior overhead
- Genode: suporta vários microkernels e tem muitos serviços e drivers para plataformas x86, sem impor arquitetura estática, mas não consegue aproveitar todos os recursos de segurança e safety do seL4 e não oferece uma história de garantias
- Desde que uma arquitetura estática atenda aos requisitos, o Microkit é a opção recomendada para construir sistemas baseados em seL4
- Arquitetura estática é um modelo em que o conjunto de módulos e a estrutura de comunicação são definidos no momento da configuração do sistema
- Considera-se que esse modelo atende às necessidades da maioria dos sistemas embarcados, incluindo sistemas ciberfísicos complexos como automóveis e aeronaves
1 comentários
Opiniões no Hacker News
O seL4 em si já é uma história antiga, mas fico curioso se foram adicionadas novas camadas ou componentes formalmente verificados além do microkernel.
Também parece haver pessoas que, ao verem a palavra “prova”, ficam emocionalmente sobrecarregadas e param de raciocinar. Verificação formal não é uma panaceia que resolve o problema infinito de uma TI segura, nem um método para produzir software absolutamente perfeito.
Pelo que entendo, é uma prova de que determinados requisitos são satisfeitos sob determinadas condições, e esses requisitos e condições podem ser bem estreitos; fora das funcionalidades e condições especificadas, ela não diz nada. Estou mais ou menos certo?
Do ponto de vista prático, também fico curioso sobre o que um especialista em segurança espera ao ver “software formalmente verificado”. Parece que a informação central aqui é qual especificação o seL4 satisfaz.
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
Também há vários bugs relacionados a memória no rastreador de issues.
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Curiosamente, o PR que corrigiu o “register clobbering” de memória não recebeu o rótulo bug, então não aparece ao filtrar por “bug”. Antes eu achava que, graças às provas, o seL4 era imune a esse tipo de problema; depois de ver isso, passei a entender que as provas não são tão abrangentes quanto a comunidade passou a acreditar. Ainda assim, o seL4 continua sendo um software muito impressionante.
Respondendo à pergunta, a especificação que o seL4 satisfaz está pública no GitHub.
https://github.com/seL4/l4v
O escalonamento de criticalidade mista oferece acesso baseado em capabilities ao tempo de CPU, limites superiores para execução de threads, garantia de prioridade e acesso a recursos para tarefas de alta criticalidade, e “passive servers” que rodam com tempo de escalonamento doado pelo chamador.
O Microkit é uma camada de abstração verificada que torna muito mais fácil construir sistemas reais sobre o seL4, e o Device Driver Framework fornece templates de drivers de dispositivo, implementações dos planos de controle/dados e ferramentas para escrever drivers e virtualizar dispositivos para I/O de alto desempenho no seL4.
A verificação formal pode garantir que determinados requisitos valem sob determinadas condições. Em geral, é verdade que esses requisitos e condições podem ser estreitos, mas o próprio seL4 tem muitas provas que tratam de uma gama ampla de propriedades que se esperaria de um kernel, e essas garantias valem mesmo sob pressupostos muito fracos. Nem mesmo se assume a correção do compilador C: há uma ferramenta separada que examina a saída do compilador e prova que o binário compilado se comporta de acordo com a semântica C exigida.
Entre os requisitos satisfeitos pelo seL4 está o de que o código binário do kernel seL4 implementa exatamente o comportamento descrito na especificação abstrata, e nada além disso. Não há buffer overflow, vazamento de memória, erro de ponteiro, dereferência de ponteiro nulo, comportamento indefinido no código C, nem encerramento do kernel exceto pelos métodos explícitos enumerados na especificação.
A especificação e o binário do seL4 também satisfazem propriedades de segurança de integridade e confidencialidade. Integridade significa que um processo não tem nenhuma forma de alterar dados para os quais não possui permissão explícita, e confidencialidade significa que dados não autorizados não podem ser lidos de nenhuma forma. Também é mostrado que não é possível inferir dados indiretamente por determinados canais laterais. Além da segurança, também são atendidas garantias de pior tempo de execução esperado e propriedades de escalonamento.
O trabalho atual está mais voltado para uma adoção mais ampla, com o LionsOS: https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
Usa bastante programação em nível de tipos para rastrear recursos, acesso ao hardware e capabilities em tempo de compilação. Como descobrir e depurar problemas em runtime é péssimo demais, é uma tentativa de elevar parte das garantias do kernel de base para o lado do compilador.
Gosto de hosts de microkernel que rodam kernels monolíticos convidados, então meus servidores rodam seL4 como camada de segurança e backup para VMs FreeBSD, e dentro delas uso jails para renderfarm, clusters BEAM e Jenkins.
O que é uma pena é não haver um port para ARM do threading e do kernel interno a processos do DragonflyBSD, ou seja, de seu design de kernel híbrido. O sonho é rodar o OpenMoonRay de forma mais eficiente em um Ampere Altra de 128 núcleos.
Hoje, a própria discussão pró/contra microkernels parece estar perdendo muito do sentido. A única forma de acessar serviços privilegiados de maneira rápida, eficiente e segura são mitigações em hardware, e há limites para o que o software pode fazer
É parecido com a diferença entre o 80286 e o 80386. Este último acrescentou suporte de hardware para multitarefa real, que o primeiro não tinha. Desde então, os mecanismos de proteção em nível de hardware, como os que possibilitaram hipervisores, continuaram aumentando
A Apple, em especial, vem colocando em seus SoCs muitos recursos que protegem o kernel, drivers e componentes no nível do chip e impõem privilégios ao usar threads em execução e ponteiros. https://support.apple.com/guide/security/operating-system-in...
Isso não quer dizer que o OS seja inviolável, mas é muito mais eficaz do que uma estratégia de gerenciar privilégios apenas por software. Ao usar esses recursos, ou algo semelhante, a estrutura do kernel parece deixar de ser tão importante; fico curioso para saber se estou errado
Também há muito a aprender com sistemas micro/híbridos mais composáveis. Por exemplo, o Plan 9 é um excelente sistema híbrido que expõe todos os objetos do sistema ao espaço de usuário por meio de um único protocolo, o 9P. Ele é híbrido porque algumas partes, como IP ou TLS, ficam dentro do kernel para evitar o overhead de chamadas de sistema
Outro aspecto interessante do projeto é que os drivers dentro do kernel são, em geral, uma forma mínima que serve apenas como uma interface 9P para a lógica de hardware. Isso transforma objetos de máquina, como ponteiros ou registros, em arquivos navegáveis, protege esses arquivos com permissões Unix padrão e permite distribuir componentes facilmente por várias máquinas pela rede. Como resultado, a lógica dos drivers pode ser movida com segurança para programas em espaço de usuário
O 9P é transparente em relação à rede e à arquitetura, então máquinas diferentes, como Arm, x86, mips etc., podem trabalhar juntas diretamente. Voltar do Plan 9 para Linux/Unix ou Windows é triste e frustrante. A flexibilidade é quase do nível de rocha ígnea, e recursos são anexados de forma incompatível entre si por meio de inúmeros protocolos que fazem a mesma coisa: servir arquivos/objetos
Do ponto de vista prático de engenharia, kernels monolíticos eram mais rápidos e fáceis, tinham mais recursos, e a segurança era o que era possível em C: melhor esforço e uma montanha de bugs. Muito hardware foi introduzido para mitigar essa bagunça. Mas, com o SeL4, em teoria talvez não seja necessário um coprocessador de segurança, porque há um grau muito alto de confiança no isolamento entre processos e na ausência de exploits de nível root. Portanto, o codesign de hardware/software é importante
Ainda assim, a equipe do SeL4 também teve de gastar muitos recursos de engenharia para eliminar canais laterais no hardware. O mundo real não se importa com simulações físicas, então o hardware também tem falhas
A vantagem do microkernel aqui é que ele é pequeno o bastante para a verificação formal conseguir lidar com ele. A própria prova tem 10 vezes o tamanho do kernel. A troca de contexto do SeL4 é uma ordem de grandeza mais rápida que a do Linux, então o impacto no desempenho deveria ser desprezível. Mas, se fosse possível verificar magicamente um kernel monolítico de milhões de linhas, não fazer troca de contexto ainda seria mais rápido. Na prática, a equipe do SeL4 tentou mover o escalonador para o espaço de usuário, mas o custo de desempenho era alto demais, então ele ficou dentro do kernel e foi acrescentado ao ônus da prova
Na verdade, o papel principal do hardware é aumentar a eficiência. Por exemplo, microkernels modernos já aproveitam bem hardware como MMU, então são bastante robustos. Depois, a pequena base de computação confiável do microkernel dá confiabilidade ao kernel, e o kernel e o hardware juntos formam uma base sólida
No fim, é uma questão de até que ponto se permite “trapacear” com o hardware, mas, no geral, microkernels aproveitam melhor os recursos de proteção. Ou então dá para olhar para exokernels
https://genode.org/index
É um sistema operacional com suporte ao seL4
Já fiz uma apresentação sobre seL4 em um capítulo local da OWASP. Não sei se consigo encontrar o material
Este projeto é algo realmente bem feito, mas hesito em vê-lo como substituto do Linux, especialmente em computação de uso geral. Isso não quer dizer que microkernels sejam, de modo geral, ruins para uso geral. O RedoxOS parece ter avançado um pouco recentemente e usa um microkernel escrito em Rust
Ainda assim, se o Redox der certo, isso por si só já será um bom avanço. O seL4 leva essas características a um extremo maior. Seus méritos técnicos são excelentes, mas até agora — e provavelmente no futuro — ele não parece ter aquilo que o tornaria “a próxima grande tendência”. Deixando considerações políticas de lado, acho que microkernels terão sucesso, e deveriam ter
Para o seL4 ser realmente útil, é preciso muita coisa em cima dele. Felizmente, também houve bastante trabalho open source nessa parte, e ele está em uma posição muito melhor do que alguns anos atrás
Para cenários estáticos, há o LionsOS[0], que já é bastante utilizável
Para cenários dinâmicos, há o Provably Secure, General-Purpose Operating System[1], que ainda está em estágio inicial
Ambos podem ser encontrados na página Projects[2] da trustworthy systems, vinculada no site do seL4
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
Fico me perguntando se o OS que roda em cima desse kernel também precisaria ser formalmente verificado para que as garantias de segurança sejam válidas
Claro que só o kernel não é muito útil, então o projeto de drivers, servidores de sistema de arquivos e outros serviços que executam sobre o kernel continua sendo importante
Também é importante notar que a maioria dos outros sistemas, incluindo o Linux, tem falhas em um nível fundamental, enquanto o seL4 de fato permite criar sistemas seguros e confiáveis
Assim, é possível executar o kernel Linux ao lado de um processo de alta segurança e ainda ter a garantia de que eles ficam isolados entre si, exceto pelo IPC permitido
Mas há limitações. DMA precisa ser desativado, e também é preciso usar apenas drivers formalmente verificados
Também é importante notar que o kernel multicore do seL4 ainda não foi verificado
O Helios Microkernel de Drew DeVault também vale uma olhada. Dizem que é baseado no seL4
https://ares-os.org/docs/helios/
Na Universidade de Karlsruhe, L4 era popular. Nunca cheguei a olhar em detalhes, mas parecia um projeto interessado principalmente em testar ideias teóricas, em vez de criar algo útil na prática.
Isso foi há 20 anos e, a meu ver, não mudou muito até hoje. Fazendo uma busca rápida, parece haver tentativas de criar sistemas operacionais sobre ele, mas elas parecem mais provas de conceito do que usos reais.
“As remessas do OKL4 ultrapassaram 1,5 bilhão no início de 2012, em sua maioria chips de modem sem fio da Qualcomm. Outras implantações incluem sistemas de infotainment automotivo.”
“Os processadores Apple série A a partir do A7 incluem um coprocessador Secure Enclave que executa um sistema operacional L4; esse OS é o sepOS, baseado no kernel L4-embedded desenvolvido pela NICTA em 2006. Como resultado, o L4 está presente em todos os dispositivos Apple modernos, incluindo Macs com Apple silicon.”
Rittinghaus, ex-aluno de Bellosa, está envolvido com o Unikraft[0], que já apareceu algumas vezes no HN, e usa tecnologia de unikernel.
[0] https://unikraft.org/
“O Secure Enclave Processor executa uma versão do microkernel L4 personalizada pela Apple.”
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
Pelo que vejo, o kernel L4Re também faz parte do Elektrobit Safe Linux.
Fiz meu TCC criando um OS baseado no Pistachio. Sempre pensei que, se tivesse estudado em Karlsruhe, provavelmente teria seguido para pesquisa em sistemas operacionais.
Eu também tinha uma ideia de projeto de sistema operacional, e a capability que eu considerava usava interposição e delegação como no seL4. Há vantagens além das descritas ali. Por exemplo, é possível usar uma capability de proxy para aplicar filtros ao áudio ou implementar transparência de rede.
Eu achava que recursos de tempo real poderiam ser permitidos como implementação opcional. Minha ideia era mais uma especificação do que uma implementação única.
Outra funcionalidade que eu queria era que todos os programas se comportassem de forma determinística, exceto por entrada e saída. Sem E/S, não seria possível saber a data/hora nem o tempo de execução do programa, e também não seria possível verificar recursos do processador. Se fosse usado um recurso sem suporte no hardware, o sistema operacional poderia emulá-lo.
Para implementar isso, eu pensava em combinar suporte de hardware e de software. O documento traz uma observação sobre ataques contra capabilities implementadas em hardware, mas, como não tenho o documento de referência, não sei se esse ataque também se aplicaria ao método que eu tinha em mente.
Do ponto de vista de segurança, parece apresentar a mesma falha do KVM no kernel Linux. Se o hipervisor estiver no ring 0, há o risco de escapar de uma VM para outra VM ou para o próprio host.
Fico curioso para saber como esse risco é mitigado.
Como o VMM não tem mais capabilities do que a própria VM, um escape da VM não tem valor, exceto em sentido acadêmico.
Veja as páginas 8 a 10 do PDF original.