⚡ electrical engineering

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

Este artigo apresenta o ESBMC-Arduino, uma estrutura de verificação fiel ao hardware que preenche a lacavra de implantação para PLCs de hardware aberto ao integrar uma camada de abstração de hardware declarativa e modelagem sonora de intervalo de entrada para eliminar alarmes falsos causados por suposições de inteiros idealizados, enquanto detecta defeitos genuínos dependentes de largura em programas IEC 61131-3 executados em microcontroladores com recursos limitados.

Autores originais: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publicado 2026-07-10

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo um robô para gerenciar um tanque de água. Você escreve as instruções em uma linguagem especial chamada IEC 61131-3, que é como um livro de receitas universal para máquinas industriais. Por anos, engenheiros têm usado simuladores de "super-robô" para verificar se essas receitas são seguras. Esses simuladores são como magos que conseguem pensar com números infinitos; eles assumem que o robô pode guardar qualquer número em sua cabeça, de menos infinito a mais infinito, e que os sensores podem relatar qualquer valor imaginável.

Mas aqui está a reviravolta: o robô real que você constrói não é um mago. É um microcontrolador minúsculo e barato (como um Arduino) que vive no mundo real. Esse pequeno chip tem um cérebro muito específico e limitado. Ele só consegue guardar números até 32.767. Se uma conta ultrapassar esse valor, o número não apenas cresce; ele quebra, volta para o início e se torna um número negativo. É como um odômetro de carro que volta de 999.999 para 000.000.

O Grande Desconecte
O artigo chama isso de "gap de implantação" (deployment gap). É a diferença entre o mundo dos sonhos do mago e a realidade limitada do robô.

Os autores descobriram que, quando os engenheiros usavam os antigos simuladores de "mago" para verificar seu código quanto à segurança, eles recebiam uma quantidade massiva de alarmes falsos. Dos 123 programas reais que testaram, os antigos simuladores gritaram "PERIGO!" 54 vezes (uma taxa de alarme falso de 44%). Mas quando olharam mais de perto, perceberam que esses "perigos" eram impossíveis. Os simuladores estavam imaginando leituras de sensores como -32.764. No mundo real, um sensor conectado a este robô só pode ler números entre 0 e 1.023 (porque é um sensor de 10 bits). Um valor de -32.764 é como um termômetro lendo "menos 32.764 graus" — simplesmente não pode acontecer.

O artigo argumenta que confiar nesses antigos simuladores é como um segurança gritando "Intruso!" porque viu um fantasma. O segurança está tecnicamente "correto" sobre o fantasma, mas é inútil porque fantasmas não existem. Os autores excluem explicitamente a ideia de que você possa apenas verificar erros matemáticos sem também verificar o que os sensores realmente podem ver. Eles mostram que fazer isso torna a verificação "não confiável" (unsound) na prática.

A Solução Mágica: O Descritor HAL
Para corrigir isso, os autores construíram uma nova ferramenta chamada ESBMC-Arduino. Pense nesta ferramenta como um filtro de "Checagem de Realidade".

Antes que o simulador de mago olhe para o código, esta nova ferramenta anexa uma pequena nota automática a cada sensor. Ela diz: "Ei, lembre-se, este sensor só pode dar números entre 0 e 1.023". Ela também lembra ao simulador: "E lembre-se, o cérebro do robô só pode conter números até 32.767".

Quando o simulador roda com essas regras, a mágica acontece:

Os 54 alarmes falsos desaparecem instantaneamente. O fantasma de -32.764 sumiu porque o simulador agora sabe que esse número é impossível.
Os 32 programas que já haviam sido provados seguros continuam seguros.
Mais importante ainda, a ferramenta não perdeu nenhum erro real: ela descobriu que os antigos simuladores estavam escondendo um tipo específico de perigo real: quando uma leitura de sensor é multiplicada por um número grande (como transformar o valor bruto de um sensor em uma porcentagem), a matemática pode transbordar o cérebro minúsculo do robô.

O Perigo Real (e quão raro ele é)
O artigo descobriu que, embora os "alarmes de fantasma" fossem comuns, os erros reais causados por esse gap eram, na verdade, bastante raros no código público que testaram. Eles só encontraram defeitos genuínos em cenários específicos onde uma leitura de sensor era multiplicada por uma constante grande (como 100) em uma placa de 16 bits.

