Um artigo científico foi publicado em Communications of the ACM , outubro de 2018, volume 61, número 10, pp. 68−77, doi: 10.1145 / 3230627

Em fevereiro de 2017, um helicóptero decolou da pista de pouso da Boeing no Arizona com a missão usual: voar pelas colinas mais próximas. Ele voou completamente de forma autônoma. De acordo com os requisitos de segurança da Administração Federal de Aviação dos EUA, o piloto não tocou nos controles. Este não foi o primeiro vôo autônomo AH-6, que a empresa chama de Passarinho não tripulado (ULB). Ele voa assim há muitos anos. No entanto, desta vez no meio do voo, o helicóptero sofreu um ataque cibernético. O computador de bordo atacou o software malicioso da câmera de vídeo, bem como o vírus transmitido pela unidade flash infectada, que foi inserida durante a manutenção. O ataque ameaçou alguns subsistemas, mas não pôde afetar a operação segura da aeronave.

Ideias-chave

• A evidência formal da arquitetura de software de um microkernel verificado pode ser dimensionada de forma barata para sistemas reais.
• Diferentes níveis de segurança e confiabilidade dentro do mesmo sistema são possíveis e desejáveis. Não é necessário garantir a máxima confiabilidade de todo o código.
• Um redesenho e refatoração moderados são suficientes para elevar os sistemas existentes ao nível de código altamente confiável.

Você pode pensar que a aviação militar pode facilmente repelir um ataque cibernético. Na realidade, uma equipe de agentes profissionais encomendados pela DARPA como parte de um programa para desenvolver sistemas de computadores militares altamente confiáveis ​​em 2013, os Sistemas Militares Cibernéticos de Alta Garantia (HACMS) invadiram com êxito a primeira versão do software ULB, que foi originalmente desenvolvida para garantir a segurança de vôo, não a proteção de ataques cibernéticos. Os hackers tiveram a oportunidade de bater em um helicóptero ou aterrissá-lo em qualquer lugar que desejassem. Portanto, o risco de tais ataques com um passageiro a bordo dificilmente pode ser superestimado, e uma tentativa malsucedida de hacking em fevereiro de 2017 indica algumas mudanças fundamentais no software.

Este artigo explica essas alterações e a tecnologia que as tornou possíveis. Essa é uma tecnologia desenvolvida como parte do programa HACMS, que visa garantir a operação segura de sistemas críticos em um ambiente cibernético hostil - neste caso, vários veículos autônomos. A tecnologia é baseada na verificação formal de software - são programas com provas matemáticas verificadas automaticamente que funcionam de acordo com suas especificações. Embora o artigo não seja dedicado aos métodos formais, ele explica como usar a verificação de artefato para proteger sistemas reais na prática.

Talvez o resultado mais impressionante do HACMS seja que a tecnologia possa ser estendida aos sistemas reais existentes, melhorando consideravelmente sua proteção contra ataques cibernéticos. Esse processo é chamado de "retrofit de segurança sísmica", semelhante às atualizações de construção sísmica. Além disso, a maior parte da reengenharia foi realizada por engenheiros da Boeing, e não por especialistas formais de verificação.


"Pássaro" durante um voo de teste não tripulado

Nem todo software de helicóptero é construído com base em modelos e evidências matemáticas. O campo da verificação formal ainda não está pronto para essa escala. No entanto, o programa HACMS demonstrou que a aplicação estratégica de métodos formais nas partes mais importantes do sistema geral melhora muito a proteção. A abordagem HACMS funciona para sistemas nos quais o recurso de segurança desejado pode ser alcançado por meio de uma aplicação puramente no nível da arquitetura. É baseado no nosso microkernel verificado no sel4, sobre o qual falaremos abaixo. Garante o isolamento entre os subsistemas, com exceção dos canais de comunicação claramente definidos e sujeitos às políticas de segurança do sistema. Esse isolamento é garantido no nível da arquitetura com a estrutura verificada do CAmkES para componentes do sistema. Usando linguagens específicas de domínio da Galois Inc. O CAmkES se integra às ferramentas de análise de arquitetura da Rockwell Collins e da Universidade de Minnesota, além de componentes de software altamente confiáveis.

As realizações do HACMS são baseadas no velho amigo fiel de um engenheiro de software - modularização. A inovação é que métodos formais provam a observabilidade de interfaces e o encapsulamento de componentes internos do módulo. Essa aderência garantida à modularidade permite que engenheiros que não são especialistas em métodos formais (como na Boeing) criem novos ou mesmo atualizem sistemas existentes e obtenham alta estabilidade. Embora as ferramentas ainda não forneçam evidências completas da segurança do sistema.

Verificação formal

