Microkernel

Estrutura de sistemas operacionais monolíticos e baseados em microkernel, respectivamente

Na ciência da computação, um microkernel (muitas vezes abreviado como μ-kernel) é a quantidade quase mínima de software que pode fornecer os mecanismos necessários para implementar um sistema operacional (SO). Esses mecanismos incluem gerenciamento de espaço de endereço de baixo nível, gerenciamento de encadeamento e comunicação entre processos (IPC).

Se o hardware fornecer vários anéis ou modos de CPU, o microkernel pode ser o único software executado no nível mais privilegiado, geralmente referido como supervisor ou modo kernel. As funções tradicionais do sistema operacional, como drivers de dispositivo, pilhas de protocolos e sistemas de arquivos, geralmente são removidas do próprio microkernel e, em vez disso, são executadas no espaço do usuário.

Em termos de tamanho do código-fonte, os microkernels geralmente são menores que os kernels monolíticos. O microkernel MINIX 3, por exemplo, tem apenas aproximadamente 12.000 linhas de código.

História

Os microkernels têm suas raízes no pioneiro da computação dinamarquesa, Per Brinch Hansen, e seu mandato na empresa de informática dinamarquesa Regnecentralen, onde liderou os esforços de desenvolvimento de software para o computador RC 4000. Em 1967, a Regnecentralen estava instalando um protótipo RC 4000 na fábrica de fertilizantes Zakłady Azotowe Puławy na Polônia. O computador usava um pequeno sistema operacional em tempo real adaptado às necessidades da fábrica. Brinch Hansen e sua equipe ficaram preocupados com a falta de generalidade e reutilização do sistema RC 4000. Eles temiam que cada instalação exigisse um sistema operacional diferente, então começaram a investigar maneiras novas e mais gerais de criar software para o RC 4000. Em 1969, seu esforço resultou na conclusão do Sistema de Multiprogramação RC 4000. Seu núcleo fornecia comunicação entre processos baseada na passagem de mensagens para até 23 processos não privilegiados, dos quais 8 por vez eram protegidos um do outro. Além disso, implementou o agendamento de fatias de tempo de programas executados em paralelo, iniciação e controle da execução do programa a pedido de outros programas em execução e iniciação de transferências de dados de ou para periféricos. Além desses mecanismos elementares, não havia nenhuma estratégia interna para execução de programas e alocação de recursos. Essa estratégia deveria ser implementada por uma hierarquia de programas em execução na qual os processos pais tinham controle total sobre os processos filhos e agiam como seus sistemas operacionais.

Seguindo o trabalho de Brinch Hansen, os microkernels foram desenvolvidos desde a década de 1970. O próprio termo microkernel apareceu pela primeira vez em 1981. Os microkernels foram concebidos como uma resposta às mudanças no mundo dos computadores e a vários desafios de adaptação de "mono-kernels" a esses novos sistemas. Novos drivers de dispositivos, pilhas de protocolos, sistemas de arquivos e outros sistemas de baixo nível estavam sendo desenvolvidos o tempo todo. Esse código normalmente estava localizado no kernel monolítico e, portanto, exigia um trabalho considerável e um gerenciamento de código cuidadoso para trabalhar. Microkernels foram desenvolvidos com a ideia de que todos esses serviços seriam implementados como programas de espaço de usuário, como qualquer outro, permitindo que fossem trabalhados monoliticamente e iniciados e parados como qualquer outro programa. Isso não apenas permitiria que esses serviços fossem mais facilmente trabalhados, mas também separaria o código do kernel para permitir que ele fosse ajustado sem se preocupar com efeitos colaterais indesejados. Além disso, permitiria que sistemas operacionais inteiramente novos fossem "construídos" em um núcleo comum, auxiliando na pesquisa de sistemas operacionais.

Os microkernels foram um tópico muito discutido na década de 1980, quando as primeiras redes locais utilizáveis foram introduzidas. O kernel AmigaOS Exec foi um dos primeiros exemplos, introduzido em 1986 e usado em um PC com relativo sucesso comercial. A falta de proteção de memória, considerada em outros aspectos uma falha, permitia que esse kernel tivesse um desempenho de passagem de mensagens muito alto porque não precisava copiar dados durante a troca de mensagens entre programas do espaço do usuário.

