An Approach for Safe and Secure Software Protection Supported by Symbolic Execution

Este artigo apresenta um método inovador de proteção de software para sistemas de controle industrial que utiliza Funções Fisicamente Inimitáveis (PUFs) para vincular o programa ao hardware e emprega execução simbólica para garantir a preservação de propriedades de segurança e resistir à engenharia reversa.

O essencial

Imagine que você tem uma receita secreta de bolo muito especial, a "Receita da Vovó". Você quer vender essa receita para uma padaria específica, mas tem medo de que alguém a copie e venda para todos os outros, ou pior, que tentem recriar a receita sem você.

O problema é que, no mundo digital, copiar um software é como fotocopiar uma página: é instantâneo e perfeito. Se você apenas proteger o arquivo, um hacker pode copiá-lo e rodá-lo em qualquer computador.

Este artigo apresenta uma solução inteligente para esse problema, focada em software industrial (como o que controla máquinas de fábrica, semáforos ou robôs). A ideia é fazer com que o software só funcione corretamente na máquina "certa" e, se for copiado para outra, ele continue funcionando, mas de um jeito estranho e aleatório, sem quebrar nada.

Aqui está a explicação passo a passo, usando analogias do dia a dia:

1. A "Digitalização" da Máquina (PUF)

Cada máquina física, por mais idêntica que pareça ser a outra, tem pequenas imperfeições microscópicas criadas durante a fabricação (como a textura única da pele de uma pessoa).

• A Analogia: Imagine que cada máquina tem uma impressão digital única feita de hardware. Os cientistas chamam isso de PUF (Função de Imprevisibilidade Física).
• Como funciona: Quando o software pergunta "Quem é você?", a máquina responde com um código único baseado nessas imperfeições. Se você tentar rodar o software em outra máquina (mesmo que seja uma cópia perfeita), a resposta será diferente.

2. O Truque do Semáforo (O Problema da Segurança)

O maior desafio não é apenas impedir que o software rode em outro lugar, mas garantir que, se ele rodar no lugar errado, não cause acidentes.

• O Cenário: Pense em um semáforo de trânsito. Se um hacker copiar o software do semáforo e rodar em um computador falso, o semáforo não pode simplesmente apagar todas as luzes ou ficar verde para todos os carros ao mesmo tempo (isso causaria um acidente).
• A Solução: O software precisa saber: "Se eu não estiver na máquina certa, não posso fazer o movimento 'Verde para todos'. Em vez disso, devo fazer algo aleatório, mas seguro, como piscar os amarelos ou manter o vermelho."

3. O "Detetive de Futuros" (Execução Simbólica)

Como o software sabe quais movimentos são seguros e quais são perigosos antes mesmo de acontecerem? É aqui que entra a Execução Simbólica.

• A Analogia: Imagine que você é um detetive que não olha para o presente, mas sim para todos os futuros possíveis ao mesmo tempo.
• O Processo: Antes de liberar o software, os autores usam um "super-robô" (o executor simbólico) que simula o software rodando em todas as situações possíveis. Ele pergunta: "Se eu mudar esta luz para verde, um carro vai bater?"
  • Se a resposta for SIM, o robô marca esse movimento como "Proibido".
  • Se a resposta for NÃO, ele marca como "Seguro".
• O Resultado: O software é programado para, se estiver na máquina errada, escolher aleatoriamente apenas entre os movimentos que o robô marcou como "Seguros". Assim, o software nunca quebra, nunca causa acidentes, mas também nunca faz o trabalho correto (o que impede o hacker de saber como o sistema deveria funcionar de verdade).

4. Por que é difícil de hackear?

Para um hacker roubar esse software, ele teria que:

1. Descobrir a "impressão digital" da máquina original (o que é impossível de copiar).
2. Ou, tentar adivinhar qual é o movimento correto a cada momento, analisando milhões de linhas de código.
3. Como o software age de forma aleatória (mas segura) em máquinas erradas, o hacker não consegue ver um padrão claro para recriar a lógica original. Seria como tentar adivinhar a senha de um cofre olhando para um cofre que abre aleatoriamente, mas sempre de um jeito que não explode a sala.

Resumo Final

Os autores criaram um "cadeado inteligente" para software industrial:

• Na máquina certa: O software usa a impressão digital única da máquina para funcionar perfeitamente.
• Na máquina errada: O software entra em um "modo de pânico seguro". Ele não trava, não explode e não causa acidentes, mas age de forma aleatória e inútil.
• A Garantia: Eles usaram matemática avançada (execução simbólica) para provar, antes mesmo de instalar o software, que ele nunca fará algo perigoso, mesmo quando for copiado ilegalmente.

Isso torna o roubo de propriedade intelectual tão difícil e caro que, para a maioria dos criminosos, simplesmente não vale a pena tentar.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "An Approach for Safe and Secure Software Protection Supported by Symbolic Execution", apresentado em português:

Título: Uma Abordagem para Proteção de Software Segura e Segura com Suporte de Execução Simbólica

1. O Problema

O artigo aborda o grave problema do roubo de Propriedade Intelectual (PI) na indústria, especificamente através da engenharia reversa de software de controle industrial.

