💬 NLP

Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

Este artigo apresenta o ESBMC-LLB, um framework de verificação formal que estende o ESBMC-PLC+ para detectar Bombas de Lógica de Escada em programas de CLP IEC 61131-3 ao expor a lógica oculta de blocos de função e sintetizar gatilhos, alcançando taxas de detecção quase perfeitas e robustez contra gatilhos adaptativos em conjuntos de dados públicos onde os métodos existentes falham.

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 um Controlador Lógico Programável (CLP) como o cérebro de uma fábrica, executando constantemente um ciclo: ele observa sensores, toma uma decisão, move uma máquina e depois começa tudo de novo em uma fração de segundo. Agora, imagine um hacker sorrateiro escondendo uma "bomba lógica" dentro desse cérebro. Essa bomba é como um dragão adormecido; ela não faz nada enquanto a fábrica funciona normalmente, mas no momento em que uma condição específica e oculta acontece (como um contador atingindo um determinado número), ela acorda e causa o caos — seja travando a máquina, mentindo sobre as leituras dos sensores ou fazendo uma válvula abrir quando deveria permanecer fechada.

Por muito tempo, as ferramentas usadas para verificar esses cérebros de fábrica tinham um ponto cego. Elas olhavam para o código principal, mas ignoravam os "blocos de função" — que são como pequenas sub-rotinas ou mini-programas dentro do código principal. O artigo explica que os dragões adormecidos (as bombas) estavam se escondendo dentro desses blocos de função ignorados. Como as ferramentas antigas descartavam esses blocos de sua visão, o código malicioso e o código seguro pareciam exatamente iguais para o verificador. Era como tentar encontrar um espião em uma multidão olhando apenas para os rostos das pessoas, enquanto o espião se escondia dentro de um casaco que o verificador nem sequer olhava.

A Grande Correção: Abrindo o Casaco
Os autores, Pierre Dantas, Lucas Cordeiro e Waldir Junior, construíram um novo método chamado ESBMC-LLB. O truque principal deles foi simples, mas poderoso: eles fizeram o verificador olhar dentro dos blocos de função. Eles adicionaram uma "camada de tradução" que pega o código oculto dentro desses blocos e o estende de forma plana para que o verificador possa vê-lo.

Uma vez que o código está visível, eles usam dois truques inteligentes para pegar a bomba:

O Cronômetro (Scan-Watchdog): Se a bomba tentar travar a máquina fazendo o programa rodar em um loop infinito, o verificador age como um árbitro rigoroso com um cronômetro. Ele diz: "Você tem 100 passos para terminar esta tarefa. Se passar disso, está fora!" Se a bomba tentar rodar em loop para sempre, o verificador a pega imediatamente.
O Testador de Fios (Output Wiring): Se a bomba tentar mentir sobre um sensor ou forçar uma máquina a se mover, o verificador conecta os fios do código oculto ao sistema principal. Se o código oculto tentar enviar uma "mentira" (como dizer para uma válvula abrir quando não deveria), o verificador vê que isso quebra as regras de segurança.

O Resultado Mágico: Encontrando o "Código Secreto"
Aqui está a parte mais legal. Quando o verificador encontra uma bomba, ele não diz apenas "Erro!". Ele realmente cospe o gatilho exato. É como se o verificador dissesse: "Eu encontrei o dragão, e aqui está a senha secreta que o acorda: 'Se o contador atingir 12'". Isso é chamado de "síntese de gatilho".

O Quão Bem Funcionou?
A equipe testou seu método em vários conjuntos de dados, e os resultados foram impressionantes, mas com algumas limitações importantes:

O Teste Público: Em um conjunto de dados famoso de 60 programas (30 seguros, 30 com bombas), seu método encontrou todas as 30 bombas. Ele pegou cada uma delas e encontrou o gatilho secreto para cada uma. Também provou que os 29 programas seguros eram verdadeiramente seguros. Um programa seguro era tão complexo que o verificador não pôde ter 100% de certeza (ele disse "não sei" em vez de "seguro"), mas não acusou falsamente.
O Teste do Hacker "Esperto": Eles tentaram enganar o sistema escondendo o gatilho em enigmas matemáticos (como usar um cálculo complexo em vez de um número simples). As ferramentas antigas que apenas procuram por padrões perderam essas armadilhas. O ESBMC-LLB, no entanto, entendeu o significado da matemática e pegou todas as 5 dessas versões traiçoeiras.
O Teste de Grande Escala: Eles geraram 310 programas (155 seguros, 155 com bombas) para testar a velocidade. O sistema pegou 100% das bombas em uma média de 70 milissegundos (isso é mais rápido que um piscar de olhos!).
O Teste do Mundo Real em uma Planta de Água: Eles testaram isso em uma simulação real de uma planta de tratamento de água (o corpus SWaT).
- Na versão mais antiga dos dados (com gatilhos de matemática simples), eles encontraram 149 de 150 bombas (99%) com zero alarmes falsos.
- O Limite: Quando testaram uma versão mais nova com matemática não linear muito complexa (como multiplicar um número por si mesmo repetidamente), o sistema travou. A matemática era difícil demais para o verificador resolver a tempo, e a detecção caiu para 49%. O artigo é muito claro aqui: seu método é ótimo para lógica padrão e matemática simples, mas encontra um limite com matemática não linear complexa. Nesses casos específicos, um tipo diferente de ferramenta (chamado detector de triagem CFG) ainda é melhor.

