💻 computer science

Misquoted No More: Securely Extracting F* Programs with IO

Este artículo introduce SEIO*, un marco que combina la citación relacional con la generación de sintaxis verificada para extraer de forma segura programas F* débilmente incrustados con tipos de E/S y de refinamiento hacia un cálculo profundamente incrustado, proporcionando pruebas verificadas por máquina de Preservación de Hiperpropiedades Relacionales Robustas (RrHP) para garantizar la seguridad contra el enlace adversarial arbitrario.

Autores originales: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

Publicado 2026-07-20

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

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

La red de seguridad invisible

Imagina que eres un maestro arquitecto que ha diseñado un magnífico coche autónomo en un mundo imaginario perfecto donde la física siempre se comporta exactamente como predices. Has escrito los planos en un lenguaje especial, súper preciso, que te permite demostrar matemáticamente que el coche nunca chocará, nunca frenará cuando no debe y siempre seguirá las reglas de la carretera. Esto es lo que los científicos de la computación llaman "verificación formal". Es como construir un coche en un sueño donde puedes estar 100% seguro de cada tornillo y cable.

Pero aquí está el problema: ese mundo de ensueño no existe en la carretera real. Para poder conducir realmente el coche, tienes que traducir tus planos perfectos a un lenguaje que los motores y neumáticos reales entiendan, como C u OCaml. Este proceso de traducción se llama "extracción". El problema es que el traductor (el programa informático que realiza la conversión) no es perfecto. Podría saltarse un tornillo, retorcer un cable o malinterpretar una regla. Si el coche del mundo real se construye sobre un error cometido durante la traducción, tu prueba perfecta de seguridad se vuelve inútil. El coche puede parecer seguro en el papel, pero chocar en la realidad.

Durante años, los científicos han intentado solucionar esto verificando el trabajo del traductor a posteriori, algo así como un mecánico que inspecciona un coche después de haber sido construido para ver si coincide con los planos. Pero este artículo presenta una forma más inteligente: en lugar de limitarse a revisar el coche terminado, construyen un "certificado de seguridad" durante la traducción que demuestra, matemáticamente, que el coche real es un gemelo perfecto del coche de ensueño, incluso si el traductor comete un error. Lo llaman un marco de "extracción segura", y está diseñado para mantener tus creaciones digitales seguras incluso cuando se mezclan con código no verificado y desordenado del mundo exterior.

La gran idea del artículo: El truque de magia de la "Citación Relacional"

Los autores de este artículo, un equipo de científicos de la computación, han construido un nuevo marco llamado SEIO★ (Secure Extraction of IO-star). Su objetivo era resolver el "problema de la traducción" para programas escritos en F★, un lenguaje utilizado para escribir software altamente seguro, como herramientas criptográficas. Estos programas en F★ suelen estar "profundamente incrustados" (shallowly embedded), que es una forma elegante de decir que están escritos en un estilo abstracto de alto nivel que es excelente para demostrar cosas, pero difícil de convertir para las computadoras en código real.

Normalmente, cuando conviertes estos programas abstractos en código real, tienes que usar un "metaprograma" (un programa que escribe otros programas) para hacer el trabajo pesado. La forma antigua de hacer esto era arriesgada: el metaprograma escribía el nuevo código y luego intentaba escribir una prueba de que el nuevo código era correcto. Si la prueba fallaba, tenías que empezar de nuevo. Si la prueba pasaba, aun así tenías que confiar en que el metaprograma no había introducido un error mientras escribía la prueba. Era como pedirle a un estudiante que calificara su propia tarea y esperar que no hiciera trampa.

El avance de los autores es una técnica que llaman Citación Relacional (Relational Quotation). En lugar de pedir al metaprograma que escriba el código final y también la prueba, le piden que haga algo mucho más simple: escribir una derivación de tipado. Piensa en esto como una tarjeta de receta paso a paso que dice: "Paso 1: Toma este ingrediente. Paso 2: Mézclalo con aquel". Esta tarjeta de receta no cocina el plato en realidad; solo demuestra que los ingredientes podrían cocinarse en un plato específico.

Aquí está la parte ingeniosa:

El Metaprograma (El escritor de recetas): El metaprograma no verificado observa el programa abstracto original y genera esta "tarjeta de receta" (la derivación de tipado). Debido a que la tarjeta de receta sigue la estructura exacta del programa original, es muy fácil de escribir.
El Control (El inspector): El propio lenguaje F★ verifica esta tarjeta de receta. Pregunta: "¿Describe esta receta realmente el programa original?". Si el metaprograma cometió un error y escribió una receta para un pastel cuando el original era una sopa, la verificación falla. Pero si la receta coincide, el lenguaje F★ tiene un 100% de seguridad de que la receta es válida.
El Paso Verificado (El Maestro Chef): Una vez que la tarjeta de receta es verificada, una función diferente, totalmente verificada (un "Maestro Chef" que ha sido matemáticamente probado como perfecto), toma esa receta y cocina el plato final (el código real). Debido a que la receta fue probada como coincidente con el original, y el chef está probado para cocinar exactamente lo que dice la receta, el plato final está garantizado para ser un gemelo perfecto del original.

Este enfoque minimiza la "confianza" que tenemos que depositar en el metaprograma no verificado. Solo confiamos en que escriba la receta, no en que cocine la comida ni califique la tarea. La parte difícil —probar que la comida es segura— la realiza el Maestro Chef verificado.

El superpoder de la "Compilación Segura"

El artículo no se detiene solo en asegurar que el código sea correcto; va un paso más allá para asegurar que sea seguro. En el mundo real, tu programa verificado podría vincularse con otro código que no es verificado —tal vez código escrito por un hacker, o simplemente código descuidado de un equipo diferente—. Este código "adversario" intenta romper las reglas de tu programa.

Los autores demuestran que su marco SEIO★ satisface una regla de seguridad superpotente llamada Preservación de Hiperpropiedad Relacional Robusta (Robust Relational Hyperproperty Preservation - RrHP). Para entender esto, imagina que tu programa verificado es una fortaleza.

Los métodos antiguos podrían decir: "Los muros de la fortaleza son fuertes, por lo tanto es segura".
Este artículo dice: "Incluso si un hacker intenta colarse por la puerta trasera, o si intentan engañar a los guardias, o si intentan cambiar las reglas del juego, tu fortaleza seguirá comportándose exactamente como la diseñaste".

Demuestran esto utilizando dos "relaciones lógicas", que son como espejos de doble cara. Un espejo comprueba si el código real hace todo lo que el código abstracto podría hacer. El otro espejo comprueba que el código real no hace nada que el código abstracto no pudiera hacer. Al probar ambos, demuestran que el código real es una sombra perfecta y segura del original, sin importar con qué código desordenado se vincule.

Lo que realmente hicieron (y lo que no)

El equipo construyó este marco enteramente dentro del lenguaje F★ y utilizó una computadora para verificar cada paso de su prueba. No solo adivinaron o simularon; demostraron matemáticamente.

Lo que funciona: Lograron extraer programas que manejan Entrada/Salida de archivos (lectura y escritura de archivos) y utilizan "tipos de refinamiento" (tipos con reglas adicionales, como "este número debe ser positivo"). Demostraron que, incluso con estas características complejas, la extracción sigue siendo segura.
Lo que aún es un trabajo en progreso: El artículo admite que su sistema actual no maneja funciones recursivas (funciones que se llaman a sí mismas) o "tipos dependientes" completos (donde los tipos pueden depender de valores) de la manera más natural. Tuvieron que usar un rodeo involucrando iteradores (bucles) para la recursión. También señalan que su metaprograma a veces tiene que adivinar dónde colocar ciertas comprobaciones de seguridad, lo que puede ser un poco tosco.
La conclusión: No han resuelto todos los problemas del universo de la programación, pero han construido un puente nuevo y mucho más seguro entre el mundo de las pruebas perfectas y el mundo desordenado del código real. Demostraron que, al dividir el trabajo en una fase de "escritura de recetas" y una fase de "cocinar", se puede obtener una seguridad fuerte sin tener que confiar completamente en el escritor de recetas.

En resumen, SEIO★ es una nueva herramienta que permite a los programadores tomar sus ideas perfectas y verificadas y convertirlas en software del mundo real con una red de seguridad matemáticamente garantizada, asegurando que, incluso si el proceso de traducción es imperfecto, el resultado final sea seguro frente al caos del mundo exterior.