• Contexto: Estima-se que as perdas anuais apenas na Alemanha sejam de 6,4 bilhões de euros devido à pirataria de produtos.
• Desafio: Diferente do hardware, que é difícil de replicar, o software pode ser copiado literalmente sem necessidade de engenharia reversa complexa. O principal esforço para roubar a PI reside em replicar o hardware.
• Objetivo: Criar um método que vincule um programa a um hardware específico (máquina alvo), de modo que o programa execute corretamente apenas nela. Se executado em outra máquina (mesmo que seja uma réplica), o comportamento deve ser diferente, mas seguro (não deve causar danos físicos ou violar restrições de segurança críticas), tornando a engenharia reversa da proteção economicamente inviável.

2. Metodologia

A proposta combina três pilares principais: Funções Não Clonáveis Fisicamente (PUFs), Máquinas de Estados Abstratos (ASMs) e Execução Simbólica.

• Vinculação Hardware-Software via PUFs:

  • Utiliza-se PUFs, que são primitivas de segurança baseadas em hardware. Pequenas variações no processo de fabricação criam características físicas únicas, gerando uma "impressão digital" digital.
  • O software consulta a PUF durante a execução (runtime) para obter uma resposta a um desafio (challenge-response).
  • A lógica do programa depende dessa resposta para determinar o próximo estado de controle. Se a resposta não corresponder à esperada (ou seja, se o software estiver em outro hardware), o fluxo do programa é alterado.

• Modelagem com Control State ASMs:

  • Os programas de controle industrial são modelados como Máquinas de Estados Abstratos (ASMs) de estado de controle.
  • As regras de transição são da forma: se (condição) então (atualizações).
  • O método transforma a especificação original do ASM em uma especificação protegida.

• Garantia de Segurança via Execução Simbólica:

  • Este é o diferencial da abordagem. Ao invés de simplesmente fazer o programa falhar ou travar se a PUF retornar um valor incorreto (o que seria inseguro para aplicações industriais), o sistema utiliza execução simbólica para garantir que, mesmo com uma resposta incorreta da PUF, o programa transite apenas para estados seguros.
  • O algoritmo calcula, simbolicamente, o conjunto de "estados seguros" (safePhases). Se a resposta da PUF levar a um estado inseguro, o programa escolhe não deterministicamente um estado seguro alternativo.

O Processo de Proteção (7 Passos Mecânicos):

1. Mapeamento: Estabelece uma injeção entre as transições de estado do programa e as respostas da PUF.
2. Substituição de Regras: Substitui a atualização direta do estado de controle (ctlState := j) por uma regra ChooseCtlState que consulta a PUF.
3. Filtragem de Segurança: Se a resposta da PUF for válida (correspondente ao hardware alvo), o estado correto é assumido. Se for inválida, o sistema escolhe aleatoriamente um estado dentro do conjunto pré-calculado de estados seguros.
4. Análise Simbólica: Executa simbolicamente o programa protegido para determinar quais transições de estado violariam as restrições de segurança (ex: dois semáforos verdes ao mesmo tempo).
5. Definição de Estados Seguros: O conjunto de estados seguros é definido como todos os estados que não violam as propriedades de segurança sob qualquer condição de caminho simbólico.

3. Principais Contribuições

• Abordagem "Safe-by-Design": Diferente de métodos anteriores (como o de Xiong et al.) que podem levar a comportamentos inseguros ou travamentos se a verificação falhar, esta abordagem garante que qualquer desvio do comportamento esperado (devido a hardware errado ou falha na PUF) resulte em um comportamento seguro, embora incorreto.
• Uso de Execução Simbólica para Proteção: É a primeira aplicação conhecida de execução simbólica para suportar proteção de cópia baseada em vinculação hardware-software, garantindo a preservação de propriedades de segurança.
• Dificuldade de Engenharia Reversa: A proteção torna a engenharia reversa extremamente difícil e cara. Um atacante que obtenha o binário não consegue prever o fluxo correto sem o hardware físico específico (PUF), e tentar recriar a lógica a partir do código descompilado é complexo e demorado devido à não-determinística introduzida nos estados incorretos.

4. Resultados e Avaliação de Segurança

• Segurança Estática: A análise estática do binário ou código descompilado não revela os valores corretos de resposta da PUF, pois eles dependem do hardware físico único. Recriar a lógica do programa manualmente a partir do código protegido é mais demorado do que reescrevê-lo do zero.
• Segurança Dinâmica:
  • Tentar executar o programa em hardware idêntico não ajuda, pois a PUF não pode ser clonada.
  • Executar no hardware original permite traçar o fluxo, mas é lento e complexo, especialmente em sistemas com muitos caminhos de execução. Além disso, a análise dinâmica pode interferir no funcionamento da PUF (ex: em PUFs baseadas em DRAM que dependem de temporização precisa).
• Robustez: O método suporta falhas na PUF (respostas incorretas raras) sem comprometer a segurança do sistema industrial.

5. Significado e Conclusão

O artigo apresenta uma solução inovadora para a proteção de software industrial, resolvendo o dilema entre segurança (impedir cópia) e segurança funcional (garantir que o sistema não cause acidentes se for copiado).

• Impacto: Permite que fabricantes de máquinas protejam seu IP contra cópia não autorizada sem o risco de que, se a cópia ocorrer, o sistema falhe de maneira catastrófica.
• Futuro: Os autores planejam automatizar a ferramenta para casos de estudo industriais reais, focando na escalabilidade e na otimização das fórmulas lógicas geradas pela execução simbólica (possivelmente usando solvers SMT) para evitar latência excessiva no tempo de resposta do software de controle.

Em resumo, a técnica transforma a proteção de software em um problema de verificação formal, onde a segurança do sistema é matematicamente garantida mesmo na presença de ataques de engenharia reversa ou falhas de hardware.