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

Este artículo presenta un nuevo método de protección de software para sistemas de control industrial que utiliza funciones físicamente no clonables (PUF) para vincular el programa al hardware y la ejecución simbólica para garantizar la seguridad y la preservación de las propiedades de seguridad ante intentos de ingeniería inversa o ejecución en máquinas no autorizadas.

Lo esencial

🛡️ El "Candado Físico" que hace que el software sea único

Imagina que tienes una receta secreta para hacer el pastel más delicioso del mundo (el software). El problema es que cualquiera puede copiar esa receta, imprimirla y venderla. En el mundo industrial, esto es un desastre: si alguien roba el software que controla una máquina de fabricación, puede copiar la máquina entera y venderla sin pagar al dueño original.

Los autores de este artículo proponen una solución genial: hacer que el software solo funcione correctamente en la máquina específica para la que fue diseñado, pero de una forma muy especial.

1. La Huella Digital de la Máquina (PUF)

Cada máquina tiene una "huella digital" física única, llamada PUF (Función Físicamente Inclonable).

• La analogía: Imagina que cada máquina tiene una cerradura hecha de madera viva. Debido a cómo creció el árbol, la textura de la madera es única. No hay dos cerraduras iguales en el mundo, ni siquiera si intentas copiarlas.
• Cómo funciona: El software le hace una pregunta a la máquina (un "desafío"). La máquina responde basándose en su textura única (la "respuesta"). Si el software está en la máquina correcta, la respuesta es perfecta y el pastel se hace. Si el software está en una copia (una máquina diferente), la textura es distinta, la respuesta es diferente y... ¡el pastel sale mal!

2. El Problema: ¿Qué pasa si el pastel sale mal?

Aquí está la parte más importante del artículo. En los métodos antiguos de protección, si el software detectaba que estaba en la máquina equivocada, simplemente se rompía, se cerraba o hacía algo peligroso (como detener una máquina industrial en medio de una operación, lo cual podría causar accidentes).

La innovación de este paper: Ellos quieren que, si el software está en la máquina equivocada, no se rompa, pero tampoco funcione bien. Debe comportarse de forma extraña y aleatoria, pero siempre de forma segura.

• La analogía: Imagina que robas el coche de un amigo. Al encenderlo, el motor arranca, pero el volante gira hacia la izquierda cuando intentas ir a la derecha, y el radio solo toca música de gatos. El coche no explota, no se estrella, pero es imposible de conducir correctamente. El ladrón se frustra porque no puede usarlo, pero nadie sale herido.

3. El "Detective Mágico" (Ejecución Simbólica)

¿Cómo saben los autores que el software se comportará "mal pero seguro" en la máquina equivocada? Usan una técnica llamada Ejecución Simbólica.

• La analogía: Imagina que eres un director de cine que quiere ensayar todas las posibles versiones de una película antes de rodarla. En lugar de usar actores reales, usas "actores fantasma" que pueden ser cualquier cosa.
  • El director le pregunta al actor fantasma: "¿Qué pasa si el semáforo está en rojo?". El actor fantasma responde: "Puede ser rojo, o verde, o amarillo".
  • El director simula todas las posibilidades a la vez.
  • Con esta técnica, los autores verifican matemáticamente que, sin importar qué respuesta "rara" le dé la máquina equivocada al software, el resultado final nunca será un accidente (por ejemplo, nunca dejarán que dos semáforos se pongan en verde al mismo tiempo).

4. ¿Por qué es difícil de hackear?

El objetivo es hacer que robar el software sea tan difícil y caro que no valga la pena.

• Si el hacker intenta copiar el código: El código necesita la "huella digital" de la máquina original para funcionar bien. Sin ella, el software hace cosas aleatorias.
• Si el hacker intenta copiar la máquina: No puede copiar la huella digital física (la textura de la madera) porque es única e inimitable.
• Si el hacker intenta adivinar la respuesta: Tendría que probar millones de combinaciones. Como el software cambia de forma aleatoria pero segura en la máquina equivocada, el hacker no puede deducir fácilmente cuál es la respuesta correcta. Es como intentar adivinar la combinación de un candado que cambia cada vez que fallas, pero que nunca se rompe.

En resumen

Este paper presenta un sistema de seguridad para máquinas industriales que une el software con el hardware de forma inseparable:

1. Seguridad: El software solo funciona bien en su máquina original gracias a una huella digital única (PUF).
2. Seguridad Física: Si alguien intenta usarlo en otra máquina, el software no se rompe ni causa accidentes; simplemente actúa de forma extraña y aleatoria, pero segura.
3. Dificultad para el ladrón: Para robarlo, el hacker tendría que descifrar un rompecabezas matemático enorme, lo cual toma tanto tiempo y dinero que es mejor dejarlo en paz.

Es como ponerle un candado a tu casa que, si alguien intenta forzarlo, no se rompe, sino que la casa empieza a cantar ópera y a pintar las paredes de colores neón: el ladrón se va frustrado, pero tu casa sigue intacta y segura.

Resumen técnico

Resumen Técnico: Protección de Software Segura y con Garantía de Seguridad mediante Ejecución Simbólica

1. El Problema

La ingeniería inversa a escala industrial representa una amenaza crítica para la propiedad intelectual (PI), con pérdidas anuales estimadas en miles de millones de euros. En el contexto de la industria de máquinas y control industrial, el robo de PI a menudo implica replicar el hardware y copiar el software verbatim (copia literal) sin necesidad de ingeniería inversa compleja.

El desafío principal es desarrollar un mecanismo de protección que:

