Composable Post-Quantum Security for FADEC-Coupled Dual-Spool Turbofan Cyber-Physical Systems

Resumo Técnico: Segurança Pós-Quântica Componível para Sistemas Ciber-Físicos de Turbojato de Duplo Eixo Acoplados a FADEC

Declaração do Problema
O artigo aborda a lacuna matemática entre a criptografia pós-quântica (PQC) e sistemas de controle aeroespacial críticos para a segurança, especificamente o Controle Digital de Motor de Autoridade Total (FADEC) acoplado a motores turbojato de duplo eixo. A literatura existente trata tipicamente a segurança criptográfica (por exemplo, encapsulamento de chaves baseado em reticulados, criptografia autenticada) e a estabilidade teórica de controle (por exemplo, margem de bombeamento, aceleração do eixo, conformidade torsional) como domínios independentes. Essa separação falha em contabilizar como fatores específicos da PQC — como expansão de texto cifrado, comprimento de transcrição de atestado e restrições de entropia de renovação de chaves — interagem com a escalabilidade de barramento em tempo real, latência de comunicação e estabilidade da planta física. Os autores argumentam que, em arquiteturas críticas para a segurança, um sistema pode ser autenticado criptograficamente, mas falhar em ser "componivelmente seguro" se a sobrecarga criptográfica violar margens de tempo ou estabilidade.

Metodologia
Os autores desenvolvem uma formulação matemática unificada dentro de um modelo híbrido estocástico, onde a evolução da planta, latência de comunicação, vazamento, qualidade do canal adversário e estado criptográfico evoluem sob uma filtração comum. A metodologia central envolve:

1. Modelo de Sistema Unificado: O sistema-alvo é modelado como uma tupla acoplada $S_\lambda$ compreendendo um modelo estocástico do motor ($P_{eng}$), um controlador FADEC, um barramento de aviônicos abstrato ($B_{bus}$), um canal de comunicação consciente de radar ($C_{ch}$), uma fonte de Função Física Incloneável (PUF) e primitivas pós-quânticas (KEM, AEAD, provas de conhecimento zero).
2. Domínio de Parâmetros Acoplados: A análise trata o estado do sistema como um conjunto produto $\Theta_{tot} = \Theta_{pq} \times \Theta_{puf} \times \Theta_{aead} \times \Theta_{bus} \times \Theta_{radar} \times \Theta_{eng} \times \Theta_{filt}$. Em vez de otimizar essas fatias independentemente, o modelo certifica-as em um único conjunto admissível.
3. Modelo de Ameaça: O adversário é uma entidade probabilística de tempo polinomial capaz de observar tráfego público, obter vazamento limitado de canal lateral (modelado via entropia mínima suave e divergência de Rényi) e injetar falhas transitórias abstratas. O modelo exclui explicitamente instruções procedimentais para atacar hardware real.
4. Tratamento Analítico Defensivo: O artigo utiliza frameworks de Composabilidade Universal (UC) para definir funcionalidades ideais para renovação de chaves, autenticação e integridade, provando depois que o protocolo real realiza essas funcionalidades apenas quando predicados específicos de estabilidade e escalabilidade são atendidos.

Principais Contribuições
O artigo fornece um "sistema de teoremas acoplados" demonstrando que a migração para PQC no controle aeroespacial não pode ser avaliada apenas por tamanhos de chaves ou dureza assintótica. As principais contribuições técnicas incluem:

• Impacto de Radar e Doppler na Renovação de Chaves: Os autores derivam que a incerteza da seção de choque de radar e a atenuação Doppler reduzem a capacidade do canal adversário, mas simultaneamente aumentam a perda de entropia ($\Delta H_{ch}$). Isso estreita o período admissível de renovação de chaves ($T_{key}$), forçando renovações mais frequentes em ambientes de alta incerteza.
• Expansão de Texto Cifrado e Escalabilidade: O artigo prova que a expansão de texto cifrado pós-quântico (especificamente $O(\lambda \log \lambda)$ para KEMs baseados em reticulados) aumenta diretamente os tempos de resposta do barramento ($R_i$). Essa expansão pode empurrar a latência total além da "janela de atuação criptográfica" ($W_{act}$), fazendo com que o sistema rejeite comandos válidos para preservar a segurança.
• Vazamento Físico e Entropia: O modelo vincula parâmetros físicos à entropia criptográfica. Especificamente, perturbações no diâmetro da ponta da pá ($\delta_{tc}$) e telemetria de vibração do eixo são mostradas atuando como canais de vazamento, reduzindo a entropia mínima suave de chaves derivadas de PUF e necessitando de limiares de alarme conservadores.
• Margens de Estabilidade sob Latência: Os autores estabelecem um limite de estabilidade entrada-para-estado (ISS) induzido por latência. Eles mostram que o atraso autenticado total ($\delta_{tot}$) corrói a taxa de decaimento exponencial do sistema de malha fechada, com a margem reduzida ainda mais pela saturação do fluxo de combustível.
• Separação entre Autenticação e Componibilidade: Um resultado teórico crítico (Contraexemplo 1) demonstra que um sistema pode possuir autenticação criptográfica perfeita (zero falsificação, zero vazamento) e ainda assim falhar em ser componivelmente seguro se prazos em tempo real forem perdidos devido ao tamanho da carga útil criptográfica.

Resultados
O artigo deriva várias desigualdades e limites formais:

• Limite Segurança-Estabilidade: É estabelecida uma condição suficiente para liberação componível onde a vantagem de distinção é limitada pela soma dos erros criptográficos ($\epsilon_{kem}, \epsilon_{aead}, \dots$) mais a probabilidade de perda de prazos ($\epsilon_{bus}$) e violações de margem de estabilidade ($\epsilon_{st}$).
• Política de Renovação: O período de renovação de chaves é mostrado como uma função das taxas de vazamento de canais laterais, vibração e incerteza de radar: $T_{key} \leq \frac{H^\epsilon_\infty(K_0) - \kappa_{min}}{\dot{\ell}_{side} + \dot{\ell}_{vib}|\delta_{tc}| + \dot{\ell}_{ch}}$.
• Desigualdade de Escalabilidade: O artigo prova que, para uma tarefa ser escalável, a latência total (resposta do barramento + verificação + atraso de propagação) deve ser menor que o mínimo entre o prazo de controle, limites de aceleração do eixo, limites de erosão da margem de bombeamento e requisitos de amostragem torsional.
• Análise de Sensibilidade: A avaliação simbólica mostra que o aumento do tamanho do texto cifrado ($L_{kem}$) reduz monotonicamente a folga de tempo e as margens de estabilidade, enquanto o aumento da incerteza de radar ($V_\Sigma$) acelera os requisitos de renovação de chaves.

Significância e Alegações
O artigo alega modestamente fornecer um envelope de garantia matemática em vez de um novo controlador, barramento ou primitiva criptográfica. Sua significância reside em:

1. Definir o Acoplamento: Caracteriza explicitamente como segurança pós-quântica, escalabilidade em tempo real e estabilidade de malha fechada interagem no controle aeroespacial crítico para a segurança.
2. Identificar Modos de Falha: Identifica regimes de parâmetros específicos onde uma "atualização criptográfica plausível" (por exemplo, textos cifrados PQC maiores) consome a folga de tempo e estabilidade necessária para o controle seguro de propulsão.
3. Escopo Defensivo: Os autores enfatizam que o modelo é uma ferramenta analítica defensiva. Não fornece orientação operacional para interferir em plataformas reais, nem substitui artefatos de certificação de motores. Em vez disso, define acoplamentos auditáveis matematicamente que processos de certificação podem instanciar e desafiar.

O trabalho conclui que a migração pós-quântica no controle aeroespacial crítico para a segurança requer um "envelope acoplado segurança-estabilidade-latência" formulado em relação a uma superfície de ataque observável explícita, em vez de uma simples substituição de algoritmos criptográficos.