A Deductive System for Contract Satisfaction Proofs

Este artículo presenta un sistema deductivo formalizado en el asistente de pruebas Rocq para demostrar la satisfacción de contratos de hardware-software mediante una técnica de bisimulación relativa que permite verificar de manera modular y completa la seguridad de programas frente a ataques de canal lateral.

Lo esencial

Imagina que tienes un coche de lujo (el hardware, como el procesador de tu computadora) y un manual de usuario (el contrato de software).

El problema es que, aunque el manual diga "este coche no hace ruido cuando aceleras", en realidad, el motor podría hacer un pequeño "clic" o vibrar de forma diferente dependiendo de si estás conduciendo por una calle segura o por una zona peligrosa. Un espía (un atacante) podría escuchar ese "clic" y deduce que estás en la zona peligrosa, robando así información secreta sin entrar en el coche.

En el mundo de la ciberseguridad, esto se llama ataque por canal lateral. La información se filtra no por lo que el programa hace, sino por cómo lo hace a nivel físico (tiempos, uso de memoria, etc.).

El Problema: ¿Cómo sabemos que el manual es honesto?

Los ingenieros crean estos "manuales" (contratos) para que los programadores puedan escribir código seguro sin tener que ser expertos en mecánica de motores. Pero, ¿cómo nos aseguramos de que el manual no miente?

Antes, para probar que el manual era correcto, los ingenieros tenían dos opciones:

1. Hacer pruebas a ciegas: Probar el coche millones de veces. Es rápido, pero podrías perder un detalle raro.
2. Escribir una demostración matemática gigante: Un documento de 25 páginas lleno de fórmulas. Es muy seguro, pero tan denso y largo que es casi imposible de verificar sin cometer errores.

La Solución: Un "Juez Digital" Interactivo

Este artículo presenta una nueva forma de probar que el manual (contrato) es honesto respecto al coche (hardware). En lugar de escribir un documento gigante o hacer pruebas a ciegas, usan un asistente de pruebas interactivas (llamado Rocq, que es como un juez muy estricto y lógico).

Pero para que el juez entienda el caso, los autores tuvieron que inventar una nueva forma de pensar. Aquí viene la parte creativa:

1. La Analogía de los Cuatro Corredores

Imagina que quieres probar que dos corredores (el Hardware y el Contrato) son "iguales" en sus movimientos, pero bajo una condición: si el Contrato corre de la misma manera en dos situaciones diferentes, entonces el Hardware también debe correr igual.

Para probar esto, no miras a un solo corredor. Imagina que tienes cuatro corredores en una pista:

• Corredor A y B: Son el "Contrato" (el manual) corriendo con dos datos diferentes.
• Corredor C y D: Son el "Hardware" (el motor real) corriendo con esos mismos datos.

El objetivo es demostrar que: Si A y B corren exactamente al mismo ritmo, entonces C y D también deben correr al mismo ritmo.

2. El Reto: No van al mismo paso (Asincronía)

El problema es que el "Manual" y el "Motor" no siempre avanzan al mismo tiempo.

• A veces, el Manual da un paso y el Motor da tres.
• A veces, el Motor se detiene a pensar (especulación) mientras el Manual sigue avanzando.

Antes, probar esto era como intentar emparejar zapatos de diferentes tallas y colores sin una regla clara. Tenías que adivinar una "regla mágica" (una relación de simulación) al principio de todo el proceso, lo cual es muy difícil.

3. La Innovación: Construir la Regla Mientras Corres

Los autores crearon un sistema deductivo (un conjunto de reglas lógicas) que les permite construir la relación de emparejamiento paso a paso, mientras ocurre la prueba.

Imagina que estás jugando a un videojuego de puzles:

• En lugar de tener que dibujar todo el mapa del nivel antes de empezar, el sistema te permite dar un paso, ver qué pasa, y luego decidir: "¡Ah! En este punto, el Manual y el Motor están sincronizados, así que guardo esa pista".
• Si el Motor se adelanta, el sistema sabe que puede "saltar" pasos del Manual hasta que vuelvan a coincidir.
• Si el Manual se adelanta, el sistema espera al Motor.

Esto se llama Bisimulación Relativa. Es como tener un juez que dice: "No necesito saber todo el camino de antemano. Solo necesito que cada vez que el Manual diga 'hago esto', el Motor pueda decir 'hago lo mismo' (o algo que parezca lo mismo), y que si el Manual se equivoca, el Motor también se equivoca de la misma manera".

¿Por qué es importante?