Os mesmos mecanismos que permitiram que o kernel fosse distribuído no espaço do usuário também permitiram que o sistema fosse distribuído pelos links de rede. Os primeiros microkernels, notavelmente o Mach criado por Richard Rashid, provaram ter um desempenho decepcionante, mas as vantagens inerentes pareciam tão grandes que se tornou uma importante linha de pesquisa no final dos anos 1990. Entretanto, nessa época a velocidade dos computadores cresceu muito em relação aos sistemas de rede, e as desvantagens de desempenho passaram a sobrepujar as vantagens em termos de desenvolvimento.

Muitas tentativas foram feitas para adaptar os sistemas existentes para obter melhor desempenho, mas a sobrecarga sempre foi considerável e a maioria desses esforços exigia que os programas do espaço do usuário fossem movidos de volta para o kernel. Em 2000, a maioria dos esforços de kernel Mach em grande escala havia terminado, embora o macOS da Apple, lançado em 2001, ainda usasse um kernel híbrido chamado XNU, que combina um kernel Mach OSF/1 fortemente modificado (híbrido). (kernel OSFMK 7.3) com código do BSD UNIX, e este kernel também é usado em iOS, tvOS e watchOS. O Windows NT, começando com o NT 3.1 e continuando com o Windows 11, usa um design de kernel híbrido. A partir de 2012, o GNU Hurd baseado em Mach também é funcional e incluído nas versões de teste do Arch Linux e Debian.

Embora o trabalho principal em microkernels tenha terminado, os experimentadores continuaram o desenvolvimento. Desde então, foi demonstrado que muitos dos problemas de desempenho de projetos anteriores não eram uma limitação fundamental do conceito, mas sim devido ao desejo do designer de usar sistemas de propósito único para implementar o máximo possível desses serviços. O uso de uma abordagem mais pragmática para o problema, incluindo código de montagem e contando com o processador para impor conceitos normalmente suportados em software, levou a uma nova série de microkernels com desempenho dramaticamente aprimorado.

Os microkernels estão intimamente relacionados aos exokernels. Eles também têm muito em comum com hipervisores, mas os últimos não reivindicam minimalismo e são especializados para suportar máquinas virtuais; o microkernel L4 freqüentemente encontra uso em uma capacidade de hipervisor.

Introdução

Os kernels dos primeiros sistemas operacionais eram bastante pequenos, em parte porque a memória do computador era limitada. À medida que a capacidade dos computadores crescia, o número de dispositivos que o kernel tinha para controlar também crescia. Ao longo da história inicial do Unix, os kernels eram geralmente pequenos, embora contivessem vários drivers de dispositivo e implementações de sistema de arquivos. Quando os espaços de endereço aumentaram de 16 para 32 bits, o design do kernel não foi mais limitado pela arquitetura do hardware e os kernels começaram a crescer.

O Berkeley Software Distribution (BSD) do Unix iniciou a era dos kernels maiores. Além de operar um sistema básico que consiste em CPU, discos e impressoras, a BSD adicionou um sistema de rede TCP/IP completo e vários recursos "virtuais" dispositivos que permitiam que os programas existentes funcionassem 'invisivelmente' pela rede. Esse crescimento continuou por muitos anos, resultando em kernels com milhões de linhas de código-fonte. Como resultado desse crescimento, os kernels eram propensos a bugs e se tornavam cada vez mais difíceis de manter.

O microkernel foi planejado para lidar com esse crescimento de kernels e as dificuldades resultantes. Em teoria, o design do microkernel permite um gerenciamento mais fácil do código devido à sua divisão em serviços de espaço do usuário. Isso também permite maior segurança e estabilidade resultantes da quantidade reduzida de código em execução no modo kernel. Por exemplo, se um serviço de rede travar devido ao estouro do buffer, apenas a memória do serviço de rede será corrompida, deixando o restante do sistema ainda funcional.

Comunicação entre processos

