Verification Modulo Tested Library Contracts

Resumen Técnico: Verificación Modulo Contratos de Librerías Probadas

1. El Problema

La verificación formal automatizada de programas grandes y complejos sigue siendo un desafío debido a la dificultad de sintetizar automáticamente invariantes inductivos y contratos precisos para librerías extensas. Los enfoques tradicionales requieren que tanto el código del cliente como las librerías sean verificados formalmente contra sus contratos, lo cual es a menudo inviable para librerías complejas.

Los autores proponen un nuevo paradigma: Verificación Modulo Contratos de Librerías Probadas (VMTLC).

• Objetivo: Verificar formalmente un programa cliente ($C$) que utiliza una librería compleja ($L$), asumiendo que los métodos de la librería cumplen ciertos contratos formales ($\Pi$).
• La Innovación: En lugar de verificar formalmente la implementación de la librería, se exige que la librería pase pruebas exhaustivas contra los contratos sintetizados.
• Definición del Problema: Dado un cliente $C$ y una librería $L$, sintetizar un conjunto de contratos formales $\Pi$ para los métodos de $L$ tales que:
  1. El cliente $C$ sea demostrado correcto asumiendo $\Pi$.
  2. Un generador de pruebas determinista (con recursos limitados) no pueda encontrar ningún caso de prueba que viole $\Pi$ en la implementación de $L$.

2. Metodología y Enfoque

El marco de trabajo se basa en un ciclo de aprendizaje guiado por contraejemplos (CEG) que integra tres componentes principales:

1. Sintetización Simultánea: El sistema sintetiza simultáneamente:
   • Contratos para la librería: Predicados que describen el comportamiento de los métodos de la librería.
   • Invariantes para el cliente: Invariantes de bucle y anotaciones necesarias para probar la corrección del cliente.
2. Resolución de Cláusulas Horn Constrainidas (CHC):
   • El problema se formula como la síntesis de soluciones para un sistema de CHCs derivado del cliente.
   • Se utiliza un solver de CHC generalizante. A diferencia de un solver estándar que podría "sobreajustar" (overfit) los contratos a los ejemplos positivos específicos, este solver busca expresiones lógicas más simples y generales que cubran los ejemplos.
   • Se emplean algoritmos de aprendizaje ICE (Implication Counterexample), que utilizan ejemplos positivos, negativos y de implicación para refinar las hipótesis.
3. Validación mediante Pruebas (Testing):
   • Los contratos sintetizados se someten a un generador de pruebas (implementado con fuzzing usando AFL++).
   • Si el generador encuentra una violación del contrato, ese caso de prueba se convierte en un ejemplo positivo (un caso que debe ser cubierto por el contrato) y se retroalimenta al solver de CHC para refinar la síntesis.
   • El ciclo continúa hasta que se encuentra un conjunto de contratos que verifica el cliente y resiste las pruebas de la librería.

3. Contribuciones Clave

• Contratos Contextuales (Contextual Contracts):

  • Los autores introducen un nuevo tipo de contrato que es válido específicamente en el contexto de las llamadas realizadas por el cliente, en lugar de ser válido para cualquier estado posible (contratos modulares).
  • Ventaja: Los contratos contextuales suelen ser más simples y fáciles de inferir porque asumen precondiciones implícitas generadas por el flujo del cliente. Por ejemplo, si un cliente solo inserta números positivos en un conjunto, el contrato de "eliminar" puede asumir que el resultado es positivo, algo que no sería cierto en un contrato modular general.
  • Esto permite verificar programas donde los contratos modulares serían demasiado complejos o imposibles de sintetizar automáticamente.

• Uso de Modelos de Lenguaje (LLMs) en ICE:

  • El marco permite utilizar LLMs (como Gemini) como aprendices ICE. El LLM propone candidatos de contratos e invariantes basados en el código y la documentación.
  • Si las propuestas fallan en la verificación o en las pruebas, los contraejemplos se devuelven al LLM para refinar la propuesta, creando un ciclo de aprendizaje híbrido (simbólico + neuronal).

• Herramienta Dualis:

  • Implementación del marco en una herramienta llamada Dualis, que orquesta la interacción entre solvers de restricciones (Z3), generadores de pruebas (AFL++) y diversos aprendices (HornICE, LLMs, o combinaciones).

4. Resultados de la Evaluación

Los autores evaluaron Dualis en un conjunto de 43 benchmarks extraídos de librerías de código abierto populares (Folly, Abseil, Android) y categorías de SV-COMP.

• Eficacia:

  • Los benchmarks seleccionados son demasiado complejos para las herramientas de verificación automática de última generación (como SeaHorn), las cuales fallaron en la mayoría de los casos.
  • Contratos Modulares: El enfoque basado en LLM puro resolvió 38 de 43 benchmarks. HornICE resolvió 19, y la combinación HornICE+LLM resolvió 25.
  • Contratos Contextuales: El rendimiento fue superior. El enfoque LLM resolvió 41 de 43 benchmarks, y HornICE+LLM resolvió 28.
  • Conclusión: Los contratos contextuales son significativamente más fáciles de sintetizar y permiten verificar más casos que los modulares.

• Validación de Contratos Sintetizados:

  • Se realizó una verificación manual y automática de los contratos generados. Todos los contratos sintetizados (tanto modulares como contextuales) resultaron ser lógicamente correctos.
  • Se probó la robustez contra mutantes incorrectos (programas con errores sutiles). El marco VMTLC con contratos modulares rechazó correctamente todos los mutantes. Con contratos contextuales, se detectaron 11/30 mutantes como incorrectos (el resto pasó debido a rutas de ejecución raras difíciles de alcanzar por el fuzzer), lo que indica que, aunque los contratos contextuales son más propensos a ser "espurios" (falsos positivos) que los modulares, aún añaden valor significativo sobre la simple prueba.

• Importancia de la Generalización:

  • Reemplazar el solver de CHC generalizante por un solver estándar (CVC5) redujo drásticamente el éxito (solo 10 contratos modulares y 15 contextuales), demostrando que la capacidad de generalizar ejemplos es crucial para el éxito del método.

5. Significado y Conclusión

El trabajo presenta un avance significativo hacia la automatización de la verificación de software a gran escala.

• Compromiso Pragmático: Propone un punto intermedio en el espacio de diseño de verificación: sacrificar la garantía de verificación formal completa de las librerías a cambio de obtener escalabilidad y automatización completa para el sistema cliente-librería.
• Viabilidad: Demuestra que es posible verificar formalmente clientes complejos si se asume que la librería cumple contratos que han sido rigurosamente probados, en lugar de formalmente verificados.
• Futuro: Abre la puerta a la verificación de programas que actualmente están fuera del alcance de las herramientas automáticas, utilizando una combinación de síntesis de invariantes, aprendizaje de máquinas (incluyendo LLMs) y pruebas intensivas.

En resumen, VMTLC ofrece una estrategia práctica para escalar la verificación formal, utilizando la prueba como un sustituto viable de la verificación formal para componentes de librería complejos, siempre que se utilicen contratos sintetizados adecuadamente (especialmente los contextuales) y se empleen solvers de CHC capaces de generalizar.