As evidências da correção matemática dos programas datam de pelo menos a década de 1960 , mas por um longo tempo seus reais benefícios para o desenvolvimento de software foram limitados em escopo e profundidade. No entanto, nos últimos anos, houve várias descobertas impressionantes na verificação formal no nível de código de sistemas reais, do compilador C CompCert verificado ao microkernel seL4 verificado (consulte os artigos científicos a respeito), o sistema de conferência verificado CoCon , o compilador CakeML ML verificado, programas verificados para provar os teoremas de Milawa e Candle , o sistema de arquivos à prova de falhas FSCQ verificado, o sistema distribuído IronFleet verificado e a estrutura verificada do kernel paralelo CertiKOS, além de importantes teoremas matemáticos, incluindo os problemas de quatro cores , a prova automática da hipótese de Kepler e o teorema de Faith - Thompson em ordem ímpar . Todos estes são sistemas reais. Por exemplo, o CompCert é um produto comercial, o microkernel seL4 é usado em aeronaves aeroespaciais e não tripuladas, como plataforma da Internet das coisas, e o sistema CoCon tem sido usado em inúmeras grandes conferências científicas.

Esses projetos de verificação exigem um esforço considerável. Para disponibilizar publicamente métodos formais, esses esforços precisam ser reduzidos. Aqui, demonstramos como uma combinação estratégica de métodos formais e informais, automação parcial de métodos formais e desenvolvimento cuidadoso de software para maximizar os benefícios de componentes isolados nos permitiu aumentar significativamente a confiabilidade de sistemas cujo tamanho e complexidade gerais são ordens de magnitude maiores do que as mencionadas acima.

Observe que aplicamos a verificação formal principalmente para o código do qual a segurança do sistema depende. Mas há outros benefícios. Por exemplo, a evidência de que o código está correto faz suposições sobre o contexto em que é executado (por exemplo, comportamento de hardware e configuração de software). A verificação formal torna essas suposições explícitas, o que ajuda os desenvolvedores a se concentrarem em outras ferramentas de verificação, como testes. Além disso, em muitos casos, o sistema inclui código verificado e não verificado. Durante as análises de código, teste e depuração, a verificação formal age como uma lente, concentrando-se no código crítico e não verificado do sistema.

seL4

Vamos começar com a base para a construção de sistemas comprovadamente confiáveis ​​- o kernel do sistema operacional (SO). Essa é a parte mais importante que garante a confiabilidade de todo o sistema de maneira econômica.

O microkernel seL4 fornece um conjunto mínimo formalmente verificado de mecanismos para implementar sistemas seguros. Ao contrário dos kernels padrão , é propositalmente universal e, portanto, adequado para implementar várias políticas de segurança e requisitos de sistema.

Um dos principais objetivos do desenvolvimento do seL4 é fornecer um forte isolamento entre os componentes que desconfiam mutuamente e que são executados no topo do kernel. Ele suporta seu trabalho como um hipervisor, por exemplo, para sistemas operacionais Linux inteiros, mantendo-os isolados de componentes críticos de segurança que podem funcionar juntos, como mostra a Figura 1. Em particular, essa função permite que os desenvolvedores de sistemas usem componentes legados com recursos ocultos. vulnerabilidades próximas a componentes altamente confiáveis.


Fig. 1. Isolamento e comunicações controladas em seL4

O núcleo seL4 ocupa uma posição especial entre os micronúcleos de uso geral. Além de oferecer melhor desempenho em sua classe , suas 10.000 linhas de código C passaram por uma verificação formal mais rigorosa do que qualquer outro software disponível publicamente na história humana em termos não apenas de linhas de prova, mas também da força de propriedades comprovadas. Baseia-se na prova da “correção funcional” da implementação principal em C. Ele garante que qualquer comportamento do kernel seja previsto por sua especificação abstrata formal: consulte o aplicativo online para ter uma idéia de como essas evidências são exibidas. Após essa garantia, adicionamos evidências adicionais que explicaremos após a introdução aos mecanismos básicos do núcleo.

API seL4

O kernel seL4 fornece um conjunto mínimo de mecanismos para a implementação de sistemas seguros: fluxos, gerenciamento de capacidade, espaços de endereço virtual, comunicação entre processos (IPC), sinalização e interrupção de entrega.

O kernel mantém seu estado nos "objetos do kernel". Por exemplo, para cada encadeamento no sistema, existe um "objeto de fluxo" que armazena informações sobre descarte, execução e controle de acesso. Os programas de espaço do usuário podem se referir apenas aos objetos do kernel indiretamente por meio dos chamados "recursos" ou "recursos", que combinam um link para um objeto com um conjunto de direitos de acesso a ele. Por exemplo, um encadeamento não pode iniciar ou parar outro encadeamento se não tiver a "capacidade" para o objeto de encadeamento correspondente.