Comunicação entre processos (IPC) é qualquer mecanismo que permite que processos separados se comuniquem entre si, geralmente enviando mensagens. A memória compartilhada é, estritamente definida, também um mecanismo de comunicação entre processos, mas a abreviação IPC geralmente se refere apenas à passagem de mensagens, e é a última que é particularmente relevante para microkernels. O IPC permite que o sistema operacional seja construído a partir de vários programas menores chamados servidores, que são usados por outros programas no sistema, invocados via IPC. A maior parte ou todo o suporte para hardware periférico é tratado dessa maneira, com servidores para drivers de dispositivo, pilhas de protocolos de rede, sistemas de arquivos, gráficos, etc.

O IPC pode ser síncrono ou assíncrono. O IPC assíncrono é análogo à comunicação de rede: o remetente despacha uma mensagem e continua a execução. O receptor verifica (pesquisa) a disponibilidade da mensagem ou é alertado por meio de algum mecanismo de notificação. O IPC assíncrono requer que o kernel mantenha buffers e filas para mensagens e lide com estouros de buffer; também requer cópia dupla de mensagens (remetente para kernel e kernel para receptor). No IPC síncrono, a primeira parte (remetente ou receptor) bloqueia até que a outra parte esteja pronta para executar o IPC. Ele não requer armazenamento em buffer ou várias cópias, mas o encontro implícito pode tornar a programação complicada. A maioria dos programadores prefere envio assíncrono e recebimento síncrono.

Microkernels de primeira geração geralmente suportavam IPC síncrono e assíncrono e sofriam de baixo desempenho do IPC. Jochen Liedtke assumiu que o projeto e a implementação dos mecanismos do IPC eram a razão subjacente para esse fraco desempenho. Em seu microkernel L4, ele foi pioneiro em métodos que reduziram os custos do IPC em uma ordem de magnitude. Isso inclui uma chamada de sistema IPC que suporta uma operação de envio e recebimento, tornando todos os IPC síncronos e passando o máximo de dados possível nos registradores. Além disso, Liedtke introduziu o conceito de troca direta de processo, onde durante uma execução IPC uma troca de contexto (incompleta) é realizada do remetente diretamente para o destinatário. Se, como em L4, parte ou toda a mensagem for passada em registradores, isso transfere a parte do registrador da mensagem sem nenhuma cópia. Além disso, a sobrecarga de chamar o agendador é evitada; isso é especialmente benéfico no caso comum em que o IPC é usado em um tipo de chamada de procedimento remoto (RPC) por um cliente que chama um servidor. Outra otimização, chamada de escalonamento preguiçoso, evita passar pelas filas de agendamento durante o IPC, deixando as threads que bloqueiam durante o IPC na fila pronta. Uma vez que o escalonador é invocado, ele move tais threads para a fila de espera apropriada. Como em muitos casos um encadeamento é desbloqueado antes da próxima invocação do agendador, essa abordagem economiza um trabalho significativo. Abordagens semelhantes já foram adotadas pelo QNX e MINIX 3.

Em uma série de experimentos, Chen e Bershad compararam os ciclos de memória por instrução (MCPI) do Ultrix monolítico com os do microkernel Mach combinado com um servidor Unix 4.3BSD rodando no espaço do usuário. Seus resultados explicaram o pior desempenho de Mach pelo MCPI mais alto e demonstraram que o IPC sozinho não é responsável por grande parte da sobrecarga do sistema, sugerindo que as otimizações focadas exclusivamente no IPC terão um efeito limitado. Liedtke mais tarde refinou os resultados de Chen e Bershad fazendo uma observação de que a maior parte da diferença entre Ultrix e Mach MCPI foi causada por perdas de cache de capacidade e concluindo que reduzir drasticamente o conjunto de trabalho de cache de um microkernel resolverá o problema.

Em um sistema cliente-servidor, a maior parte da comunicação é essencialmente síncrona, mesmo usando primitivas assíncronas, já que a operação típica é um cliente chamando um servidor e aguardando uma resposta. Como também se presta a uma implementação mais eficiente, a maioria dos microkernels geralmente seguiu o exemplo do L4 e forneceu apenas uma primitiva IPC síncrona. O IPC assíncrono pode ser implementado no topo usando threads auxiliares. No entanto, a experiência mostrou que a utilidade do IPC síncrono é duvidosa: o IPC síncrono força um design multi-thread em sistemas simples, com as complexidades de sincronização resultantes. Além disso, uma invocação de servidor semelhante a RPC sequencializa o cliente e o servidor, o que deve ser evitado se eles estiverem sendo executados em núcleos separados. Versões do L4 implantadas em produtos comerciais, portanto, acharam necessário adicionar um mecanismo de notificação assíncrono para oferecer melhor suporte à comunicação assíncrona. Esse mecanismo semelhante a um sinal não transporta dados e, portanto, não requer armazenamento em buffer pelo kernel. Por terem duas formas de IPC, eles violaram o princípio da minimalidade. Outras versões do L4 mudaram completamente para IPC assíncrono.

