💻 computer science

SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

SEAL es un analizador estático de prototipo modular para verificar programas con estructuras de datos vinculadas no acotadas que aprovecha la lógica de separación y el solver basado en SMT, Astral, para lograr resultados competitivos en la categoría de LinkedLists mientras ofrece una extensibilidad significativa para el desarrollo futuro.

Autores originales: Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Publicado 2026-02-09

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás tratando de verificar que una ciudad compleja y siempre cambiante de carreteras y edificios sea segura para navegar. Debes asegurarte de que nadie se caiga de un puente (un "desreferencia de puntero nulo" o NULL-pointer dereference), que nadie intente demoler un edificio que ya no existe (un error de "uso después de la liberación" o use-after-free) y que nadie derribe accidentalmente un edificio dos veces (un error de "doble liberación" o double-free).

Esto es exactamente lo que hace SEAL, pero en lugar de una ciudad, analiza programas informáticos que gestionan listas de datos complejas y cambiantes (como las listas enlazadas).

Aquí explicamos cómo funciona SEAL, desglosado en conceptos sencillos:

1. La idea central: Un detective especializado

La mayoría de las herramientas que comprueban estos programas son como detectives que utilizan un libro de reglas específico y rígido para cada tipo de crimen. SEAL es diferente. Utiliza un "motor de lógica" de propósito general llamado ASTRAL.

Piensa en ASTRAL como un superinteligente traductor. Cuando SEAL ve un rompecabezas complejo sobre cómo se conectan los datos en la memoria, traduce ese rompecabezas a un lenguaje que un resolvedor estándar y potente (llamado resolvedor SMT) entiende perfectamente. Esto hace que SEAL sea muy flexible. Es como tener un detective que puede cambiar de idioma para hablar con cualquier experto, en lugar de estar atrapado hablando solo un dialecto.

2. El desafío: Finito vs. Infinito

Los programas que verifica SEAL suelen implicar listas enlazadas: cadenas de datos donde un elemento apunta al siguiente.

El Problema: Algunas listas son cortas y fijas (como una cadena de 3 eslabones). Otras son no acotadas (unbounded), lo que significa que podrían tener 10 eslabones, o 10,000, o ser infinitas.
La Dificultad: Intentar comprobar cada longitud posible de una cadena infinaria es imposible para una computadora. Tomaría una eternidad.
El Truco de SEAL: SEAL utiliza una técnica de abstracción. Imagina que estás mirando un tren muy largo. En lugar de contar cada vagón, SEAL dice: "Está bien, esto es un 'tren largo'". Reemplaza los detalles desordenados del medio de la cadena con una única etiqueta limpia (un "predicado"). Esto le permite razonar sobre toda la cadena sin perderse en los detalles.

3. Cómo funciona: El analizador de "forma"

SEAL es un "analizador de forma" (shape analyzer). No solo mira números; mira la forma de la memoria.

Montículos simbólicos (Symbolic Heaps): Crea un mapa de la memoria utilizando "montículos simbólicos". Piensa en esto como un plano que dice: "Aquí hay un bloque de memoria, y este se conecta con este otro bloque".
Punto fijo del bucle (Loop Fixpoint): Cuando un programa se ejecuta en un bucle (repitiendo la misma acción), SEAL comprueba si la "forma" de la memoria se ha estabilizado. Si la forma en la ronda actual parece "suficientemente segura" en comparación con la ronda anterior, deja de comprobar el bucle y lo declara seguro.

4. Fortalezas y debilidades actuales

El artículo admite que SEAL es todavía un prototipo (una versión temprana), pero tiene unas estadísticas impresionantes:

Las Buenas Noticias (Fortalezas):

El Club de los "No Acotados": En una competencia reciente, hubo 20 herramientas intentando verificar programas con listas infinitas. Solo cuatro herramientas tuvieron éxito. SEAL fue una de ellas.
Potencial Futuro: Debido a que SEAL utiliza ese "traductor" flexible (ASTRAL), es más fácil enseñarle nuevas formas. Los autores creen que eventualmente podrán enseñarle a manejar estructuras complejas como árboles o listas de salto (skip-lists, que son como autopistas de varios niveles para los datos) en las que otras herramientas tienen dificultades.