Os threads interagem e sincronizam enviando mensagens através dos "pontos finais" de comunicação entre processos. Um encadeamento com capacidade de enviar para o terminal correspondente pode enviar uma mensagem para outro encadeamento que tem a capacidade de receber para esse terminal. Os objetos de notificação fornecem sincronização entre conjuntos de semáforos binários. A conversão de endereço virtual é controlada por objetos do kernel que representam diretórios de páginas, tabelas de páginas e objetos de quadro ou abstrações sutis sobre os objetos de arquitetura do processador correspondentes. Cada fluxo possui uma certa capacidade de "VSpace", que aponta para a raiz da árvore dos objetos de conversão de endereço de fluxo. Os recursos em si são gerenciados pelo kernel e armazenados nos objetos do kernel "CNodes", localizados na estrutura do gráfico, que mapeia links para objetos com direitos de acesso, semelhante à comparação de tabelas de páginas virtuais com endereços físicos na memória. Cada thread tem sua própria capacidade de identificar o CNode raiz. O conjunto de recursos disponíveis nessa raiz, chamamos de "CSpace Stream". As habilidades podem ser transferidas através de terminais com transferência de tarefas e também podem ser declaradas compartilhadas usando o CSpace comum. A Figura 2 mostra esses objetos do kernel.


Fig. 2. Objetos do kernel em um sistema seL4 com dois threads interagindo através de um nó de extremidade

Evidência de segurança

Devido à sua versatilidade, as APIs do kernel seL4 são de baixo nível e suportam arquiteturas de sistema altamente dinâmicas. Portanto, é difícil obter evidências diretas dessas APIs.

O conceito de alto nível de políticas de controle de acesso abstrai de objetos individuais e recursos do kernel, capturando a configuração de controle de acesso do sistema usando um conjunto de "assuntos" (componentes) abstratos e os poderes que cada um deles tem sobre outros (por exemplo, para ler dados e enviar mensagens) . No exemplo da fig. 2, os componentes A e B obtiveram autoridade sobre o terminal.

Sewell e colegas provaram que as políticas de controle de acesso seL4 garantem o respeito de dois recursos básicos de segurança: restrição de privilégios e integridade.

A restrição de autoridade significa que a política de controle de acesso é uma aproximação segura estática (inalterada) de recursos específicos e objetos do kernel no sistema para qualquer estado futuro. Essa propriedade implica que, não importa como o sistema evolua, nenhum componente receberá mais autoridade do que a política de controle de acesso prevê. Na Figura 2, a política para o componente B não possui acesso de gravação ao componente A. Portanto, o componente B nunca poderá obter esse acesso no futuro. Essa propriedade implica que o raciocínio no nível da política é uma aproximação segura ao raciocínio sobre o estado específico do controle de acesso no sistema.

Integridade significa que, não importa o que o componente faça, ele nunca poderá alterar dados no sistema (incluindo quaisquer chamadas do sistema que possa fazer) que claramente não tem permissão para alterar a política de controle de acesso. Por exemplo, na fig. 2, o único componente da autoridade de A sobre outro componente é o direito de enviar dados para o terminal de onde o componente B. recebe informações. Isso significa que o componente A só pode alterar seu estado, o estado do encadeamento B e o estado do buffer de mensagens. Não pode alterar outras partes do sistema.

Um efeito colateral da integridade é a confidencialidade, quando um componente é incapaz de ler informações de outro componente sem permissão : é uma propriedade forte comprovada da não interferência não transitiva e não transitória. Ou seja, em um sistema configurado corretamente (com restrições mais rigorosas do que apenas para integridade), nenhum dos componentes pode, sem permissão, descobrir informações sobre outro componente ou sua execução. A prova expressa essa propriedade em termos da política de fluxo de informações, que pode ser extraída da política de controle de acesso usada na prova de integridade. As informações serão transmitidas somente quando explicitamente permitido pela política. A prova cobre fluxos de informações explícitos, bem como possíveis canais de armazenamento ocultos no kernel. Mas os canais de sincronização estão fora de sua área e devem ser processados ​​por outros meios .

Outras evidências no seL4 incluem uma extensão da correção funcional e, portanto, teoremas de segurança para um nível binário da arquitetura ARMv7 e um perfil de tempo de execução do pior caso para o kernel ( 1 , 2 ), necessário para sistemas em tempo real. O núcleo seL4 está disponível para várias arquiteturas: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 e Intel x64. No momento, ele passou no teste da máquina na arquitetura do ARMv7 para toda a pilha de verificação, bem como no ARMv7a com extensões de hipervisor para correção funcional.

Arquitetura Segurança