Como o IPC síncrono bloqueia a primeira parte até que a outra esteja pronta, o uso irrestrito pode facilmente levar a impasses. Além disso, um cliente pode montar facilmente um ataque de negação de serviço em um servidor enviando uma solicitação e nunca tentando receber a resposta. Portanto, o IPC síncrono deve fornecer um meio para evitar o bloqueio indefinido. Muitos microkernels fornecem timeouts em chamadas IPC, o que limita o tempo de bloqueio. Na prática, é difícil escolher valores de timeout sensatos, e os sistemas quase inevitavelmente usam timeouts infinitos para clientes e timeouts zero para servidores. Como consequência, a tendência é não fornecer timeouts arbitrários, mas apenas um sinalizador que indique que o IPC deve falhar imediatamente se o parceiro não estiver pronto. Essa abordagem fornece efetivamente uma escolha de dois valores de tempo limite de zero e infinito. Versões recentes de L4 e MINIX seguiram esse caminho (versões mais antigas de L4 usavam timeouts). O QNX evita o problema exigindo que o cliente especifique o buffer de resposta como parte da chamada de envio de mensagem. Quando o servidor responde, o kernel copia os dados para o buffer do cliente, sem ter que esperar que o cliente receba a resposta explicitamente.

Servidores

Servidores de microkernel são essencialmente programas daemon como quaisquer outros, exceto que o kernel concede a alguns deles privilégios para interagir com partes da memória física que estão fora dos limites da maioria dos programas. Isso permite que alguns servidores, principalmente os drivers de dispositivo, interajam diretamente com o hardware.

Um conjunto básico de servidores para um microkernel de uso geral inclui servidores de sistema de arquivos, servidores de driver de dispositivo, servidores de rede, servidores de exibição e servidores de dispositivo de interface de usuário. Este conjunto de servidores (retirado do QNX) fornece aproximadamente o conjunto de serviços oferecidos por um kernel monolítico do Unix. Os servidores necessários são iniciados na inicialização do sistema e fornecem serviços, como acesso a arquivos, rede e dispositivos, para programas aplicativos comuns. Com esses servidores rodando no ambiente de um aplicativo de usuário, o desenvolvimento do servidor é semelhante ao desenvolvimento de aplicativos comuns, em vez do processo de construção e inicialização necessário para o desenvolvimento do kernel.

Além disso, muitas "falhas" pode ser corrigido simplesmente parando e reiniciando o servidor. No entanto, parte do estado do sistema é perdida com a falha do servidor, portanto, essa abordagem requer que os aplicativos lidem com a falha. Um bom exemplo é um servidor responsável por conexões TCP/IP: Se este servidor for reiniciado, os aplicativos sofrerão um erro "perdido" conexão, uma ocorrência normal em um sistema em rede. Para outros serviços, a falha é menos esperada e pode exigir alterações no código do aplicativo. Para QNX, a capacidade de reinicialização é oferecida como o QNX High Availability Toolkit.

Drivers de dispositivo

Os drivers de dispositivo freqüentemente realizam acesso direto à memória (DMA) e, portanto, podem gravar em locais arbitrários da memória física, incluindo várias estruturas de dados do kernel. Esses drivers devem, portanto, ser confiáveis. É um equívoco comum pensar que isso significa que eles devem fazer parte do kernel. Na verdade, um driver não é inerentemente mais ou menos confiável por fazer parte do kernel.