1. Seguridad Real: Permite verificar matemáticamente que los procesadores modernos (que son muy complejos y hacen trucos para ir rápido) no están filtrando secretos.
2. Modularidad: Puedes probar una parte del motor (por ejemplo, cómo maneja las predicciones de saltos) y luego probar otra parte (cómo maneja la memoria) por separado, y luego unir las pruebas. Es como armar un Lego en lugar de esculpir una estatua de mármol.
3. Automatización: Al usar el asistente de pruebas (Rocq), el sistema verifica que cada paso de tu lógica sea correcto. Si te equivocas en un detalle, el juez te detiene inmediatamente.

En Resumen

Los autores han creado una caja de herramientas lógica que permite a los ingenieros demostrar, de forma interactiva y paso a paso, que un procesador de computadora no está "delatando" secretos a través de sus movimientos físicos.

En lugar de escribir un libro de 25 páginas que nadie entiende, ahora pueden construir una prueba como si estuvieran armando un rompecabezas interactivo, donde el sistema les asegura que cada pieza encaja perfectamente. Esto hace que la seguridad de nuestros dispositivos sea mucho más robusta y verificable.

Resumen técnico

Aquí presento un resumen técnico detallado del artículo "A Deductive System for Contract Satisfaction Proofs" (Un sistema deductivo para pruebas de satisfacción de contratos), basado en el contenido proporcionado.

1. El Problema: Verificación de Contratos Hardware-Software

El contexto del trabajo surge de la necesidad de defenderse contra ataques de canal lateral (como Meltdown y Spectre) en hardware compartido. Para ello, se utilizan contratos hardware-software, que son especificaciones abstractas del comportamiento de fugas de información de una CPU a nivel de Arquitectura de Conjunto de Instrucciones (ISA), sin requerir detalles microarquitectónicos profundos.

• Definición de Satisfacción de Contrato: Un hardware satisface un contrato si el contrato "sobre-approxima" correctamente las fugas del hardware. Formalmente: si el contrato predice la misma fuga para dos ejecuciones de un programa con estados iniciales diferentes (pero con valores públicos idénticos), entonces el hardware también debe producir fugas indistinguibles.
• El Desafío: Probar esta propiedad es un problema de relación 4-aria (cuaternaria). Implica comparar dos trazas del contrato y dos trazas del hardware simultáneamente.
  • Las ejecuciones son asíncronas: un paso del contrato puede corresponder a varios pasos del hardware y viceversa (ej. debido a la especulación o ejecución fuera de orden).
  • Los enfoques existentes (model checking, pruebas manuales) tienen limitaciones: el model checking depende de la implementación de algoritmos y puede no terminar; las pruebas manuales son propensas a errores y difíciles de verificar (ej. una prueba de 25 páginas para un procesador simple).
  • El objetivo es desarrollar un sistema deductivo formal dentro de un asistente de pruebas (Rocq, anteriormente Coq) que sea modular, incremental y capaz de manejar la asincronía sin requerir definir relaciones de simulación complejas de antemano.

2. Metodología: Bisimulación Relativa y Coinducción Parametrizada

Los autores proponen un enfoque basado en la Bisimulación Relativa y la Coinducción Parametrizada.

A. Igualdad de Trazas Relativa

El problema de satisfacción del contrato se identifica como un caso particular de igualdad de trazas relativa: probar que "la igualdad de trazas en el contrato implica la igualdad de trazas en el hardware".
$$\llbracket P \rrbracket_C(s_1) = \llbracket P \rrbracket_C(s_2) \implies \llbracket P \rrbracket_H(h_1) = \llbracket P \rrbracket_H(h_2)$$

B. Bisimulación Relativa (4-aria)

Para resolver esto, definen una relación de bisimulación relativa ($rbisim$) sobre cuatro estados ($s_1, s_2$ del contrato y $h_1, h_2$ del hardware).

• Desafío de la sincronización: Una bisimulación estricta "lockstep" (paso a paso) falla porque los contratos y el hardware pueden avanzar a diferentes velocidades. Una bisimulación "relajada" (que permite saltar pasos arbitrariamente) resulta insana (demasiado permisiva).
• Solución: La definición de $rbisim$ combina un punto fijo máximo (coinductivo) para los pasos del hardware y un punto fijo mínimo (inductivo) para los pasos del contrato.
  • Los pasos del hardware se tratan coinductivamente (permitiendo razonamiento asíncrono).
  • Los pasos del contrato se tratan inductivamente (garantizando que la premisa de igualdad de trazas del contrato se "desenrolla" correctamente).
  • Esta mezcla asegura que la relación sea sana y completa para la igualdad de trazas relativa.

C. Sistema Deductivo y Quintuplos de Prueba

Para facilitar la demostración práctica, los autores desarrollan un sistema deductivo basado en Coinducción Parametrizada (Paco).

