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

Resumen Técnico: ESBMC-ARDUINO

Problema: La brecha de despliegue en los PLC de hardware abierto
Los Controladores Lógicos Programables (PLC) de hardware abierto, como OpenPLC ejecutándose en Arduino OPTA, CONTROLLINO e Industrial Shields M-Duino, han democratizado la programación IEC 61131-3 para dispositivos de clase microcontrolador de bajo costo. Estas plataformas se utilizan cada vez más en educación, automatización a pequeña escala y como sustrato de tiempo de ejecución para la investigación de seguridad en Sistemas de Control Industrial (ICS). Sin embargo, existe una "brecha de despliegue" crítica entre los modelos abstractos utilizados por los verificadores de código abierto existentes (por ejemplo, ESBMC-PLC, PLCverif) y el entorno de ejecución de hardware real.

Los verificadores actuales operan sobre un modelo de ciclo de escaneo abstracto que asume enteros idealizados e ilimitados y entradas sin restricciones. En contraste, los artefactos desplegados se ejecutan en Unidades de Microcontrolador (MCU) con recursos limitados que poseen anchos de palabra de máquina específicos (por ejemplo, un int de 16 bits en placas AVR de 8 bits) y convertidores analógico-digitales (ADC) de resolución finita (típicamente de 10 bits, lo que produce valores en $[0, 1023]$). Esta discrepancia conduce a dos modos de falla:

1. Defectos omitidos: Un programa puede ser probado como seguro en el modelo abstracto pero inseguro en el dispositivo debido a un desbordamiento de enteros causado por anchos de palabra estrechos (por ejemplo, un cálculo de escalado que se envuelve en una placa de 16 bits).
2. Alarmas fantasma (Falsos positivos): Más críticamente, una verificación consciente del ancho que tiene en cuenta el ancho de palabra pero ignora los límites de entrada de hardware explora valores de sensores que ningún ADC físico puede producir (por ejemplo, valores negativos o valores que exceden 1023). Esto resulta en reportes de desbordamiento espurios. La evaluación en un corpus de 123 programas de terceros demostró que la comprobación de desbordamiento de 16 bits ingenua genera una tasa de falsas alarmas del 44% (54/123), mientras que encuentra cero defectos genuinos.

Metodología: Verificación fiel al hardware
El artículo propone un método para cerrar esta brecha mediante la construcción de un "modelo de despliegue" ($M_{dev}$) que represente fielmente el hardware objetivo. El núcleo de este enfoque es un descriptor de Capa de Abstracción de Hardware (HAL) y un proceso de reducción (lowering) consistente.

1. Descriptor HAL ($H$): Una tupla declarativa $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ que captura:
   • $w$: El ancho de la palabra de máquina (por ejemplo, 16 bits para AVR, 32 bits para ARM).
   • $b_{adc}$ y $b_{pwm}$: La resolución de los Convertidores Analógico-Digitales y las salidas de Modulación por Ancho de Pulso (PWM).
   • $\mu$: Un mapa de vinculación de E/S derivado automáticamente del esquema de direccionamiento directo de IEC 61131-3 (por ejemplo, las direcciones %IW se mapean a entradas analógicas con rangos de ADC específicos).
2. Reducción Fiel (Faithful Lowering): El método transforma el programa PLC ($P$) en un modelo de despliegue ($M_{dev}(P, H)$) mediante:
   • La interpretación de la aritmética en el ancho de palabra objetivo $w$ (reproduciendo exactamente el desbordamiento por complemento a dos).
   • La inyección de restricciones assume inmediatamente después del muestreo de entrada para restringir las variables a sus rangos realizables por el hardware (por ejemplo, $0 \leq adc \leq 1023$).
   • La sobre-aproximación de bloques funcionales no lineales (por ejemplo, PID) con salidas no deterministas para mantener la tractabilidad.
3. Motor de Verificación: El método reutiliza el backend de ESBMC (Model Checking basado en SMT y $k$-inducción) sin modificaciones. La reducción ocurre en el frontend de Diagrama de Escalera (LD), añadiendo un gancho ligero (aproximadamente 4 de 40 líneas) que impone los límites de entrada y establece el ancho de palabra de la arquitectura.

Contribuciones Clave

1. Método de Verificación Fiel al Hardware: Un enfoque formal que transfiere la disciplina de modelo-objetivo de la programación C para sistemas embebidos de seguridad crítica (establecida por herramientas como Frama-C y Astrée) al dominio de los PLC. A diferencia de esas herramientas, este método deriva automáticamente los límites de entrada a partir del esquema de direccionamiento estándar de IEC 61131-3 y los descriptores de la placa.
2. Instanciación ESBMC-Arduino: Una implementación concreta para objetivos de clase Arduino, que obtiene los parámetros HAL de los núcleos oficiales de Arduino. Soporta tanto objetivos de 16 bits (AVR) como de 32 bits (ARM).
3. Evaluación Empírica: Una evaluación rigurosa en 123 programas reales y un corpus controlado de 20 patrones.

Resultados

• Eliminación de Falsas Alarmas: En el corpus de 123 programas, habilitar el anotador HAL eliminó todas las 54 falsas alarmas (reduciendo el conteo de inseguros de 54 a 0) mientras preservaba cada prueba de robustez (32 programas permanecieron probados como seguros).
• Detección de Defectos Genuinos: Un corpus controlado demostró que el método detecta defectos genuinos dependientes del ancho (por ejemplo, desbordamiento en el escalado de ADC a porcentaje en placas de 16 bits) con testigos físicamente realizables.
• Validación Cruzada entre Herramientas: El fenómeno de las "alarmas fantasma" fue reproducido utilizando herramientas independientes (CBMC y Frama-C/EVA) sobre espejos en C de la lógica, confirmando que el problema es inherente a la verificación ingenua consciente del ancho sin modelado de entrada, y no específico de ESBMC.
• Rendimiento: La sobrecarga del anotador HAL es insignificante; los tiempos de verificación permanecen por debajo de un segundo por programa.
• Limitaciones: Aunque las falsas alarmas se eliminan, 91 programas en el corpus real devolvieron veredictos "desconocidos" debido a la incompleitud de la $k$-inducción en bloques de funciones con estado interno. Esta es una limitación de la capacidad del probador para cerrar pasos inductivos, no del modelo de entrada.

Significancia
El artículo argumenta que el valor principal de este trabajo no es el recuento de errores descubiertos (que son raros en los corpus públicos específicos analizados, dominados por lógica booleana y de temporizadores), sino la restauración de la solidez (soundness). Los autores demuestran que la verificación consciente del ancho de forma ingenua es inutilizable para el aseguramiento debido a una tasa de falsas alarmas del 44% que ahoga los hallazgos genuinos. Al derivar automáticamente los rangos de entrada realizables por el hardware, el método convierte una herramienta poco fiable en una que emite únicamente reportes realizables, permitiendo a los ingenieros confiar en los resultados de verificación para los PLC de hardware abierto. El enfoque se presenta como una estrategia de adopción realista y de bajo costo (un descriptor de 4 campos y un gancho de 40 líneas) que se integra con la infraestructura de verificación madura en lugar de proponer un nuevo diseño desde cero.