Embora a execução de um driver de dispositivo no espaço do usuário não reduza necessariamente os danos que um driver malcomportado pode causar, na prática é benéfico para a estabilidade do sistema na presença de drivers com erros (em vez de maliciosos): violações de acesso à memória pelo driver o próprio código (ao contrário do dispositivo) ainda pode ser capturado pelo hardware de gerenciamento de memória. Além disso, muitos dispositivos não são compatíveis com DMA, seus drivers podem se tornar não confiáveis ao executá-los no espaço do usuário. Recentemente, um número crescente de computadores apresenta IOMMUs, muitos dos quais podem ser usados para restringir o acesso de um dispositivo à memória física. Isso também permite que os drivers de modo de usuário se tornem não confiáveis.

Os drivers de modo de usuário são anteriores aos microkernels. O Michigan Terminal System (MTS), em 1967, suportava drivers de espaço de usuário (incluindo seu suporte de sistema de arquivos), o primeiro sistema operacional a ser projetado com essa capacidade. Historicamente, os drivers eram menos problemáticos, já que o número de dispositivos era pequeno e confiável de qualquer maneira, portanto, tê-los no kernel simplificou o design e evitou possíveis problemas de desempenho. Isso levou ao estilo tradicional de driver no kernel do Unix, Linux e Windows NT. Com a proliferação de vários tipos de periféricos, a quantidade de código de driver aumentou e em sistemas operacionais modernos domina o kernel em tamanho de código.

Componentes essenciais e minimalismo

Como um microkernel deve permitir a criação de serviços de sistema operacional arbitrários, ele deve fornecer algumas funcionalidades principais. No mínimo, isso inclui:

• Alguns mecanismos para lidar com espaços de endereço, necessários para gerenciar a proteção de memória
• Algumas abstração de execução para gerenciar a alocação de CPU, tipicamente threads ou ativações de agendamento
• Comunicação inter-processo, necessária para invocar servidores em execução em seus próprios espaços de endereço

Esse design mínimo foi desenvolvido pelo Brinch Hansen's Nucleus e o hypervisor da VM da IBM. Desde então, foi formalizado no princípio da minimalidade de Liedtke:

Um conceito é tolerado dentro do microkernel somente se movê-lo fora do kernel, ou seja, permitir implementações concorrentes, impediria a implementação da funcionalidade necessária do sistema.

Todo o resto pode ser feito em um programa de modo de usuário, embora os drivers de dispositivo implementados como programas de usuário possam, em algumas arquiteturas de processador, exigir privilégios especiais para acessar o hardware de E/S.

Relacionado ao princípio da minimalidade, e igualmente importante para o projeto do microkernel, está a separação entre mecanismo e política, é o que possibilita a construção de sistemas arbitrários em cima de um kernel mínimo. Qualquer política incorporada ao kernel não pode ser substituída no nível do usuário e, portanto, limita a generalidade do microkernel. A política implementada em servidores de nível de usuário pode ser alterada substituindo os servidores (ou permitindo que o aplicativo escolha entre servidores concorrentes que oferecem serviços semelhantes).

Por questões de eficiência, a maioria dos microkernels contém escalonadores e gerencia cronômetros, violando o princípio da minimalidade e o princípio da separação política-mecanismo.

A inicialização (inicialização) de um sistema baseado em microkernel requer drivers de dispositivo, que não fazem parte do kernel. Normalmente, isso significa que eles são empacotados com o kernel na imagem de inicialização e o kernel oferece suporte a um protocolo de inicialização que define como os drivers são localizados e iniciados; este é o procedimento de bootstrap tradicional dos microkernels L4. Alguns microkernels simplificam isso colocando alguns drivers-chave dentro do kernel (em violação do princípio da minimalidade), LynxOS e o Minix original são exemplos. Alguns até incluem um sistema de arquivos no kernel para simplificar a inicialização. Um sistema baseado em microkernel pode inicializar por meio de um carregador de inicialização compatível com inicialização múltipla. Esses sistemas geralmente carregam servidores vinculados estaticamente para fazer uma inicialização inicial ou montar uma imagem do sistema operacional para continuar a inicialização.

Um componente-chave de um microkernel é um bom sistema IPC e um design de gerenciador de memória virtual que permite implementar o tratamento de falhas de página e a troca em servidores de modo de usuário de maneira segura. Como todos os serviços são executados por programas em modo de usuário, meios eficientes de comunicação entre os programas são essenciais, muito mais do que em kernels monolíticos. O design do sistema IPC faz ou quebra um microkernel. Para ser eficaz, o sistema IPC não deve apenas ter baixa sobrecarga, mas também interagir bem com o escalonamento da CPU.