A seção anterior descreveu os métodos de programação pelos quais o kernel seL4 cria uma base sólida para sistemas comprovadamente confiáveis. O kernel forma uma base de computação confiável (TCB) - um componente essencial do software que deve funcionar corretamente para garantir a segurança do sistema. Em sistemas reais, essa base é muito mais ampla do que apenas um microkernel. É necessário verificar uma pilha de software adicional para obter o mesmo nível de confiança do kernel. No entanto, existem classes de sistemas para as quais não há necessidade dessa verificação: eles precisam de teoremas de isolamento no nível do kernel para derivar certas propriedades de segurança no nível do sistema. Esta seção fornece um exemplo desse sistema.

Esses são sistemas nos quais as arquiteturas de componentes já implementaram uma propriedade crítica, talvez junto com vários pequenos componentes confiáveis. Nosso exemplo é o software de controle de vôo quadcopter, um dispositivo de demonstração no programa HACMS mencionado anteriormente.

A Figura 3 mostra os principais componentes de hardware do quadrocóptero. A arquitetura é intencionalmente mais complexa do que a exigida pelo quadcopter, pois deveria representar o ULB e, nesse nível de abstração, é semelhante à arquitetura do ULB.


Fig. 3. Arquitetura de uma aeronave autônoma

A figura mostra dois computadores principais: um computador de bordo que interage com a estação terrestre e controla o software a bordo (por exemplo, a câmera) e um computador de navegação para controlar o voo do veículo, ler dados do sensor e controlar os motores. Os computadores são conectados através de uma rede interna ou barramento CAN em um quadrocopter, Ethernet em ULB. O quadrocopter também possui um ponto WiFi desprotegido, o que possibilita demonstrar métodos de proteção adicionais.

Neste exemplo, considere um computador de bordo. Quatro propriedades básicas devem ser cumpridas para isso:

• autenticação adequada de comandos da estação terrestre;
  
• privacidade de chaves criptográficas;
  
• nenhuma mensagem adicional para o computador de navegação;
  
• o software não confiável de outros sistemas de bordo não pode afetar o voo do dispositivo.

A hipótese de trabalho é que a câmera não é confiável, potencialmente comprometida ou maliciosa, que seus drivers e software desatualizado estão potencialmente comprometidos, bem como quaisquer canais de comunicação externos. Neste exemplo, assumimos a criptografia correta e forte, ou seja, que a chave não pode ser apanhada e vamos além do escopo da tarefa para suprimir as radiocomunicações do inimigo com uma estação terrestre.

A Figura 4 mostra como a arquitetura do quadrocóptero é projetada para fornecer essas propriedades. A máquina virtual (VM) do Linux serve como um contêiner para software de dispositivo de bordo herdado, drivers de câmera e pontos de acesso WiFi. Isolamos o módulo de controle de criptografia em seu próprio componente, com conexões ao barramento CAN, ao canal da estação terrestre e à máquina virtual Linux para enviar dados para a estação terrestre. A tarefa do componente criptográfico é transmitir (apenas) mensagens autorizadas para o computador de bordo através da interface CAN da pilha e enviar dados de diagnóstico de volta à estação terrestre. O componente de rádio envia e recebe mensagens brutas que são criptografadas e descriptografadas (com autenticação) pelo componente criptográfico.


Fig. 4. Arquitetura simplificada do computador de bordo com quadcopter

A configuração das propriedades desejadas do sistema é reduzida apenas às propriedades de isolamento e ao comportamento da arquitetura em termos de fluxos de informações, bem como ao comportamento de um único componente criptográfico confiável. Assumindo o comportamento correto desse componente, as chaves não podem ser comprometidas, pois nenhum outro componente tem acesso a elas. O canal entre o Linux e o componente criptográfico na Fig. 4 destina-se apenas a mensagens e não dá acesso à memória. Somente mensagens autorizadas podem entrar no barramento CAN, porque o componente criptográfico é a única comunicação com o barramento. Software não confiável e WiFi, como parte da máquina virtual Linux, são encapsulados pelo isolamento de componentes e só podem interagir com o restante do sistema por meio de um componente criptográfico confiável.

É fácil imaginar que essa análise da arquitetura possa ser automatizada em grande parte, verificando modelos e ferramentas de raciocínio mecânico de nível superior. Conforme observado nos sistemas MILS , os limites dos componentes dessa arquitetura não são apenas uma ferramenta conveniente para particionamento e gerenciamento de código, mas o isolamento forçado fornece limites efetivos para o raciocínio formal sobre o comportamento do sistema. No entanto, tudo depende da aplicação adequada dos limites dos componentes em tempo de execução na implementação final do sistema binário.

