Núcleo de separação - Separation kernel

Um kernel de separação é um tipo de kernel de segurança usado para simular um ambiente distribuído. O conceito foi apresentado por John Rushby em um artigo de 1981. Rushby propôs o kernel de separação como uma solução para as dificuldades e problemas que surgiram no desenvolvimento e verificação de grandes e complexos kernels de segurança que tinham como objetivo "fornecer operação segura multinível em sistemas multiusuário de uso geral". De acordo com Rushby, "a tarefa de um kernel de separação é criar um ambiente indistinguível daquele fornecido por um sistema distribuído fisicamente: deve aparecer como se cada regime fosse uma máquina separada e isolada e que a informação só pudesse fluir de uma máquina para outro ao longo de linhas de comunicação externas conhecidas. Uma das propriedades que devemos provar de um kernel de separação, portanto, é que não há canais para o fluxo de informações entre os regimes além daqueles explicitamente fornecidos. "

Uma variante do kernel de separação, o kernel de particionamento, ganhou aceitação na comunidade da aviação comercial como uma forma de consolidar, em um único processador, funções múltiplas, talvez de criticidade mista . Produtos de sistema operacional comercial em tempo real neste gênero têm sido usados ​​por fabricantes de aeronaves para aplicações aviônicas de segurança crítica.

Em 2007, o Information Assurance Directorate da US National Security Agency (NSA) publicou o Separation Kernel Protection Profile (SKPP), uma especificação de requisitos de segurança para kernels de separação adequados para serem usados ​​nos ambientes de ameaças mais hostis. O SKPP descreve, no jargão dos Critérios Comuns , uma classe de produtos modernos que fornecem as propriedades fundamentais do kernel de separação conceitual de Rushby. Ele define os requisitos funcionais e de garantia de segurança para a construção e avaliação de kernels de separação, ao mesmo tempo que fornece alguma latitude nas opções disponíveis para os desenvolvedores.

O SKPP define o kernel de separação como "mecanismos de hardware e / ou firmware e / ou software cuja função principal é estabelecer, isolar e separar múltiplas partições e controlar o fluxo de informações entre os assuntos e os recursos exportados alocados para essas partições." Além disso, os principais requisitos funcionais do kernel de separação incluem:

  • Proteção de todos os recursos (incluindo CPU , memória e dispositivos) contra acesso não autorizado.
  • Separação dos recursos internos usados ​​pelo Target of Evaluation Security Functions (TSF) dos recursos exportados disponibilizados aos sujeitos.
  • Particionamento e isolamento de recursos exportados.
  • A mediação dos fluxos de informação entre partições e entre recursos exportados.
  • Serviços de auditoria.

O kernel de separação aloca todos os recursos exportados sob seu controle em partições. As partições são isoladas, exceto para fluxos de informações explicitamente permitidos. As ações de um sujeito em uma partição são isoladas (viz., Não podem ser detectadas por ou comunicadas a) sujeitos em outra partição, a menos que esse fluxo tenha sido permitido. As partições e fluxos são definidos nos dados de configuração. Observe que 'partição' e 'assunto' são abstrações ortogonais. 'Partição', como indicado por sua gênese matemática, fornece um agrupamento teórico de conjunto de entidades do sistema, enquanto 'sujeito' nos permite raciocinar sobre as entidades ativas individuais de um sistema. Assim, uma partição (uma coleção, contendo zero ou mais elementos) não é um assunto (um elemento ativo), mas pode conter zero ou mais assuntos. O kernel de separação fornece aos seus programas de software hospedados particionamento de alta segurança e propriedades de controle de fluxo de informações que são à prova de violação e não podem ser ignoradas. Esses recursos fornecem uma base confiável configurável para uma variedade de arquiteturas de sistema.

Soluções

Em 2011, a Diretoria de Garantia de Informações encerrou o SKPP. A NSA não irá mais certificar sistemas operacionais específicos, incluindo kernels de separação contra o SKPP, observando que "a conformidade com este perfil de proteção, por si só, não oferece confiança suficiente de que as informações de segurança nacional estão devidamente protegidas no contexto de um sistema maior no qual o conformante o produto está integrado ".

O microkernel seL4 tem uma prova formal de conceito de que pode ser configurado como um kernel de separação. A continuação forçada de informações junto com isso implica que é um exemplo de alto nível de segurança. O kernel de separação Muen também é um kernel de separação de código aberto formalmente verificado para máquinas x86.

Veja também

Referências