Por exemplo, se um sensor lê 898 (um valor normal e real) e o código o multiplica por 100, o resultado é 89.800. Isso é grande demais para o cérebro de 16 bits do robô (máximo de 32.767). O número dá a volta, torna-se um número negativo, e o robô pensa que o tanque de água está vazio quando, na verdade, está transbordando. A nova ferramenta detectou exatamente esse cenário e forneceu aos engenheiros um exemplo físico real da leitura do sensor que causaria a falha.

O Que o Artigo Não Alega
Os autores são muito honestos sobre o que não fizeram. Eles não provaram que todos os programas agora estão seguros. Dos 123 programas, 91 terminaram com um veredito de "desconhecido". Isso não é porque a ferramenta está quebrada; é porque a matemática para provar a segurança desses programas específicos é difícil demais para o motor atual concluir. A ferramenta removeu com sucesso o ruído (os alarmes falsos) e manteve o sinal (as provas reais), mas não conseguiu resolver os enigmas mais difíceis ainda.

Eles também não testaram isso em números de ponto flutuante (decimais como 3,14) ou simulações físicas complexas. Eles focaram estritamente em números inteiros e lógica booleana (interruptores de liga/desliga).

A Conclusão
O artigo demonstra que, para verificar PLCs de hardware aberto (como os usados em escolas e pequenas fábricas), você não pode apenas verificar a matemática; você tem que verificar os limites do hardware. Ao adicionar automaticamente uma "Checagem de Realidade" que diz ao simulador o que os sensores realmente podem fazer, eles transformaram uma ferramenta barulhenta e não confiável em uma ferramenta digna de confiança. Eles não encontraram um milhão de novos bugs, mas impediram a ferramenta de dar alarmes falsos, tornando possível para os engenheiros confiarem novamente nas verificações de segurança.

Resumo Técnico: ESBMC-ARDUINO

Problema: O Hiato de Implantação em PLCs de Hardware Aberto
Os Controladores Lógicos Programáveis (PLCs) de hardware aberto, como o OpenPLC rodando em Arduino OPTA, CONTROLLINO e Industrial Shields M-Duino, democratizaram a programação IEC 61131-3 para dispositivos de classe microcontrolador de baixo custo. Essas plataformas são cada vez mais utilizadas em educação, automação de pequena escala e como o substrato de tempo de execução para pesquisa de segurança em Sistemas de Controle Industrial (ICS). No entanto, existe um "hiato de implantação" crítico entre os modelos abstratos usados pelos verificadores de código aberto existentes (ex: ESbras-PLC, PLCverif) e o ambiente de execução de hardware real.

Os verificadores atuais operam em um modelo de ciclo de varredura (scan-cycle) abstrato, assumindo inteiros idealizados e ilimitados e entradas não restritas. Em contraste, os artefatos implantados rodam em Unidades de Microcontrolador (MCUs) com recursos limitados, possuindo larguras de palavra de máquina específicas (ex: int de 16 bits em placas AVR de 8 bits) e Conversores Analógico-Digitais (ADCs) de resolução finita (tipicamente 10 bits, resultando em valores no intervalo $[0, 1023]$ ). Essa discrepância leva a dois modos de falha:

Defeitos Omitidos: Um programa pode ser provado seguro no modelo abstrato, mas inseguro no dispositivo devido ao estouro de inteiro (overflow) causado por larguras de palavra estreitas (ex: um cálculo de escalonamento que sofre wrap-around em uma placa de 16 bits).
Alarmes Fantasmas (Falsos Positivos): Mais criticamente, a verificação consciente da largura que considera a largura da palavra, mas ignora os limites de entrada do hardware, explora valores de sensores que nenhum ADC físico poderia produzir (ex: valores negativos ou valores superiores a 1023). Isso resulta em relatórios de estouro espúrios. A avaliação em um corpus de 123 programas de terceiros mostrou que a verificação de estouro de 16 bits ingênua gera uma taxa de falso alarme de 44% (54/123), enquanto encontra zero defeitos genuínos.

Metodologia: Verificação Fiel ao Hardware
O artigo propõe um método para fechar esse hiato construindo um "modelo de implantação" ( $M_{dev}$ ) que represente fielmente o hardware alvo. O núcleo desta abordagem é um descritor de Camada de Abstração de Hardware (HAL) e um processo de redução (lowering) consistente.