• Quintuplos de Prueba: Introducen la notación $R \vdash \begin{bmatrix} s_1 & s_2 \\ h_1 & h_2 \end{bmatrix}$, donde $R$ es una hipótesis de coinducción (un conjunto de cuádruplos de estados).
• Reglas de Inferencia:
  • C-Leak / C-Step: Manejan el lado del contrato. Permiten concluir si las fugas difieren o avanzar un paso del contrato (tratado inductivamente).
  • H-Step: Maneja el lado del hardware. Requiere que las fugas sean iguales y avanza los estados del hardware (tratado coinductivamente).
  • Invariantes y Ciclos: Permiten acumular hipótesis y cerrar pruebas cuando se reencuentran estados ya conocidos en la hipótesis.
• Ventaja: No es necesario definir la relación de simulación completa al inicio. El sistema permite construir la relación de manera incremental durante la prueba.

D. Técnicas "Up-To"

El sistema integra técnicas avanzadas para simplificar pruebas:

• Simetría y Equivalencia: Permiten intercambiar estados o reemplazarlos por estados con fugas equivalentes.
• Transitividad: Permiten descomponer la prueba reduciendo la fuga en el contrato o aumentándola en el hardware (con restricciones de "lockstep" para el hardware para garantizar la sanidad).

3. Contribuciones Clave

1. Formalización de la Bisimulación Relativa: Definen una relación de 4 estados que caracteriza exactamente la satisfacción de contratos, manejando la asincronía mediante la mezcla de inducción y coinducción.
2. Sistema Deductivo Modular: Presentan un conjunto de reglas de inferencia (quintuplos) que permiten realizar pruebas interactivas de manera incremental, evitando la necesidad de "adivinar" invariantes complejos de antemano.
3. Integración de Técnicas Up-To: Demuestran cómo integrar formalmente principios de simetría, transitividad y reemplazo de estados dentro del marco de coinducción parametrizada para simplificar drásticamente las pruebas.
4. Implementación y Validación: Formalizaron todo el sistema en el asistente de pruebas Rocq y lo aplicaron a dos casos de estudio complejos derivados del contrato CT-SPEC.

4. Resultados y Casos de Estudio

Los autores validaron su sistema probando dos abstracciones clave del contrato CT-SPEC:

1. Contrato "Always-Mispredict" (Siempre Mal Predice):

   • Objetivo: Demostrar que un hardware con predicción de ramas y ejecución especulativa satisface un contrato que siempre ejecuta ambas ramas (la correcta y la incorrecta) y luego revierte los efectos arquitectónicos.
   • Desafío: El hardware puede predecir correctamente (ejecutando solo la rama correcta) o incorrectamente, mientras que el contrato siempre ejecuta ambas. Esto requiere razonamiento asíncrono complejo.
   • Resultado: El sistema permitió probar la satisfacción manejando la desincronización temporal entre el contrato (que ejecuta la rama incorrecta primero) y el hardware (que puede saltarla si la predicción es correcta), utilizando la regla de "paso de contrato" para avanzar la hipótesis inductivamente.

2. Contrato "Sequential" (Secuencial):

   • Objetivo: Demostrar que un hardware con ejecución fuera de orden satisface un contrato que ejecuta instrucciones estrictamente en orden.
   • Desafío: El hardware puede reordenar instrucciones "delayables" (que no dependen de otras), mientras que el contrato las ejecuta secuencialmente.
   • Resultado: El sistema permitió probar que el reordenamiento de instrucciones no altera las fugas observables, utilizando las reglas de transición para simular el buffer de hardware y restaurar la invariante cuando el buffer se vacía.

5. Significado e Impacto

• Rigor Formal: Proporciona la primera base deductiva completa y mecanizada para probar la satisfacción de contratos hardware-software, superando las limitaciones de las pruebas manuales y el model checking puro.
• Modularidad: Al permitir construir invariantes incrementalmente y usar técnicas "up-to", reduce la complejidad cognitiva de probar propiedades hiperpropiedades (relacionales) en sistemas asíncronos.
• Generalidad: Aunque diseñado para contratos de seguridad, la técnica de Bisimulación Relativa es aplicable a otros problemas de seguridad como la compilación segura, la refinación de información y la seguridad relativa.
• Herramienta Práctica: La implementación en Rocq y la disponibilidad del código (Zenodo) ofrecen una base sólida para que investigadores y desarrolladores verifiquen futuros diseños de procesadores y contratos de seguridad de manera automatizada y verificada.

En resumen, el artículo presenta un avance fundamental en la verificación formal de seguridad de hardware, transformando un problema de razonamiento relacional complejo en un proceso deductivo estructurado, manejable y verificable por máquinas.