Os mecanismos discutidos anteriormente do kernel seL4 são capazes de fornecer tal implementação, mas o nível de abstração de mecanismos contrasta fortemente com os blocos e as setas do esquema arquitetural: uma política de controle de acesso ainda mais abstrata ainda contém muito mais detalhes do que o esquema de arquitetura. Em um sistema real desse tamanho, dezenas de milhares de objetos e "habilidades" do kernel são criados por software, e erros de configuração podem levar a violações de segurança. Em seguida, discutiremos como não apenas automatizamos a configuração e a criação desse código, mas também como provar automaticamente a conformidade com os limites da arquitetura.

Verificação de exibição de componente

Como as evidências de segurança são simplificadas com abstrações formais de políticas de segurança, a abstração também ajuda no design do sistema. A plataforma Camkes do componente é executada em abstrações seL4 sobre os mecanismos de baixo nível do kernel, fornecendo primitivas de comunicação e decompondo o sistema em unidades funcionais, conforme mostrado na Fig. 5. Usando essa plataforma, os arquitetos de sistemas podem projetar e construir sistemas baseados no seL4 em termos de componentes de alto nível que interagem entre si e com dispositivos de hardware por meio de conectores, como chamadas de procedimento remoto (RPC), dataports e eventos.


Fig. 5. Fluxo de trabalho do CAmkES

Geração de código

Internamente, o CAmkES implementa essas abstrações usando objetos de kernel de baixo nível no seL4. Cada componente contém (pelo menos) um fluxo, CSpace e VSpace. Os conectores RPC usam objetos de terminal e o CAmkES gera código intermediário para processar mensagens e enviá-las aos terminais do IPC. Da mesma forma, o conector do dataport é implementado através da memória compartilhada - quadros comuns presentes nos espaços de endereço de dois componentes - e, opcionalmente, pode limitar a direção da transferência de dados. Finalmente, o conector de evento é implementado usando o mecanismo de notificação seL4.

O CAmkES também gera no capDL uma especificação de baixo nível da configuração inicial de objetos e dos recursos do kernel do sistema. Essa especificação se torna entrada para o inicializador seL4, queele inicia primeiro após o carregamento e executa as operações seL4 necessárias para criar uma instância e inicializar o sistema .

Assim, a plataforma de componentes gera código sem esforço adicional por parte do desenvolvedor. A arquitetura de componentes descreve um conjunto de blocos e setas, e a tarefa de implementação resume-se a simplesmente preencher os campos. A plataforma gera o restante, fornecendo a implementação da arquitetura descrita.

Em uma plataforma com componentes tradicionais, o código gerado expandirá a base de computação confiável do sistema, pois pode afetar a funcionalidade dos componentes. No entanto, o CAmkES também gera evidências.

Evidência automática

Ao gerar o código "intermediário", o CAmkES produz provas formais em Isabelle / HOL, executando a validação durante a tradução e demonstrando que o código "intermediário" gerado obedece à especificação de alto nível, e a especificação capDL gerada é a especificação correta da descrição do CAmkES . Também provamos que o inicializador seL4 configura corretamente o sistema na configuração inicial necessária. Ao mesmo tempo, automatizamos a maior parte da construção do sistema sem expandir a base de computação confiável.

Os desenvolvedores raramente olham para a emissão de geradores de código; eles estão interessados ​​apenas na funcionalidade e na lógica de negócios. Também assumimos que as evidências do código intermediário não precisam ser verificadas, ou seja, os desenvolvedores podem se concentrar em provar a correção de seu próprio código. Assim como o cabeçalho CAmkES gerado fornece ao desenvolvedor uma API para o código gerado, os operadores de lema de nível superior produzem uma API para prova. Os lemas descrevem o comportamento esperado dos conectores. No exemplo de middleware RPC na Figura 6 função gerada$$ fornece uma maneira de chamar uma função remota$f$$$ em outro componente. Para salvar a abstração, chame$g$$$ deve ser equivalente a chamar$f$$$$g$ . O lema gerado pelo sistema garante que $$do código RPC gerado se comporta como uma chamada direta$f$$$$g$ .


Fig. 6. Código RPC gerado

Para o uso real das evidências geradas pelo sistema, elas devem ser compostas por evidências (quase) arbitrárias fornecidas pelo usuário, como para uma função$$ , e para contextos em que$g$$$$g$ e $$$f$.Para alcançar essa composição, a especificação do conector é parametrizada através das especificações fornecidas pelo usuário para funções remotas. Dessa maneira, os engenheiros podem raciocinar sobre sua arquitetura fornecendo especificações e evidências para seus componentes e confiar nas especificações do código gerado.

Até o momento, demonstramos esse processo do começo ao fim usando o conector RPC CAmkES especial ( 1 , 2 ). Como os modelos para outros conectores (dataports e eventos) são muito mais simples que os RPCs, não será difícil expandir o gerador de evidências para suportar esses conectores, o que permitirá criar sistemas verificados mais diversos.