O Que Eles Não Reivindicam
Os autores são muito honestos sobre o que sua ferramenta não consegue fazer. Eles declaram explicitamente que, se uma bomba for projetada para terminar sua tarefa rapidamente (sem rodar em loop infinito) e não quebrar nenhuma regra de segurança específica que eles instruíram o verificador a observar, a ferramenta pode falhar. Não é uma varinha mágica que encontra todas as coisas ruins possíveis; ela encontra aquelas que ou travam o sistema ou quebram as regras de segurança que eles definiram.

A Conclusão
Este artigo mostra que, ao simplesmente "abrir o casaco" para olhar dentro dos blocos de função e usar um verificador inteligente que entende o significado do código, podemos pegar bombas industriais sorrateiras que costumavam se esconder à vista de todos. Ele encontra as bombas, diz exatamente como acioná-las (para que possamos pará-las) e prova que o resto do sistema é seguro — a menos que a matemática fique louca demais, caso em que precisamos de um tipo diferente de detetive. Os autores apresentam isso como uma nova ferramenta poderosa que trabalha junto com os métodos existentes, não uma que substitui tudo.

Resumo Técnico: Detecção de Bombas de Lógica de Escada em Programas PLC IEC 61131-3 Usando ESBMC-PLC+

1. Definição do Problema

Controladores Lógicos Programáveis (PLCs) são a espinha dorsal de Sistemas de Controle Industrial (ICS) críticos para a segurança. Uma ameaça específica, a Bomba de Lógica de Escada (Ladder Logic Bomb - LLB), envolve a inserção de lógica de controle maliciosa que permanece dormente durante a operação normal e os testes de comissionamento. A bomba é ativada apenas quando uma condição de gatilho (trigger) específica é atendida, executando uma carga útil (payload) que manipula atuadores, forja leituras de sensores ou nega o controle do operador (ex: via não terminação).

Os métodos de detecção existentes enfrentam duas limitações primárias:

Cegueira Estrutural: Muitas LLBs escondem-se dentro de corpos de Blocos de Função (Function Blocks - FB). Verificadores de Diagrama de Escada (LD) padrão costumam descartar os corpos dos FBs de sua Representação Intermediária (IR) para simplificar a verificação, tornando a lógica maliciosa invisível ao provador.
Falta de Garantias Não Limitadas: Detectores baseados em assinaturas ou triagem de Grafo de Fluxo de Controle (CFG) dependem de padrões sintáticos. Eles podem ser evitados por gatilhos adaptativos (ex: valores computados, aritmética opaca) e não podem fornecer provas formais da ausência de bombas em todos os possíveis ciclos de varredura (scan cycles).

2. Metodologia: ESBMC-LLB

Os autores apresentam o ESBMC-LLB, um método que reaproveita o verificador ESBC-PLC+ existente (um model checker IEC 61131-3 usando vetores de bits SMT e $k$ -indução) para detectar LLBs. A abordagem não modifica o backend de verificação, mas introduz uma camada de modelagem leve no frontend para expor a lógica oculta e recategorizar a detecção como uma verificação de propriedade de segurança formal.

Componentes Principais

Tradução do Corpo do Bloco de Função (Function-Block-Body Translation):
- Os autores observam que os verificadores de LD existentes descartam os corpos dos FBs. O ESBMC-LLB analisa os corpos dos FBs definidos pelo usuário e os traduz em código GOTO nativo (atribuições, loops, comparações).
- Isso garante que a lógica maliciosa residente nos FBs esteja presente na IR e seja alcançável pelo provador.
Mecanismos de Detecção:
O método mapeia payloads de LLB para violações de segurança específicas:
- Watchdog de Varredura (para Negação de Controle/Não Terminação): Um contador de iteração limitado é assertado dentro de cada loop de degrau (rung loop), fiel a um temporizador de watchdog de um PLC real. Se um payload controlado por gatilho entra em um loop de não terminação, ele viola a restrição de orçamento, tornando-se uma violação de segurança alcançável.
- Fiação de Saída (para Falsificação de Atuador/Sensor): Os pinos de saída dos FBs são conectados às variáveis do programa que os consomem. Se um payload forja um valor, este se propaga pelo programa e viola uma propriedade de segurança fornecida (ex: exclusão mútua de atuadores intertravados).
Resultados de Verificação:
- $k$ -Indução: Se o programa for benigno, a $k$ -indução fornece uma prova não limitada de que a propriedade de segurança se mantém para todos os ciclos de varredura, certificando a ausência de bombas da classe modelada.
- Modelagem de Verificação Limitada (Bounded Model Checking - BMC): Se uma bomba estiver presente, o BMC retorna um rastro de contraexemplo. Este rastro constitui o gatilho de detonação (a sequência de entrada específica e a contagem de ciclos de varredura), permitindo a síntese automática do gatilho.