Las Malas Noticias (Debilidades):

Vocabulario Limitado: Actualmente, SEAL solo entiende un subconjunto pequeño del lenguaje C. Todavía no puede manejar matemáticas complejas con números o muchos tipos de punteros.
Juego de Adivinanza: A veces, SEAL tiene que adivinar qué tipo de estructura de datos está construyendo un código. Si adivina mal (por ejemplo, pensando que una estructura compleja es solo una lista simple), podría pasar por alto un error o dar una respuesta de "no lo sé".
Falsos Positivos: Debido a que utiliza abstracciones (simplificando los detalles), a veces puede pensar que un programa no es seguro cuando en realidad sí lo es. El artículo señala que podrían solucionar esto volviendo a ejecutar la comprobación sin simplificaciones, pero eso toma más tiempo.

5. La conclusión

SEAL es una nueva herramienta modular diseñada para demostrar que los programas que gestionan cadenas de datos complejas e infinitas son seguros. Aunque aún no es perfecto y no entiende todas las características del lenguaje C, su diseño único —utilizar un traductor general para resolver acertijos lógicos— lo convierte en una de las pocas herramientas capaces de manejar los tipos más difíciles de problemas de seguridad de memoria. Los autores esperan que, al mantener el sistema flexible, puedan hacerlo aún mejor en futuras competencias.

Resumen Técnico: SEAL – Ejecución Simbólica con Lógica de Separación

Planteamiento del Problema

La verificación de programas que manipulan estructuras de datos vinculadas no acotadas sigue siendo un desafío significativo en el análisis estático. Si bien muchas herramientas dependen del modelado de verificación acotada o de heurísticas especializadas, estos enfoques suelen tener dificultades con la complejidad de razonar sobre longitudes de listas arbitrarias y formas de memoria complejas. Además, los analizadores existentes basados en la lógica de separación (SL) suelen acoplar el análisis con resolvedores dedicados y no modulares, lo que limita su extensibilidad y su capacidad para integrarse con otras teorías lógicas.

Metodología

SEAL es un analizador estático diseñado para la verificación de programas que manipulan estructuras de datos vinculadas no acotadas. Emplea una interpretación abstracta hacia adelante sobre fórmulas de lógica de separación (SL). La metodología central se distingue por una arquitectura modular que desacopla claramente el motor de análisis del motor de razonamiento lógico.

Componentes Principales

Dominio Abstracto (Heaps Simbólicos):
- SEAL representa los estados de memoria abstractos como heaps simbólicos, que son fórmulas de SL de la forma $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ .
- Las fórmulas atómicas ( $\phi_i$ $ϕ_{i}$ ) incluyen:
  - Fórmulas puras: Describen (des)igualdades de punteros o restricciones sobre valores que no son punteros.
  - Átomos de puntos-a (points-to): Describen celdas de memoria individuales.
  - Predicados inductivos: Describen secuencias no acotadas de punteros (por ejemplo, listas).
  - Memoria libre: Un predicado especial que representa explícitamente la memoria liberada que permanece alcanzable.
