From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Título: Da Tipagem de Alto Nível para Monitores de Baixo Nível: Síntese de Verificadores de Runtime para MAVLink

Autores: Arthur Amorim, Paul Gazzillo, Max Taylor e Lance Joneckis.
Contexto: Segurança de Veículos Aéreos Não Tripulados (UAVs), Verificação de Runtime, Tipos de Sessão.

1. O Problema

Os protocolos de comunicação padrão para UAVs, como o MAVLink, são eficientes em largura de banda, mas carecem de mecanismos para impor a validade contextual de sequências de mensagens.

• Vulnerabilidade: O MAVLink define a sintaxe das mensagens, mas não a semântica (lógica de execução). Isso permite ataques "furtivos" (stealthy attacks), onde um ator malicioso envia comandos sintaticamente corretos, mas semanticamente fora de ordem ou em momentos inadequados (ex: enviar um comando de missão sem a contagem correta de itens), levando a estados inseguros sem disparar detectores de anomalia física.
• Limitações de Soluções Anteriores:
  • Detecção baseada em física: Métodos como o R2U2 comparam dados de sensores a modelos físicos, mas falham em detectar ataques lógicos onde o comportamento físico permanece nominal.
  • DATUM (Trabalho Prévio): Utilizava Tipos de Sessão Multiparte Refinados (RMPSTs) globais para especificação e verificação. No entanto, sofria de duas falhas críticas:
    1. Carga de Especificação: A verificação intrínseca exigia que os usuários fornecessem termos de prova, argumentos acumuladores e histórico de rótulos manualmente, obscurecendo a lógica do protocolo e tornando a compilação lenta.
    2. Incompatibilidade de Desempenho: O backend de extração para OCaml introduzia um runtime gerenciado (coleta de lixo, overhead de memória RSS) incompatível com microcontroladores de recursos limitados em UAVs.

2. Metodologia: O Framework Platum

O artigo apresenta o Platum (Performant Lightweight Assured Typed Universal Messaging), um framework que separa a especificação da verificação de bem-formação e sintetiza monitores diretamente em C.

• DSL Minimalista: O usuário fornece apenas os cinco componentes semânticos de um tipo de sessão global: emissor, receptor, rótulo, variável de payload e predicado de refinamento. Não há necessidade de termos de prova ou scaffolding de verificação na interface do usuário.
• Verificação Extrínseca via Meta-F:*
  • Após a definição do tipo de sessão, o framework utiliza procedimentos de decisão reflexivos no Meta-F* para inspecionar a AST (Árvore de Sintaxe Abstrata).
  • São verificadas quatro invariantes estruturais algoritmicamente:
    1. Unicidade de Rótulos: Garante ausência de não-determinismo.
    2. Recursão Guardada: Evita loops internos infinitos sem comunicação.
    3. Progresso Global: Garante que o protocolo não fique "preso" (stuck).
    4. Fidelidade da Sessão: Garante que todas as transições levem a estados definidos.
• Síntese Direta para C (FSM):
  • Diferente de cadeias de extração genéricas (como Low*), o Platum traduz diretamente a AST confirmada em Máquinas de Estados Finitos (FSMs) planas em C.
  • Os predicados de refinamento (lógica dependente de dados) são transformados em instruções condicionais if/else em C.
  • O resultado é um código sem alocação dinâmica, sem coleta de lixo e com tempo de execução determinístico, pronto para microcontroladores ARM.
• Arquitetura de Implantação: O monitor sintetizado é implantado como um proxy centralizado na fronteira de comunicação entre a Estação de Controle no Solo (GCS) e o UAV, interceptando e validando o tráfego antes de retransmiti-lo.

3. Principais Contribuições

1. DSL Global RMPST Minimalista: Uma linguagem de especificação que exige apenas os cinco componentes semânticos, eliminando a carga de prova manual exigida por abordagens intrínsecas.
2. Pipeline de Síntese Direta para C: Um mecanismo que converte tipos de sessão refinados em FSMs C estáticos, eliminando a dependência de runtimes gerenciados (como OCaml) e permitindo implantação em hardware embarcado restrito.
3. Verificação Algorítmica via Reflexão: Uso de procedimentos de decisão no Meta-F* para validar invariantes estruturais em tempo de compilação, garantindo que apenas especificações bem-formadas gerem código.
4. Validação Empírica: Demonstração de que é possível obter garantias formais de segurança sem sacrificar o desempenho em tempo real.

4. Resultados e Avaliação

A avaliação foi realizada através de simulação SITL (Software-In-The-Loop) com o ArduPilot, comparando o Platum (C) com o DATUM (OCaml) no cenário de upload de missão.

• Latência:
  • O Platum reduziu a latência total do sistema em 4x em comparação ao DATUM.
  • Latência do Monitor (C): ~3.88 µs (ativa).
  • Latência Total do Sistema (Platum): 13.33 µs vs. 56.74 µs (DATUM).
• Consumo de Memória (RSS):
  • O Platum apresentou um aumento de RSS de apenas 8.39 MB (majoritariamente devido ao overhead do Python no teste de proxy, não ao monitor C).
  • O monitor C em si requer apenas algumas centenas de bytes.
  • O DATUM exigiu um aumento de mais de 13.72 MB devido ao runtime do OCaml.
• Determinismo: Ao eliminar o coletor de lixo (GC) do OCaml, o Platum oferece tempos de execução previsíveis, essenciais para loops de controle em tempo real de UAVs.

5. Significado e Conclusão

O trabalho demonstra que é viável utilizar Tipos de Sessão Refinados Globais como linguagem de especificação para segurança de protocolos UAV, superando as barreiras de usabilidade e desempenho que impediam sua adoção prática.

• Segurança Lógica: O Platum fecha a lacuna entre a detecção física e a lógica, impedindo ataques que exploram falhas na ordem ou no contexto das mensagens.
• Viabilidade Embarcada: Ao sintetizar código C plano e livre de alocação, o framework torna possível a execução de verificadores formais complexos diretamente em controladores de voo com recursos limitados (ex: STM32), sem a necessidade de modificar o firmware do UAV ou depender de correções da equipe de desenvolvimento do protocolo.
• Futuro: O trabalho abre caminho para a extensão desse modelo para outros subprotocolos do MAVLink e para a exploração de verificações de runtime descentralizadas.

Em suma, o Platum transforma especificações formais de alto nível em monitores de baixo nível de alta performance, oferecendo uma solução prática e verificada para a segurança de comunicações de UAVs.