Resumen Técnico: Misquoted No More: Extracción Segura de Programas F★ con IO

1. Planteamiento del Problema

El lenguaje orientado a la prueba F★ se utiliza ampliamente para escribir y verificar programas que están incrustados superficialmente (shallowly embedded) mediante mónadas para representar efectos (por ejemplo, I/O). Una vez verificados, estos programas se extraen típicamente a lenguajes convencionales como OCaml o C para su ejecución. Sin embargo, este proceso de extracción es actualmente no verificado y constituye parte del núcleo de confianza (trusted computing base o TCB).

El desafío central reside en el paso de "citación" (quotation) requerido para extraer programas incrustados superficialmente. La citación implica traducir un programa incrustado superficialmente (donde los efectos se representan mediante tipos monádicos) a un árbol de sintaxis incrustado profundamente (deeply embedded) (una representación concreta del lenguaje objetivo). Verificar este metaprograma de citación es un desafío abierto importante porque requiere una metateoría mecanizada para el lenguaje de origen, e incluso para sistemas maduros como Rocq, la verificación de la citación sigue sin resolverse.

Los enfoques previos para certificar la extracción dependen fuertemente de la validación de la traducción (translation validation), donde un metaprograma genera tanto el código extraído como una prueba de corrección, la cual es posteriormente verificada por el sistema de tipos. Si bien esto reduce el TCB en comparación con la verificación del metaprograma, todavía depende de que el metaprograma genere pruebas válidas, las cuales pueden fallar o ser incorrectas. Además, el trabajo existente se centra primordialmente en la corrección (preservación del comportamiento funcional) en lugar de la seguridad. Cuando el código extraído se enlaza con código adversarial no verificado, las garantías formales del programa original verificado pueden verse comprometidas, lo que conduce a la falta de solidez (unsoundness) o brechas de seguridad.

2. Metodología

Los autores introducen SEIO★, un marco para extraer programas F★ incrustados superficialmente con I/O y tipos de refinamiento a un cálculo $\lambda$ simplemente tipado incrustado profundamente ( $\lambda_{io}$ ). La metodología divide el proceso de extracción en dos fases distintas para minimizar la dependencia de la validación de la traducción:

Fase 1: Citación Relacional (Validación de la Traducción)
En lugar de generar directamente el código objetivo, el marco utiliza un metaprograma para generar una derivación de tipado para el programa incrustado superficialmente original.

Relación de Tipado Relacional: Los autores definen una relación de tipado que caracteriza al subconjunto de F★ (llamado IO★) que se está extrayendo. Esta relación opera sobre "valores F★ abiertos" (funciones de entornos de evaluación a valores) en lugar de expresiones sintácticas, lo que le permite manejar variables libres en una incrustación superficial.
Metaprograma: Un metaprograma simple recorre la estructura del programa de origen y construye una derivación de tipado correspondiente.
Validación: La derivación generada es verificada por el sistema de tipos de F★. Debido a que la relación de tipado utiliza tipos dependientes, el verificador de tipos asegura que la derivación corresponda sintáctica y semánticamente al programa original. Este paso es la única parte que depende de la validación de la traducción.

Fase 2: Generación de Sintaxis Verificada
Una vez obtenida una derivación de tipado válida, una función de F★ pura y verificada recorre recursivamente la derivación para generar la sintaxis $\lambda_{io}$ objetivo.

Dado que la derivación de tipado está vinculada estructuralmente al programa de origen mediante tipos dependientes, la función de generación de sintaxis garantiza producir código semánticamente relacionado con el original.
Este paso está totalmente verificado dentro de F★, eliminando la necesidad de validación de la traducción en la fase de generación de código.

Garantías de Seguridad mediante Relaciones Lógicas
Para probar la seguridad, los autores definen dos relaciones lógicas trans-lenguaje entre el lenguaje de origen (IO★) y el lenguaje objetivo ( $\lambda_{io}$ ):

Objetivo-a-Origen: Relaciona un programa objetivo con un programa de origen, asegurando que cada comportamiento del objetivo tenga un comportamiento de origen correspondiente.
Origen-a-Objetivo: Relaciona un programa de origen con un programa objetivo, asegurando que cada comportamiento del origen tenga un comportamiento de objetivo correspondiente.

