AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation

Problema
La verificación formal es crítica para garantizar la seguridad de los protocolos criptográficos, pero sigue siendo una barrera significativa para los profesionales. Aunque herramientas como Tamarin y ProVerif han automatizado gran parte del proceso de verificación, persiste la brecha entre los modelos simbólicos de alto nivel y las implementaciones concretas de los protocolos. Cerrar esta brecha requiere tradicionalmente una experiencia sustancial en métodos formales para modelar manualmente las implementaciones o para interpretar los resultados de la verificación para bases de código específicas. Además, los enfoques existentes que extraen modelos de lenguajes de propósito general suelen imponer restricciones restrictivas (como prohibir bucles o recursión) para mantener la tractabilidad, dejando partes de la máquina de estados del protocolo a supuestos manuales. Esta limitación es problemática, ya que vulnerabilidades históricas (por ejemplo, SKIP) han surgido de máquinas de estados implementadas incorrectamente. Además, la transferencia de los resultados de la verificación a las implementaciones concretas carece de una conexión sólida y automatizada, lo que requiere conocimiento experto para asegurar que una propiedad probada en un modelo simbólico se cumpla realmente en el código en ejecución.

Metodología
Los autores presentan AutoTam, un novedoso enfoque de "primero el lenguaje" (language-first) que integra la implementación del protocolo, la generación de modelos simbólicos y la ejecución simbólica dinámica. El núcleo de la metodología es un lenguaje de dominio específico (DSL) diseñado específicamente para protocolos criptográficos.

1. Lenguaje AutoTam: El lenguaje está diseñado para alinearse con el nivel de abstracción de las propiedades de seguridad de alto nivel manteniendo la capacidad de ser ejecutable. Modela los protocolos como máquinas de estados finitos donde los roles consisten en estados (divididos en partes de salida y entrada) y transiciones. El lenguaje restringe el flujo de control al nivel de la máquina de estados del protocolo para asegurar la decidibilidad durante la traducción, evitando problemas de alcanzabilidad indecidibles. Soporta máquinas de estados arbitrarias, incluyendo ciclos requeridos para fases de transporte, pero limita las elecciones intra-procedimentales para que formen parte de la lógica de la máquina de estados.
2. Intérprete y Ejecución: AutoTam incluye un intérprete que ejecuta descripciones de protocolos directamente. Esto permite la interoperabilidad de pruebas con implementaciones existentes (por ejemplo, WireGuard). El intérprete utiliza una tabla de búsqueda para funciones predefinidas (E/S de red, operaciones criptográficas como ChaCha20-Poly1305, Ed25519 y Blake2s) implementadas mediante la biblioteca formalmente verificada HACL.
3. Traducción Sólida a Tamarin: Los autores desarrollaron un procedimiento de traducción que convierte las descripciones de protocolos de AutoTam en modelos de Tamarin. La traducción mapea transiciones extendidas (que combinan la entrada del estado de origen, la lógica de transición y la salida del estado de destino) en reglas de reescritura únicas de Tamarin. Los autores proporcionan una prueba formal de solidez (soundness), demostrando que cualquier propiedad de traza probada en el modelo Tamarin generado se cumple para la ejecución concreta de la implementación de AutoTam bajo el modelo Dolev-Yao. Esto asegura que los resultados de la verificación sean directamente aplicables a la implementación.
4. Integración de Ejecución Simbólica: Para abordar la seguridad de memoria y los errores a nivel de implementación, AutoTam se integra con el motor de ejecución simbólica dinámica KLEE. El intérprete se compila a bytecode de LLVM, y las funciones criptográficas se reemplazan con abstracciones simbólicas. Esto permite la exploración sistemática de rutas de ejecución bajo entradas de red arbitrarias, descartando errores de memoria como desbordamientos de búfer (buffer overflows).

Contribuciones Clave

• Lenguaje AutoTam: Un lenguaje de dominio específico totalmente ejecutable para protocolos criptográficos que codifica naturalmente máquinas de estados, análisis de mensajes y operaciones criptográficas.
• Extracción de Modelos Sólida: Un procedimiento para extraer modelos de Tamarin de implementaciones ejecutables, acompañado de una prueba formal de solidez respecto a las propiedades de traza. Esto garantiza que las propiedades de traza universales verificadas en el modelo se traduzcan de vuelta a la implementación.
• Ejecución Simbólica Integrada: Un flujo de trabajo totalmente integrado utilizando KLEE para analizar las implementaciones de AutoTam para la seguridad de memoria, proporcionando pruebas de cobertura completas contra entradas de red arbitrarias.
• Casos de Estudio: La implementación y verificación de dos protocolos:
  • Un protocolo de intercambio de claves Diffie-Hellman firmado.
  • El protocolo de VPN WireGuard.
    Los autores demuestran que su implementación de WireGuard es interoperable con las implementaciones existentes del kernel de Linux y de Go, y logra un rendimiento aceptable.

Resultados

• Eficiencia de Verificación: La herramienta generó modelos de Tamarin para ambos casos de estudio en menos de 1 segundo. El protocolo Diffie-Hellman fue verificado para todas las propiedades de seguridad (secreto, autenticación) en menos de 5 segundos.
• Verificación de WireGuard: La verificación del modelo de WireGuard requirió un "lema de fuentes" (sources lemma) añadido manualmente para guiar al probador, un requisito común para protocolos complejos en Tamarin. A pesar de esto, el modelo generado fue verificado con éxito para propiedades de intercambio de manos (handshake) (secreto débil y acuerdo inyectivo) en aproximadamente 360 segundos.
• Fidelidad del Modelo: El modelo de WireGuard generado capturó más detalles que varios modelos escritos por expertos existentes, incluyendo el modelado explícito de los pasos de HKDF y la validación/desencriptación de AEAD, que a menudo se abstraen en otros trabajos.
• Seguridad de Memoria: El análisis de ejecución simbólica exploró con éxito miles de rutas de ejecución para ambos protocolos (por ejemplo, 4,120 rutas para el respondedor de WireGuard) y no encontró errores de memoria, descartando eficazmente desbordamientos de búfer y errores similares de implementación.
• Rendimiento: La implementación de WireGuard basada en el intérprete de AutoTam logró un rendimiento comparable a la implementación oficial de WireGuard en Go cuando se ejecuta en hardware idéntico, a pesar de carecer de optimizaciones específicas de bajo nivel.

Significancia
El artículo afirma que AutoTam ofrece un camino simplificado hacia el desarrollo de protocolos seguros al minimizar la necesidad de experiencia en verificación formal durante la fase de implementación. Al vincular el lenguaje de implementación directamente con el modelo simbólico, el enfoque asegura que escribir la implementación del protocolo en AutoTam resulte, en gran medida, en un modelo "listo para la verificación" de forma gratuita. La propiedad de solidez es central para esta afirmación, ya que cierra la brecha entre la verificación abstracta y la ejecución concreta, permitiendo a los desarrolladores confiar en las pruebas formales para la seguridad de la implementación. Además, la integración de la ejecución simbólica proporciona una doble capa de seguridad: verificación formal de la lógica del protocolo y detección automatizada de errores de memoria a nivel de implementación. Los autores posicionan esto como un paso significativo hacia la mejora de la adopción de métodos formales en la industria, reduiendo la barrera de la experiencia y asegurando que el modelo verificado refleje con precisión el código en ejecución.