Após o código de comunicação, o CAmkES cria a configuração inicial de controle de acesso para aplicar os limites da arquitetura. Para provar que essas duas descrições do sistema - capDL e CAmkES - coincidem, considere a descrição do CAmkES como uma abstração da descrição do capDL. Usamos a estrutura testada anteriormente para derivar a autoridade de um objeto sobre outro da descrição do capDL. Então, aumentaremos as evidências para o nível da política. Além disso, definimos regras para retirar autoridade entre componentes na descrição do CAmkES. Essa prova garante que os objetos capDL representados como um gráfico de privilégios com objetos agrupados por componentes tenham os mesmos limites entre os grupos que no gráfico equivalente do componente CAmkES. Intuitivamente, essa correspondência de limites significa que a análise da arquitetura de política da descrição do CAmkES salvará a política da descrição gerada pelo capDL, que, por sua vez, é garantida para atender aos requisitos de restrição de autoridade, integridade e confidencialidade, conforme mencionado anteriormente.

Por fim, para provar a inicialização correta, o CAmkES usa um inicializador universal que inicia como a primeira tarefa do usuário após o carregamento. No seL4, essa primeira (e única) tarefa do usuário tem acesso a toda a memória disponível, usando-a para criar objetos e “habilidades” de acordo com a descrição detalhada do capDL, que ele aceita como entrada. Está provado queO estado após a execução do inicializador satisfaz o estado descrito na especificação especificada . Essa prova é verdadeira para o modelo inicializador exato, mas ainda não no nível de implementação. Comparada à profundidade do restante da cadeia de evidências, essa limitação pode parecer fraca, mas já é uma evidência mais formal do que a exigida no nível mais alto (EAL7) dos critérios gerais de avaliação de segurança.

Atualização de segurança sísmica

Na prática, é difícil garantir o desenvolvimento de um sistema do zero por questões de segurança; portanto, a capacidade de atualizar software antigo é crucial para o desenvolvimento de sistemas seguros. Nossa estrutura baseada em seL4 suporta um processo iterativo que chamamos de "atualizações de segurança sísmica", pois um arquiteto regular atualiza edifícios existentes para maior estabilidade sísmica. Ilustramos o processo pelo exemplo de adaptação gradual da arquitetura de software existente de um helicóptero não tripulado, passando do esquema de teste tradicional para um sistema altamente confiável com teoremas suportados por métodos formais. Embora este exemplo seja baseado em um projeto ULB real, ele é simplificado aqui e não inclui todos os detalhes.

A arquitetura original do helicóptero coincide com a arquitetura descrita na Fig. 3. Sua funcionalidade é fornecida por dois computadores separados: o computador de navegação controla o voo real e o computador de bordo executa tarefas de alto nível (como se comunicar com uma estação terrestre e navegar pela imagem da câmera). A versão inicial do computador de bordo era um aplicativo monolítico para Linux. Durante o processo de modernização, os engenheiros da Boeing aplicaram os métodos, ferramentas e componentes fornecidos pelos parceiros do HACMS.

Etapa 1. Virtualização

A primeira etapa foi tomar o sistema como ele é e executá-lo em uma máquina virtual sobre um hipervisor seguro (veja a Figura 7). Na metáfora da modernização sísmica, isso corresponde a colocar o sistema em uma base mais móvel. Uma máquina virtual sobre o seL4 neste sistema consiste em um componente CAmkES, que inclui um monitor de máquina virtual (VMM) e um sistema operacional convidado, neste caso o Linux. O kernel fornece abstrações de hardware de virtualização e o VMM gerencia essas abstrações para a máquina virtual. O kernel seL4 limita não apenas o sistema operacional convidado, mas também o VMM, portanto, você não precisa confiar na implementação do VMM para fornecer isolamento forçado. Uma falha no VMM resultará em uma falha do sistema operacional convidado, mas não em todo o sistema.


Fig. 7. Todas as funcionalidades em uma máquina virtual

Dependendo da configuração do sistema, a máquina virtual pode ter acesso aos dispositivos por meio de drivers paravirtualizados, drivers de passagem ou ambos. No caso de drivers de passagem, os desenvolvedores podem usar o MMU ou IOMMU do sistema para evitar a violação dos limites de isolamento por dispositivos e drivers de hardware no sistema convidado. Observe que simplesmente iniciar o sistema em uma máquina virtual não adiciona benefícios adicionais de segurança ou confiabilidade. A etapa 1 é necessária apenas para se preparar para a etapa 2.

Etapa 2. Várias máquinas virtuais