Estas relaciones se definen sobre semánticas que producen trazas (trace-producing semantics), donde las operaciones de I/O generan eventos (trazas). Los autores demuestran que SEIO★ satisface la Preservación de Hiperpropiedad Relacional Robusta (RrHP), el criterio de compilación segura más fuerte definido por Abate et al. [1]. RrHP implica abstracción completa (preservación de la equivalencia observacional) y la preservación de propiedades de traza e hiperpropiedades (por ejemplo, la no interferencia) frente a contextos adversariales arbitrarios.

Manejo de Tipos de Refinamiento
El marco se extiende para soportar tipos de refinamiento (restricciones lógicas sobre los tipos). Dado que F★ descarga las pruebas de refinamiento utilizando resolvedores SMT sin producir términos de prueba explícitos, el metaprograma de citación relacional debe recomputar las precondiciones más débiles (weakest preconditions) desde cero durante la citación y volver a probarlas para asegurar que la derivación de tipado permanezca válida.

3. Contribuciones Clave

Citación Relacional: Una novedosa técnica de validación de la traducción que utiliza tipos dependientes para definir una relación de tipado para programas incrustados superficialmente. Permite que un metaprograma genere una derivación de tipado que es verificada por el sistema de tipos para asegurar que corresponda al programa de origen, evitando la necesidad de verificar el propio metaprograma.
Marco SEIO★: Un marco de extracción completo para programas F★ con I/O y tipos de refinamiento, extrayéndolos a un cálculo $\lambda$ incrustado profundamente.
Compilación Segura Formal: Una prueba verificada por máquina en F★ de que SEIO★ satisface RrHP. Esta es la primera vez que un marco de extracción para un lenguaje orientado a la prueba proporciona tales garantías de seguridad fuertes contra código adversarial arbitrario vinculado.
Relaciones Lógicas Trans-Lenguaje: La definición y prueba de dos relaciones lógicas asimétricas que cierran la brecha entre un lenguaje incrustado superficialmente con semántica de producción de trazas y un lenguaje incertado profundamente con semántica operacional estándar.
Soporte para Tipos de Refinamiento: Una extensión del marco para manejar tipos de refinamiento mediante la recomputación y reverificación de las precondiciones durante la citación.

4. Resultados

Los autores implementaron SEIO★ en F★, incluyendo más de 900 definiciones de alto nivel.
Extrajeron con éxito un ejemplo ejecutable: un envoltorio de validación para agentes de IA no verificados que lee un archivo, llama a un agente y verifica el resultado.
El marco fue probado con varios agentes (tanto correctos como maliciosos) escritos directamente en el lenguaje $\lambda_{io}$ objetivo.
La prueba verificada por máquina confirma que la extracción preserva las propiedades de seguridad incluso cuando se enlaza con código arbitrario no verificado, satisfaciendo RrHP.
El artefacto incluye un flujo de trabajo para compilar el código $\lambda_{io}$ extraído a OCaml utilizando el marco Peregrine y Malfunction, permitiendo su ejecución práctica.

5. Significado y Reivindicaciones

El artículo afirma avanzar en el estado del arte en dos maneras clave:

Minimizar la Validación de la Traducción: Al confinar la validación de la traducción a la generación de una derivación de tipado (citación relacional) y verificar el paso subsiguiente de generación de sintaxis, el marco reduce la dependencia de metaprogramas no verificados en comparación con el trabajo previo de extracción certificada.
Seguridad sobre Corrección: A diferencia del trabajo anterior que se centraba en la corrección funcional, SEIO★ proporciona garantías de compilación segura formal. Asegura que los programas F★ verificados retengan sus propiedades de seguridad (como la no interferencia y las propiedades de traza) incluso cuando se enlazan con código arbitrario, no verificado o adversarial.

Los autores señalan que este trabajo va más allá del estado del arte actual, que aún no ha proporcionado tales garantías de compilación segura para la extracción desde lenguajes orientados a la prueba. Reconocen limitaciones, como la falta actual de soporte para funciones recursivas generales y tipos dependientes completos, que quedan para trabajos futuros. El artículo enfatiza que, si bien el metaprograma de citación relacional no está verificado, su simplicidad y la rigurosa verificación de los pasos subsiguientes hacen que el enfoque general sea robusto.