Descritor HAL ( $H$ ): Uma tupla declarativa $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ que captura:
- $w$ : A largura da palavra de máquina (ex: 16 bits para AVR, 32 bits para ARM).
- $b_{adc}$ e $b_{pwm}$ : A resolução dos Conversores Analógico-Digitais e das saídas de Modulação por Largura de Pulso (PWM).
- $\mu$ : Um mapa de vinculação de E/S derivado automaticamente do esquema de endereçamento direto da IEC 61131-3 (ex: endereços %IW mapeiam para entradas analógicas com intervalos de ADC específicos).
Redução Fiel (Faithful Lowering): O método transforma o programa PLC ( $P$ $P$ ) em um modelo de implantação ( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ ) ao:
- Interpretar a aritmética na largura de palavra alvo $w$ (reproduzindo exatamente o wrap-around de complemento de dois).
- Injetar restrições assume imediatamente após a amostragem de entrada para restringir as variáveis aos seus intervalos realizáveis pelo hardware (ex: $0 \leq adc \leq 1023$ ).
- Sobre-aproximar blocos de funções não lineares (ex: PID) com saídas não determinísticas para manter a tratabilidade.
Mecanismo de Verificação: O método reutiliza o backend do ESBMC (Bounded Model Checking baseado em SMT e $k$ -indução) sem modificações. A redução ocorre no frontend de Diagrama de Escada (LD), adicionando um gancho leve (aprox. 40 linhas) que impõe os limites de entrada e define a largura de palavra da arquitetura.

Principais Contribuições

Método de Verificação Fiel ao Hardware: Uma abordagem formal que transfere a disciplina de alvo-modelo da segurança de sistemas embarcados em C (estabelecida por ferramentas como Frama-C e Astrée) para o domínio PLC. Diferente dessas ferramentas, que exigem contratos de entrada manuais, este método deriva automaticamente os limites de entrada a partir do esquema de endereçamento padrão IEC 61131-3 e dos descritores da placa.
Instanciação ESBMC-Arduino: Uma implementação concreta para alvos da classe Arduino, obtendo parâmetros HAL de núcleos oficiais do Arduino. Suporta alvos de 16 bits (AVR) e 32 bits (ARM).
Avaliação Empírica: Uma avaliação rigorosa em 123 programas reais e um corpus controlado de 20 padrões.

Resultos

Eliminação de Falsos Alarmes: No corpus de 123 programas, habilitar o anotador HAL eliminou todos os 54 falsos alarmes (reduzindo a contagem de inseguros de 54 para 0) enquanto preservou cada prova de robustez (32 programas permaneceram provados seguros).
Detecção de Defeitos Genuínos: Um corpus controlado demonstrou que o método detecta defeitos genuínos dependentes de largura (ex: estouro no escalonamento de ADC para porcentagem em placas de 16 bits) com testemunhas fisicamente realizáveis.
Validação Cruzada entre Ferramentas: O fenômeno dos "alarmes fantasmas" foi reproduzido usando ferramentas independentes (CBMC e Frama-C/EVA) em espelhos C da lógica, confirmando que o problema é inerente à verificação ingênua consciente da largura sem modelagem de entrada, e não específico ao ESBMC.
Desempenho: O overhead do anotador HAL é negligenciável; os tempos de verificação permanecem abaixo de um segundo por programa.
Limitações: Embora os falsos alarmes sejam eliminados, 91 programas no corpus real retornaram vereditos "desconhecidos" devido à incompletude da $k$ -indução em blocos de função com estado interno. Esta é uma limitação da capacidade do provador de fechar passos indutivos, não do modelo de entrada.

Significância
O artigo argumenta que o principal valor deste trabalho não é a contagem de bugs descobertos (que são raros nos corpora públicos específicos pesquisados, dominados por lógica Booleana e de temporização), mas sim a restauração da correção (soundness). Os autores demonstram que a verificação ingênua consciente da largura é inutilizável para garantia devido a uma taxa de falso alarme de 44% que abafa descobertas genuínas. Ao derivar automaticamente os intervalos de entrada realizáveis pelo hardware, o método converte uma ferramenta não confiável em uma que emite apenas relatórios realizáveis, permitindo que engenheiros confiem nos resultados de verificação para PLCs de hardware aberto. A abordagem é apresentada como uma estratégia de adoção realista e de baixo custo (um descritor de 4 campos e um gancho de 40 linhas) que se integra à infraestrutura de verificação madura em vez de exigir uma proposta do zero.

Mais como este