O segundo passo da modernização sísmica fortalece os muros existentes. No software, um desenvolvedor pode aumentar a segurança e a confiabilidade dividindo o sistema de origem em vários subsistemas, cada um dos quais consiste em uma máquina virtual que executa apenas parte do código do sistema de origem. Cada combinação VM / VMM é realizada em um componente CAmkES separado, que introduz isolamento entre diferentes subsistemas, não permitindo que eles se influenciem e, em seguida, permite a coexistência de diferentes níveis de segurança.

Em geral, as seções seguem a arquitetura de software existente, embora se a arquitetura não for suficiente para um isolamento efetivo, pode ser necessário um novo design.

Como regra, as seções devem interagir entre si, portanto, neste ponto, também adicionaremos canais de comunicação. Para garantir a segurança, é imperativo que essas interfaces sejam estreitas, limitando a conexão entre partições apenas ao que é absolutamente necessário. Além disso, os protocolos de interface devem ser eficientes, com um número mínimo de mensagens ou volume de dados. É fundamental que o seL4 permita controlar e limitar a troca de memória entre partições para minimizar a quantidade de dados.

Além das máquinas virtuais que representam os subsistemas do sistema de origem, também extraímos e implementamos componentes para quaisquer recursos compartilhados (como uma interface de rede).

Você pode repetir a etapa 2 até alcançarmos os detalhes desejados das seções. O detalhamento correto é um compromisso entre a resistência do isolamento, por um lado, e os custos gerais de comunicação e reconstrução, por outro.

Em nosso exemplo, temos três seções: uma máquina virtual que implementa as funções de comunicação de uma estação terrestre executando o Linux; outra máquina virtual que implementa funções de navegação baseada em câmera (também executando o Linux); e um componente de compartilhamento de rede nativo, como mostrado na fig. 8)


Fig. 8. Funcionalidade dividida em várias máquinas virtuais

Etapa 3. Componentes Nativos

Quando um sistema é decomposto em seções separadas de uma máquina virtual, algumas ou todas as seções individuais podem ser reimplementadas como componentes nativos, em vez de máquinas virtuais. Isso reduzirá significativamente a superfície de ataque para a mesma funcionalidade. Uma vantagem adicional de converter um componente em código de máquina é reduzir a carga e aumentar a produtividade, removendo o SO convidado e a sobrecarga de execução de código e comunicação do VMM.

Os componentes nativos também aumentam o potencial de aplicação da verificação formal e outros métodos para aumentar a confiabilidade de um componente. As opções são diferentes: da verificação funcional completa do código nativo à geração conjunta de código e evidência, verificação do modelo, uso de linguagens de programação com segurança de tipo, análise estática ou teste rigoroso tradicional de uma base de código menor.

Graças ao isolamento fornecido pelo seL4 e pela arquitetura dos componentes, é possível trabalhar juntos em um sistema de componentes com diferentes níveis de confiabilidade. Nesse caso, os componentes de baixa confiabilidade não reduzem a confiabilidade geral do sistema, e os desenvolvedores se beneficiam do fato de que você não precisa se esforçar para verificar esse código.

Em nosso exemplo, analisaremos a máquina virtual para o canal de comunicação entre o computador de bordo e a estação terrestre em módulos nativos. Nos componentes nativos, as funções de comunicação, criptografia e controle (gerenciador de missão) são implementadas. Deixaremos a câmera e o Wi-Fi na máquina virtual como um componente obsoleto não confiável (veja a Fig. 9). Essa separação se tornou um compromisso entre os esforços para refazer os subsistemas e os benefícios do uso de componentes nativos em termos de desempenho e confiabilidade.


Fig. 9. Funcionalidade implementada em componentes nativos

Etapa 4. Confiabilidade do sistema como um todo

Tendo recebido todos os módulos necessários, daremos o passo final: análise de todo o sistema como um todo, com base na confiabilidade da arquitetura e nos componentes individuais.

Na estrutura do HACMS, a comunicação, a criptografia e um módulo de controle são implementados na linguagem orientada a objetos , provavelmente segura para o tipo Ivory , com alocação de uma quantidade fixa de memória no heap. Sem verificação adicional, o Ivory não nos dá garantias de correção funcional, mas confia na tolerância a falhas e na confiabilidade de emergência. Dado o isolamento dos componentes, acreditamos que essas garantias permaneçam na presença de componentes não confiáveis ​​(como a máquina virtual da câmera).

O componente de rede é implementado no código C padrão, que consiste no código do usuário da plataforma e no código da biblioteca existente. Seu nível de confiabilidade corresponde ao nível obtido através da implementação cuidadosa de códigos conhecidos. A confiabilidade pode ser aprimorada sem muita despesa, usando métodos como a síntese do driver , além de usar linguagens de tipo seguro como o Ivory. Em uma análise geral da segurança do sistema, qualquer comprometimento de um componente de rede afetará apenas pacotes de rede. Como o tráfego é criptografado, esse ataque não comprometerá a condição das especificações de que apenas os comandos autorizados entram no computador de bordo.