Desempenho

Na maioria dos processadores convencionais, obter um serviço é inerentemente mais caro em um sistema baseado em microkernel do que em um sistema monolítico. No sistema monolítico, o serviço é obtido por uma única chamada de sistema, que requer duas chaves de modo (alterações do anel do processador ou do modo da CPU). No sistema baseado em microkernel, o serviço é obtido enviando uma mensagem IPC para um servidor e obtendo o resultado em outra mensagem IPC do servidor. Isso requer uma troca de contexto se os drivers forem implementados como processos ou uma chamada de função se forem implementados como procedimentos. Além disso, passar dados reais para o servidor e vice-versa pode incorrer em sobrecarga extra de cópia, enquanto em um sistema monolítico o kernel pode acessar diretamente os dados nos buffers do cliente.

Desempenho é, portanto, um problema potencial em sistemas de microkernel. A experiência de microkernels de primeira geração, como Mach e ChorusOS, mostrou que os sistemas baseados neles tiveram um desempenho muito ruim. No entanto, Jochen Liedtke mostrou que os problemas de desempenho do Mach eram resultado de um design e implementação ruins, especificamente a pegada de cache excessiva do Mach. Liedtke demonstrou com seu próprio microkernel L4 que, por meio de design e implementação cuidadosos e, especialmente, seguindo o princípio da minimalidade, os custos do IPC podem ser reduzidos em mais de uma ordem de grandeza em comparação com Mach. O desempenho IPC do L4 ainda é imbatível em uma variedade de arquiteturas.

Embora esses resultados demonstrem que o baixo desempenho de sistemas baseados em microkernels de primeira geração não é representativo para kernels de segunda geração, como L4, isso não constitui prova de que sistemas baseados em microkernel possam ser construídos com bom desempenho. Foi demonstrado que um servidor Linux monolítico portado para L4 exibe apenas uma pequena porcentagem de sobrecarga em relação ao Linux nativo. No entanto, tal sistema de servidor único exibe poucas, se alguma, das vantagens que os microkernels supostamente fornecem ao estruturar a funcionalidade do sistema operacional em servidores separados.

Existem vários sistemas multi-servidor comerciais, em particular os sistemas de tempo real QNX e Integrity. Nenhuma comparação abrangente de desempenho em relação a sistemas monolíticos foi publicada para esses sistemas multiservidor. Além disso, o desempenho não parece ser a preocupação primordial para esses sistemas comerciais, que, em vez disso, enfatizam tempos de resposta de tratamento de interrupção rápidos e confiáveis (QNX) e simplicidade em prol da robustez. Uma tentativa de construir um sistema operacional multiservidor de alto desempenho foi o projeto IBM Sawmill Linux. No entanto, este projeto nunca foi concluído.

Entretanto, foi demonstrado que os drivers de dispositivo no nível do usuário podem se aproximar do desempenho dos drivers no kernel, mesmo para dispositivos de alta taxa de transferência e alta interrupção, como Gigabit Ethernet. Isso parece implicar que sistemas multiservidor de alto desempenho são possíveis.

Segurança

Os benefícios de segurança dos microkernels têm sido discutidos com frequência. No contexto da segurança, o princípio de minimalidade dos microkernels é, alguns argumentaram, uma consequência direta do princípio do menor privilégio, segundo o qual todo código deve ter apenas os privilégios necessários para fornecer a funcionalidade necessária. Minimalidade requer que a base de computação confiável (TCB) de um sistema seja mantida mínima. Como o kernel (o código que executa no modo privilegiado do hardware) tem acesso não controlado a qualquer dado e pode, portanto, violar sua integridade ou confidencialidade, o kernel sempre faz parte do TCB. Minimizá-lo é natural em um projeto voltado para a segurança.