3. Principais Contribuições

O artigo descreve cinco contribuições primárias:

Exposição de Lógica Oculta: Uma camada de modelagem que traduz corpos de FB para a IR do verificador, tornando alcançável a bomba anteriormente indetectável residente em FBs.
Detecção Dupla com Síntese de Gatilho: Mecanismos para detectar tanto a não terminação (via watchdog de varredura) quanto a falsificação de valores (via fiação de saída), onde o contraexemplo do BMC recupera automaticamente o gatilho de detonação.
Robustez contra Adversários Adaptativos: Como o método raciocina sobre a semântica do programa em vez de padrões sintáticos, ele detecta gatilhos projetados para evitar a triagem baseada em CFG (ex: constantes computadas, acumuladores multivariáveis de varredura).
Avaliação Abrangente:
- Validação de Terceiros: 100% de detecção no dataset público de Iacobelli et al. (30 programas maliciosos).
- Escalabilidade: 100% de recall e zero falsos positivos em um corpus de taxonomia Booleana/inteira de 310 programas (tempo médio de execução de 70ms).
- Benchmark de Mundo Real: A primeira avaliação de um model checker semântico no benchmark analógico PLC-Defuser SWaT.
Caracterização do Trade-off Semântica vs. CFG: Uma delineação clara de onde a verificação de modelo semântica se destaca (lógica Booleana/inteira, analógica linear, provas não limitadas) versus onde a triagem de CFG retém a vantagem (não terminação analógica não linear).

4. Resultados Experimentais

Lógica Booleana e Inteira

Dataset Iacobelli: Detectou todos os 30 programas maliciosos (100% de recall) com zero falsos positivos. O único programa benigno reportado como "UNKNOWN" não foi um falso positivo, mas uma limitação do passo indutivo sobre o estado inteiro.
Gatilhos Adaptativos: Detectou com sucesso 5/5 variantes de uma bomba onde o gatilho estava oculto via valores computados, potenciação, fatoração ou acumulação temporal, enquanto um proxy de triagem de CFG detectou apenas a linha de base ingênua (1/5).
Escalabilidade: Em um corpus gerado de 310 programas (Booleano/inteiro), o método alcançou 100% de recall e zero falsos positivos com um tempo médio de detecção de 70ms.

Controle Analógico (Benchmark SWaT)

Os autores avaliaram o método no corpus PLC-Defuser SWaT (planta de tratamento de água segura), que envolve lógica não-booleana (REAL/INT).

Parsing Habilitado: Uma extensão de modelagem analógica (suportando tipos REAL e bobinas não-booleanas) permitiu que o corpus fosse analisado pela primeira vez por um model checker semântico.
Gatilhos Lineares (v1.0.0): No release arquivado contendo bombas de não terminação de gatilho linear, o ESBMC-LLB detectou 149/150 (99%) dos programas maliciosos com zero falsos positivos.
Gatilhos Não Lineares (Snapshot de Dev): Em uma versão posterior contendo bombas de não terminação de aritmética não linear (ex: $i := i*i$ ), a detecção caiu para 49%. O backend SMT sofreu timeout ao ser forçado a raciocinar sobre aritmética não linear através do unrolling de loops.
Comparação: Os autores observam que, na não terminação analógica não linear, os detectores de triagem de CFG (como o PLC-Defuser) mantêm a vantagem, enquanto a verificação de modelo semântica lidera em lógica Booleana/inteira e controle analógico linear.

5. Significância e Alegações

O artigo posiciona o ESBMC-LLB não como um substituto para todos os detectores existentes, mas como uma abordagem complementar que preenche lacunas específicas no cenário de verificação de segurança:

Garantias Não Limitadas: Diferente de scanners de assinatura ou model checkers limitados, o ESBC-LLB pode fornecer uma prova formal de que nenhuma bomba de uma classe específica existe em todos os ciclos de varredura.
Síntese Automática de Gatilho: Ele não apenas sinaliza um programa como malicioso; ele gera a sequência exata de entradas necessária para detonar a bomba, auxiliando na análise forense.
Robustez à Ofuscação: É imune a técnicas de ofuscação sintática que derrotam a triagem baseada em CFG.
Limitações Modestas: Os autores explicitamente reconhecem que a abordagem é sólida (sound), mas não completa para todos os tipos de payload. Ela é limitada a payloads que ou falham em terminar ou violam uma propriedade de segurança especificada. Além disso, apresenta dificuldades com aritmética não linear em contextos analógicos, onde atualmente fica atrás dos métodos de triagem estrutural de CFG.

O trabalho conclui que a verificação de modelo semântica e a triagem de CFG são complementares: a primeira fornece provas não limitadas e robustez para lógica Booleana/inteira e analógica linear, enquanto a segunda permanece superior para lidar com a não terminação analógica não linear. A ponte entre essas abordagens (ex: via sumarização de loop ou verificações híbridas guiadas por CFG) é identificada como uma direção promissora para pesquisas futuras.