- El dominio rastrea valores enteros precisos dentro de un rango configurable (por defecto $[-5, 5]$ ). Los estados en las ubicaciones del programa se representan como disjunciones (conjuntos) de heaps simbólicos.
Abstracción y Ensanchamiento (Widening):
- Para manejar bucles y espacios de estados infinitos, SEAL realiza un ensanchamiento generalizando las formas de la memoria. Esto implica encontrar predicados espaciales compatibles (puntos-a o predicados de lista) y unirlos en un único predicado de lista, siempre que la ubicación de vinculación no sea objetivo de punteros externos o variables del programa.
- El sistema rastrea longitudes mínimas de lista hasta un límite fijo para garantizar las garantías de aciclicidad durante la abstracción.
- Adivinación de Predicados (Predicate Guessing): Actualmente, SEAL adivina el predicado inductivo esperado para las estructuras de C antes del análisis basándose en el recuento de campos (por ejemplo, un campo autorreferencial $\to$ SLL; dos $\to$ DLL). Esta heurística puede llevar a una clasificación errónea (por ejemplo, una estructura destinada a ser una lista anidada clasificada como una lista doblemente enlazada).
El Resolvedor ASTRAL:
- A diferencia de la mayoría de las herramientas de SL que utilizan heurísticas dedicadas para la satisfacibilidad y la implicación, SEAL depende de ASTRAL, un resolvedor de lógica de separación de propósito general.
- ASTRAL traduce las fórmulas de SL en teorías SMT (específicamente vectores de bits y arreglos) utilizando un límite en el despliegue de predicados.
- Las fórmulas traducidas se pasan al resolvedor SMT BITWUZLA.
- ASTRAL soporta predicados inductivos definidos por el usuario, lo que permite a SEAL definir sus propios predicados sin necesidad de soporte integrado en el resolvedor para ellos.
Mecánica del Análisis:
- Puntos Fijos de Bucle (Loop Fixpoints): Se alcanza un punto fijo cuando la implicación entre el estado de la iteración actual del bucle ( $S$ ) y el estado de la iteración anterior ( $T$ ) es válida. Esto se aproxima verificando si para cada heap en $S$ , existe un heap en $T$ que lo implica.
- Análisis Interprocedural: Las llamadas a funciones se optimizan mediante resúmenes (pares de precondición/postcondición).
- Simplificación: El sistema aplica simplificaciones sintácticas, como la reducción de clases de equivalencia y la eliminación de variables fuera de alcance.

Contribuciones Clave

Arquitectura Modular: Al separar el motor de interpretación abstracta del motor de razonamiento lógico mediante ASTRAL, SEAL logra un diseño destinado a ser más fácil de extender y combinar con el razonamiento en otras teorías.
Resolución de Propósito General: La integración de ASTRAL permite a SEAL aprovechar los resolvedores SMT para la implicación y la satisfacibilidad de SL, evitando la necesidad de resolvedores personalizados y dedicados para cada variante específica de la lógica.
Verificación de Listas No Acotadas: La herramienta es capaz de verificar programas con listas vinculadas no acotadas, una categoría donde muchas herramientas competidoras fallan.

Resultados Experimentales

SEAL participó en la categoría MemSafety-LinkedLists de la competencia SV-COMP.

Rendimiento General: Sobre el conjunto completo de 134 programas, SEAL verificó 55 como "True" (correctos) y encontró 4 "False" (errores), con 75 reportando sin resultado.
Subconjunto de Listas No Acotadas: En el subconjunto de 69 programas que requieren razonar sobre estructuras de datos no acotadas, SEAL verificó 14 programas como correctos y encontró 2 errores.
Comparación:
- SEAL superó a 2LS (que solo verificó 3 programas no acotados).
- SEAL verificó menos programas que PREDATORHP (46) y CPACHECKER (40), ambos los cuales utilizan grafos de memoria simbólica (SMG).
- SEAL fue uno de los cuatro únicos analizadores capaces de verificar programas con listas no acotadas en esta categoría.

Significado y Reivindicaciones

El artículo posiciona a SEAL como un prototipo prometedor con un enfoque específico en la extensibilidad en lugar del dominio inmediato del rendimiento bruto.

Potencial Futuro: Los autores afirman que el diseño modular de la herramienta y su dependencia de ASTRAL proporcionan una base sólida para soportar estructuras de datos complejas que no pueden representarse fácilmente mediante SMG, tales como listas saltadas (skip-lists) y árboles.
Limitaciones: Como prototipo temprano, SEAL actualmente soporta solo un subconjunto de C (aritmética de punteros limitada, seguimiento de enteros específico) y depende de la adivinación heurística de predicados, lo que puede llevar a falsos positivos o a la incapacidad de reportar violaciones cuando falta información de enteros.
Hoja de Ruta: Los autores pretenden mejorar la selección de predicados durante el análisis, sintetizar predicados inductivos a partir de ejemplos y, potencialmente, embeber SEAL como un dominio abstracto dentro del marco Frama-C EVA para manejar valores de no-puntero más complejos.

En resumen, SEAL demuestra que un enfoque de resolución de lógica de separación basado en SMT y de propósito general es una alternativa viable y extensible a las heurísticas especializadas, ofreciendo una vía para verificar estructuras de datos complejas y no acotadas en futuras competencias.