A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

As aeronaves modernas estão se tornando cada vez mais complexas, dependendo de computadores poderosos para gerenciar tudo, desde controles de voo até navegação e planejamento de missão. Para garantir a segurança, a indústria da aviação utiliza regras rigorosas que exigem que todo software seja testado e verificado para um nível específico de confiança. Para os sistemas mais críticos, como aqueles que mantêm um avião no ar, esse nível de confiança é o mais alto possível. No entanto, um novo desafio surgiu à medida que esses computadores evoluíram de processadores únicos para chips multi-core, semelhantes aos processadores poderosos encontrados em laptops e servidores modernos. Quando múltiplos programas rodam simultaneamente em diferentes núcleos do mesmo chip, eles frequentemente competem pelo acesso a recursos compartilhados, especificamente uma área de memória de alta velocidade chamada cache de último nível (last-level cache). Essa competição pode fazer com que um programa desacelere outro de forma imprevisível, criando uma incerteza de tempo que é perigosa para o software de aviação crítico para a segurança.

Para resolver isso, pesquisadores têm desenvolvido maneiras de isolar esses programas para que eles não interfiram uns nos outros. Uma abordagem promissora envolve um tipo de gerenciador de software, conhecido como hipervisor, que se posiciona entre o hardware e as aplicações, dividindo os recursos do computador em compartimentos separados e seguros. A questão permanece, contudo, se esse isolamento é forte o suficiente para atender aos padrões rigorosos exigidos pela aviação comercial. Uma equipe de pesquisadores da Advanced Micro Devices e da Universidade Técnica de Munique explorou essa questão ao criar um plano detalhado de como certificar um tipo específico de computador multi-core para uso em aeronaves. O trabalho deles foca em uma configuração que utiliza um hipervisor chamado Xen em processadores AMD, combinado com uma técnica chamada coloração de cache (cache coloring), para garantir que diferentes partições de software não possam acidentalmente "pisar no calo" umas das outras.

Os pesquisadores começaram identificando o problema específico: em um processador multi-core, o cache de memória compartilhado é o principal lugar onde ocorre a interferência. Se um programa encher o cache, ele pode forçar outro programa a esperar, causando atrasos que podem perder um prazo crítico. Para evitar isso, a equipe propôs um método onde a memória do computador é dividida em grupos distintos, ou "cores" (cores), baseados em onde os dados residem. Cada programa de software recebe seu próprio conjunto único de cores, e o sistema é configurado para que os dados de um programa nunca substituam os dados de outro no cache. Crucialmente, essa regra também se aplica ao próprio hipervisor. Os pesquisadores garantiram que os próprios dados do gerenciador de software também sejam travados em seu próprio conjunto exclusivo de cores, evitando que ele acidentalmente desaloje os dados dos programas críticos para a segurança que está gerenciando. Isso cria uma garantia construtiva de que a interferência é limitada, o que significa que é matematicamente limitada e previsível, em vez de apenas torcer para que não aconteça.

O artigo apresenta um mapeamento desta configuração técnica para as regras oficiais de certificação usadas pelas autoridades de aviação nos Estados-States e na Europa. Essas regras, conhecidas como DO-178C e AC 20-193, exigem que os requerentes provem que os recursos compartilhados são gerenciados com segurança. Os autores demonstram como sua configuração específica atende a esses requisitos ao mostrar que o mecanismo de coloração de cache isola efetivamente o cache de último nível. Eles também mostram como o próprio caso de segurança do hipervisor, que é documentado separadamente pela comunidade de código aberto, pode ser reutilizado como evidência para o fabricante da aeronave. Isso permite que o fabricante foque em provar que suas aplicações específicas funcionam corretamente dentro desse ambiente isolado, em vez de ter que provar a segurança do hardware de computador subjacente do zero. Os pesquisadores delineiam um caminho claro de como um fabricante de aeronaves poderia usar essa configuração para alcançar uma certificação de segurança de nível médio, conhecida como DAL-B, que é adequada para muitas funções importantes, mas não críticas para a vida.

No entanto, os autores são cuidadosos ao definir os limites de seu trabalho. Eles declaram explicitamente que este plano ainda não prova que o sistema é seguro o suficiente para o nível mais alto de certificação, conhecido como DAL-A, que é exigido para os controles de voo mais críticos. Para atingir esse nível superior, seriam necessários passos adicionais, como provar formalmente com matemática que a ferramenta de alocação de memória nunca comete um erro e reunir mais experiência prática extensa com o processador específico. O artigo também esclarece que não cobre cargas de trabalho de inteligência artificial ou processamento gráfico, que são áreas emergentes que exigiriam soluções diferentes. Além disso, os autores enfatizam que este é um artigo de metodologia, não uma certificação final; ele fornece um argumento estruturado e um conjunto de ferramentas, mas a aprovação real ainda deve vir dos reguladores de aviação, que revisarão os detalhes específicos de cada programa de aeronave.

O cerne da pesquisa é uma demonstração prática de como essas regras de segurança abstratas podem ser aplicadas a uma plataforma de computação do mundo real. A equipe descreveu uma configuração específica onde um computador com quatro núcleos é dividido em partições separadas para diferentes tarefas, como controle de voo, percepção e gerenciamento de missão. Eles mostraram como atribuir a cada partição um núcleo dedicado e uma fatia específica do cache de memória, garantindo que o software de controle de voo sempre tenha os recursos necessários sem ser retardado pelas outras tarefas. Eles também detalharam como o sistema verifica erros na inicialização para garantir que o isolamento de memória esteja funcionando corretamente antes que a aeronave sequer decole. Essa abordagem oferece uma maneira de usar chips de computador poderosos e comercialmente disponíveis na aviação sem sacrificar a previsibilidade e a segurança que a indústria exige.

Ao final, o artigo oferece uma ponte entre a rápida evolução do hardware de computação comercial e o ritmo lento e deliberado da certificação de segurança da aviação. Ele mostra que, com a configuração certa, especificamente usando coloração de cache e um hipervisor de particionamento estático, é possível criar um ambiente de computação onde a interferência é controlada e previsível. Embora o caminho para os níveis mais altos de certificação ainda exija mais trabalho, esta pesquisa fornece uma base sólida para que os fabricantes comecem a integrar esses processadores avançados em suas aeronaves. O trabalho serve como um modelo, demonstrando que os mecanismos técnicos existem para suportar a integração segura de multi-core, desde que as regras específicas e as evidências exigidas pelos reguladores sejam cuidadosamente seguidas e verificadas.