Consequentemente, projetos de microkernel têm sido usados para sistemas projetados para aplicações de alta segurança, incluindo KeyKOS, EROS e sistemas militares. De fato, os critérios comuns (CC) no mais alto nível de garantia (Evaluation Assurance Level (EAL) 7) têm uma exigência explícita de que o objetivo da avaliação seja "simples", um reconhecimento da impossibilidade prática de estabelecer a verdadeira confiabilidade para um sistema complexo. Novamente, o termo "simples" é enganosa e mal definida. Pelo menos os Critérios de Avaliação do Sistema de Computador Confiável do Departamento de Defesa introduziram um palavreado um pouco mais preciso nas classes B3/A1:

"O TCB [implement] completa e conceitualmente simples mecanismos de proteção com semântica definida com precisão. A engenharia significativa do sistema deve ser direcionada para minimizar a complexidade do TCB, bem como excluir do TCB os módulos que não são críticos de proteção."

—Departamento de Defesa Critérios de Avaliação do Sistema de Computação Confiável

Em 2018, um artigo apresentado na Conferência de Sistemas da Ásia-Pacífico afirmou que os microkernels eram comprovadamente mais seguros do que os kernels monolíticos, investigando todos os CVEs críticos publicados para o kernel do Linux na época. O estudo concluiu que 40% dos problemas não poderiam ocorrer em um microkernel formalmente verificado e apenas 4% dos problemas permaneceriam totalmente não mitigados em tal sistema.

Terceira geração

Trabalhos mais recentes sobre microkernels têm se concentrado em especificações formais da API do kernel e provas formais das propriedades de segurança e correção da implementação da API. O primeiro exemplo disso é uma prova matemática dos mecanismos de confinamento no EROS, com base em um modelo simplificado da API do EROS. Mais recentemente (em 2007) foi realizado um conjunto abrangente de provas verificadas por máquina das propriedades do modelo de proteção do seL4, uma versão do L4.

Isso levou ao que é conhecido como microkernels de terceira geração, caracterizado por uma API orientada à segurança com acesso a recursos controlado por capacidades, virtualização como uma preocupação de primeira classe, novas abordagens para o kernel gerenciamento de recursos e uma meta de design de adequação para análise formal, além da meta usual de alto desempenho. Exemplos são Coyotos, seL4, Nova, Redox e Fiasco.OC.

No caso do seL4, a verificação formal completa da implementação foi alcançada, ou seja, uma prova matemática de que a implementação do kernel é consistente com sua especificação formal. Isso fornece uma garantia de que as propriedades comprovadas sobre a API realmente são válidas para o kernel real, um grau de garantia que vai além do CC EAL7. Ele foi seguido por provas de propriedades de aplicação de segurança da API e uma prova demonstrando que o código binário executável é uma tradução correta da implementação C, tirando o compilador do TCB. Juntas, essas provas estabelecem uma prova de ponta a ponta das propriedades de segurança do kernel.

Exemplos

Alguns exemplos de microkernels são:

• BlackBerry
• Genode
• Helenos.
• Horizonte
• A família L4 microkernel
• Minix
• Redox
• Ar condicionado

Nanokernel

O termo nanokernel ou picokernel historicamente referido:

• Um kernel onde a quantidade total de código do kernel, ou seja, a execução de código no modo privilegiado do hardware, é muito pequena. O termo picoker. foi às vezes usado para enfatizar ainda mais o tamanho pequeno. O termo Nanoker. foi cunhado por Jonathan S. Shapiro no papel The KeyKOS NanoKernel Architecture. Foi uma resposta sardônica a Mach, que alegou ser um microkernel enquanto Shapiro o considerava monolítico, essencialmente não estruturado e mais lento do que os sistemas que procurava substituir. Reutilização subsequente e resposta ao termo, incluindo a cunhagem de picokernel, sugerem que o ponto foi largamente perdido. Ambos Nanoker. e picoker. ter posteriormente veio a ter o mesmo significado expresso pelo termo microkernel.
• Uma camada de virtualização sob um sistema operacional, que é mais corretamente referida como um hipervisor.
• Uma camada de abstração de hardware que forma a parte mais baixa de um kernel, às vezes usada para fornecer funcionalidade em tempo real para sistemas operacionais normais, como Adeos.

Há também pelo menos um caso em que o termo nanokernel é usado para se referir não a um kernel pequeno, mas a um que suporta uma resolução de relógio de nanossegundos.