• Vincule el software al hardware: El programa solo debe ejecutarse correctamente en la máquina objetivo específica.
• Garantice la seguridad (Safety): Si el software se ejecuta en una máquina no autorizada (incluso una réplica del hardware) o si falla la respuesta del mecanismo de seguridad, el programa no debe fallar ni causar daños. Debe comportarse de manera diferente (incorrecta pero segura) para dificultar la ingeniería inversa, pero sin violar las restricciones de seguridad críticas (ej. evitar que dos semáforos se pongan en verde simultáneamente).
• Resista la ingeniería inversa: Hacer que el esfuerzo para romper la protección sea económicamente inviable para el atacante.

2. Metodología

Los autores proponen un método novedoso que combina tres pilares tecnológicos:

A. Funciones de Función Física Inimitable (PUF)
Se utiliza una PUF (basada en características físicas únicas del hardware, como variaciones en la memoria DRAM o componentes dedicados) para generar respuestas digitales únicas ante desafíos específicos. Esto crea una "huella digital" del hardware que no puede ser clonada.

B. Máquinas de Estados Abstractos (ASMs) de Estado de Control
El software objetivo se modela como Máquinas de Estados Abstractos (ASMs), específicamente en su forma de "estado de control". Esto permite representar programas de control industrial como un conjunto finito de reglas de transición entre estados, facilitando su análisis formal.

C. Ejecución Simbólica para Garantizar la Seguridad
Esta es la contribución central. En lugar de simplemente redirigir el flujo de control a una función aleatoria si la PUF falla (lo cual podría causar un comportamiento inseguro o un crash), el método utiliza ejecución simbólica para precalcular matemáticamente qué transiciones de estado son "seguras".

El Proceso de Protección (Paso a Paso):

1. Vinculación: Se asocian las transiciones de estado del programa original con respuestas específicas de la PUF.
2. Análisis Simbólico: Antes de la implementación, se ejecuta simbólicamente el programa. Se asignan valores simbólicos a las variables de estado y se analizan todas las posibles rutas de ejecución.
3. Determinación de Estados Seguros: Se identifica el conjunto de estados siguientes (safePhases o safeCtlStates) que, aunque no sean el estado correcto esperado por la lógica original, no violan las propiedades de seguridad (invariantes) del sistema.
4. Transformación del Código:
   • Si el programa se ejecuta en el hardware correcto, la PUF devuelve la respuesta esperada y el programa avanza al estado correcto.
   • Si se ejecuta en hardware incorrecto o la PUF falla, el programa entra en un modo de "degradación segura": elige no determinísticamente un estado del conjunto precalculado de estados seguros.
5. Resultado: El software en una máquina no autorizada funciona, pero produce resultados incorrectos (no útiles para el atacante) y, crucialmente, nunca entra en un estado peligroso.

3. Contribuciones Clave

• Enfoque "Safe-by-Design" (Seguro por Diseño): A diferencia de métodos anteriores que podían causar fallos o comportamientos inseguros al fallar la verificación de hardware, este método garantiza formalmente que las propiedades de seguridad se mantengan incluso en caso de fallo o ejecución no autorizada.
• Uso de Ejecución Simbólica en Protección de Copias: Es la primera vez, según los autores, que la ejecución simbólica se utiliza específicamente para habilitar la protección de copias basada en vinculación hardware-software, asegurando la preservación de invariantes de seguridad.
• Generalización Formal: Se presenta un algoritmo mecánico de 7 pasos que puede transformar cualquier especificación ASM de estado de control en una versión protegida, vinculada a una PUF específica.
• Resistencia a la Ingeniería Inversa: Al hacer que el comportamiento en hardware no autorizado sea no determinista pero seguro, se elimina la posibilidad de que el atacante deduzca la lógica correcta simplemente observando el comportamiento en una máquina clonada.

4. Resultados y Evaluación

• Evaluación de Seguridad (Modelo de Amenaza):
  • Análisis Estático: Un atacante con acceso al binario no puede determinar las respuestas correctas de la PUF. Revertir la lógica del control de estado es extremadamente complejo y costoso, a menudo más que reescribir el software desde cero.
  • Análisis Dinámico: Incluso si el atacante tiene acceso al hardware original, la naturaleza no determinista de las respuestas de la PUF en máquinas no autorizadas y la interferencia potencial con los tiempos de respuesta (especialmente en PUFs basadas en DRAM) dificultan la extracción de la lógica correcta.
• Evaluación de Seguridad (Safety): El método demuestra formalmente (mediante el ejemplo de un semáforo de tráfico) que las transiciones hacia estados inseguros (ej. dos luces verdes) son excluidas del conjunto de transiciones permitidas cuando la PUF no valida el hardware.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

• Cambio de Paradigma: Mueve la protección de software de un enfoque puramente defensivo (ocultar o encriptar) a uno de resiliencia garantizada. Acepta que el software puede ser copiado, pero asegura que la copia no sea funcional ni peligrosa.
• Aplicabilidad Industrial: Al centrarse en ASMs de estado de control, el método es directamente aplicable a la vasta mayoría de los programas de control industrial (PLC, sistemas embebidos), que son los objetivos principales del robo de propiedad intelectual en la industria.
• Viabilidad Económica: Al hacer que la ingeniería inversa sea un proceso largo, costoso y sin garantías de éxito (debido a la aleatoriedad segura), desincentiva económicamente a los atacantes.
• Futuro: Los autores planean automatizar la identificación de estados de control y la traducción de restricciones de seguridad para escalar el método a estudios de caso industriales reales, utilizando solucionadores SMT para manejar la complejidad de las fórmulas lógicas generadas.

En conclusión, el paper propone una solución robusta que une la seguridad física (PUF) con la verificación formal (Ejecución Simbólica) para crear software que es intrínsecamente seguro incluso cuando es robado o ejecutado en entornos no autorizados.