A máquina virtual da câmera de vídeo é a parte mais fraca do sistema, pois é executada no sistema Linux e deve conter vulnerabilidades. Mas a VM está isolada; portanto, se os invasores a quebrarem, não poderão passar para outros componentes. A pior coisa que um invasor pode fazer é enviar os dados incorretos para o componente de controle. Como no quadrocóptero, esse componente verifica os dados recebidos da câmera. E ele resistiu com sucesso ao ataque cibernético mencionado no início do artigo. Foi um ataque de “caixa branca”, onde a equipe de Pentesters teve acesso a todo código e documentação, bem como a todos os canais de comunicação externos. Ela recebeu intencionalmente acesso root à máquina virtual da câmera, simulando um ataque bem-sucedido a software desatualizado. A contenção de ataques e a capacidade de defesa contra esse cenário muito poderoso se tornaram um teste valioso de nossos requisitos de segurança e a identificação de quaisquer suposições perdidas, problemas de interface ou outros problemas de segurança que a equipe de pesquisa possa não reconhecer.

Limitações e trabalhos futuros

Este artigo fornece uma visão geral do método para alcançar níveis muito altos de segurança para sistemas nos quais o recurso de segurança é aplicável por meio da arquitetura de componentes. Provamos teoremas para o nível do kernel e sua configuração correta, bem como teoremas que garantem que a plataforma do componente defina corretamente os limites de segurança de acordo com a descrição de sua arquitetura e que gere o código correto para chamadas de procedimentos remotos. A conexão com a análise de segurança de alto nível do sistema permanece informal, e os teoremas do código de comunicação não cobrem todas as primitivas de comunicação fornecidas pela plataforma. Para obter automaticamente um teorema que cubra todo o sistema do começo ao fim, é necessário trabalho adicional. No entanto, nesta fase, é claro que esta é uma tarefa viável.

O principal objetivo do trabalho apresentado é reduzir drasticamente os esforços de verificação para classes específicas de sistemas. A abordagem puramente arquitetural descrita aqui pode ser estendida a outros sistemas que não o ULB, mas é claramente limitada pelo fato de poder apenas expressar propriedades determinadas pela arquitetura de componentes do sistema. Os retornos diminuirão se essa arquitetura for alterada durante a execução do programa e se as propriedades forem criticamente dependentes do comportamento de muitos componentes confiáveis ​​ou componentes de tamanho muito grande.

O primeiro passo para diminuir essas limitações é criar uma biblioteca de componentes pré-testados com um alto nível de confiabilidade para uso como blocos de construção confiáveis ​​nessas arquiteturas. Essa biblioteca pode incluir padrões de segurança (como desinfecção de dados de entrada, filtros de saída, privacidade e monitores de tempo de execução) potencialmente gerados a partir de especificações de nível superior, além de componentes de infraestrutura como módulos criptográficos reutilizáveis, armazenamento de chaves, sistemas de arquivos, Pilhas e drivers de rede altamente confiáveis. Se a segurança depende de mais de um desses componentes, é necessário justificar a confiabilidade de sua interação e compartilhamento. Os principais problemas técnicos aqui são discussões sobre simultaneidade e protocolos, bem como fluxo de informações na presença de componentes confiáveis. Apesar dessas limitações, o trabalho demonstra o rápido desenvolvimento de sistemas reais altamente confiáveis ​​baseados no seL4. Atualmente, a criação de tais sistemas é possível a um custo menor do que os testes tradicionais.

Aplicação: custos trabalhistas

O desenvolvimento do design e código do seL4 levou dois anos-homem. Se adicionarmos todas as evidências específicas do sorotipo, um total de 18 pessoas-ano será obtido para 8700 linhas de código para C. Para comparação, o desenvolvimento de um microkernel L4Ka :: Pistachio de tamanho comparável da família seL4 levou seis homens-ano e não forneceu um nível significativo de confiabilidade. Isso significa uma diferença na velocidade de desenvolvimento de apenas 3,3 vezes entre o software verificado e o tradicional. De acordo com o método de avaliação de Colbert e Bohm , a certificação segundo os critérios tradicionais da EAL7 para 8700 linhas de código C levará mais de 45,9 pessoas-ano. Isso significa que a verificação formal da implementação no nível binário já é 2,3 vezes mais barata que o nível mais alto de certificação, de acordo com os critérios gerais, enquanto fornece confiabilidade significativamente mais alta.

Para comparação, a abordagem HACMS descrita aqui usa apenas evidências existentes para cada novo sistema, incluindo evidências geradas pelas ferramentas. Assim, o esforço geral de prova para um sistema que combina com essa abordagem se resume a semanas-homem, não anos, e o teste se resume apenas a validar suposições.