💻 computer science

Misquoted No More: Securely Extracting F* Programs with IO

Este artigo introduz o SEIO*, um framework que combina citação relacional com geração de sintaxe verificada para extrair de forma segura programas F* superficialmente incorporados com tipos de IO e de refinamento para um cálculo profundamente incorporado, fornecendo provas verificadas por máquina de Preservação de Hiperpropriedade Relacional Robusta (RrHP) para garantir a segurança contra vinculação adversária arbitrária.

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

Publicado 2026-07-20

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

A Rede de Segurança Invisível

Imagine que você é um arquiteto mestre que projetou um carro autônomo magnífico em um mundo imaginário perfeito, onde a física sempre se comporta exatamente como você prevê. Você escreveu as plantas em uma linguagem especial, superprecisa, que permite provar matematicamente que o carro nunca baterá, nunca freará quando não deveria e sempre seguirá as regras da estrada. Isso é o que os cientistas da computação chamam de "verificação formal". É como construir um carro em um sonho onde você pode ter 100% de certeza de cada parafuso e fio.

Mas aqui está o problema: esse mundo dos sonhos não existe na estrada real. Para realmente dirigir o carro, você tem que traduzir suas plantas perfeitas para uma linguagem que motores e pneus reais entendam, como C ou OCaml. Esse processo de tradução é chamado de "extração". O problema é que o tradutor (o programa de computador que faz a conversão) não é perfeito. Ele pode derrubar um parafuso, torcer um fio ou entender mal uma regra. Se o carro do mundo real for construído sobre um erro cometido durante a tradução, sua prova perfeita de segurança torna-se inútil. O carro pode parecer seguro no papel, mas bater na realidade.

Por anos, os cientistas tentaram corrigir isso verificando o trabalho do tradutor após o fato, como um mecânico inspecionando um carro depois de construído para ver se ele corresponde aos planos. Mas este artigo apresenta uma maneira mais inteligente: em vez de apenas verificar o carro acabado, eles constroem um "certificado de segurança" durante a tradução que prova, matematicamente, que o carro real é um gêmeo perfeito do carro do sonho, mesmo que o tradutor cometa um erro. Eles chamam isso de um framework de "extração segura" e ele foi projetado para manter suas criações digitais seguras mesmo quando elas são misturadas com código não verificado do mundo exterior.

A Grande Ideia do Artigo: O Truque de Mágica da "Citação Relacional"

Os autores deste artigo, uma equipe de cientistas da computação, construíram um novo framework chamado SEIO★ (Secure Extraction of IO-star). O objetivo deles era resolver o "problema da tradução" para programas escritos em F★, uma linguagem usada para escrever software altamente seguro, como ferramentas criptográficas. Esses programas em F★ são frequentemente "profundamente incorporados" (shallowly embedded), uma forma elegante de dizer que são escritos em um estilo abstrato de alto nível, que é ótimo para provar coisas, mas difícil para computadores transformarem em código real.

Normalmente, quando você transforma esses programas abstratos em código real, precisa usar um "metaprograma" (um programa que escreve outros programas) para fazer o trabalho pesado. A forma antiga de fazer isso era arriscada: o metaprograma escreveria o novo código e depois tentaria escrever uma prova de que o novo código estava correto. Se a prova falhasse, você teria que começar de novo. Se a prova passasse, você ainda tinha que confiar que o metaprograma não inseriu um erro enquanto escrevia a prova. Era como pedir a um aluno para corrigir o próprio dever de casa e esperar que ele não colasse.

A descoberta dos autores é uma técnica que eles chamam de Citação Relacional (Relational Quotation). Em vez de pedir ao metaprograma para escrever o código final e a prova, eles pedem que ele faça algo muito mais simples: escreva uma derivação de tipagem. Pense nisso como um cartão de receita passo a passo que diz: "Passo 1: Pegue este ingrediente. Passo 2: Misture com aquele". Este cartão de receita não cozinha a refeição de fato; ele apenas prova que os ingredientes poderiam ser cozinhados em um prato específico.

Aqui está a parte inteligente:

O Metaprograma (O Escritor de Receitas): O metaprograma não verificado olha para o programa abstrato original e gera este "cartão de receita" (a derivação de tipagem). Como o cartão de receita segue a estrutura exata do programa original, é muito fácil de escrever.
A Verificação (O Inspetor): A própria linguagem F★ verifica este cartão de receita. Ela pergunta: "Esta receita realmente descreve o programa original?". Se o metaprograma cometeu um erro e escreveu uma receita de bolo quando o original era uma sopa, a verificação falha. Mas se a receita corresponder, a linguagem F★ tem 100% de certeza de que a receita é válida.
A Etapa Verificada (O Chef Mestre): Uma vez que o cartão de receita é verificado, uma função diferente, totalmente verificada (um "Chef Mestre" que foi matematicamente provado como perfeito), pega essa receita e cozinha o prato final (o código real). Como a receita foi provada como correspondente ao original, e o chef é provado como cozinhando exatamente o que a receita diz, o prato final é garantido como um gêmeo perfeito do original.

Essa abordagem minimiza a "confiança" que temos que depositar no metaprograma não verificado. Só precisamos confiar que ele escreva a receita, não que cozinhe a comida ou corrija o dever de casa. A parte difícil — provar que a comida é segura — é feita pelo Chef Mestre verificado.

O Superpoder da "Compilação Segura"

O artigo não para apenas em garantir que o código esteja correto; ele vai um passo além para garantir que seja seguro. No mundo real, seu programa verificado pode ser vinculado com outro código que não é verificado — talvez código escrito por um hacker, ou apenas um código descuidado de outra equipe. Esse código "adversário" tenta quebrar as regras do seu programa.

Os autores provam que o framework SEIO★ satisfaz uma regra de segurança super forte chamada Preservação de Hiperpropriedade Relacional Robusta (RrHP). Para entender isso, imagine que seu programa verificado é uma fortaleza.

Métodos antigos poderiam dizer: "As paredes da fortaleza são fortes, então ela é segura".
Este artigo diz: "Mesmo que um hacker tente entrar pela porta dos fundos, ou se tentarem enganar os guardas, ou se tentarem mudar as regras do jogo, sua fortaleza ainda assim se comportará exatamente como você projetou".

Eles provam isso usando duas "relações lógicas", que são como espelhos de duas vias. Um espelho verifica se o código real faz tudo o que o código abstrato poderia fazer. O outro verifica se o código real não faz nada que o código abstrato não poderia fazer. Ao provar ambos, eles mostram que o código real é uma sombra perfeita e segura do original, não importa com qual código bagunçado ele seja vinculado.

O Que Eles Realmente Fizeram (e Não Fizeram)

A equipe construiu este framework inteiramente dentro da linguagem F★ e usou um computador para verificar cada etapa de sua prova. Eles não apenas adivinharam ou simularam; eles provaram isso matematicamente.

O que funciona: Eles obtiveram sucesso na extração de programas que lidam com Entrada/Saída de arquivos (leitura e escrita de arquivos) e usam "tipos de refinamento" (tipos com regras extras, como "este número deve ser positivo"). Eles mostraram que, mesmo com esses recursos complexos, a extração permanece segura.
O que ainda é um trabalho em progresso: O artigo admite que seu sistema atual não lida com funções recursivas (funções que chamam a si mesmas) ou "tipos dependentes" completos (onde os tipos podem depender de valores) da maneira mais natural. Eles tiveram que usar um contorno envolvendo iteradores (loops) para a recursão. Eles também observam que seu metaprograma às vezes tem que adivinhar onde colocar certas verificações de segurança, o que pode ser um pouco desajeitado.
O Veredito: Eles não resolveram todos os problemas do universo da programação, mas construíram uma nova ponte muito mais segura entre o mundo das provas perfeitas e o mundo bagunçado do código real. Eles provaram que, ao dividir o trabalho em uma fase de "escrita de receita" e uma fase de "cozinhar", você pode obter garantias de segurança fortes sem precisar confiar totalmente no escritor da receita.

Em resumo, o SEIO★ é uma nova ferramenta que permite aos programadores pegar suas ideias perfeitas e verificadas e transformá-las em software do mundo real com uma rede de segurança matematicamente garantida, assegurando que, mesmo que o processo de tradução seja imperfeito, o resultado final ainda esteja seguro contra o caos do mundo exterior.

Resumo Técnico: Não Mais Citado Incorretamente: Extração Segura de F★Programs com IO

1. Declaração do Problema

A linguagem orientada a provas F★ é amplamente utilizada para escrever e verificar programas que são fracamente incorporados (shallowly embedded) usando mônadas para representar efeitos (ex: I/O). Uma vez verificados, esses programas são tipicamente extraídos para linguagens convencionais como OCaml ou C para execução. No entanto, esse processo de extração é atualmente não verificado e constitui parte da base de computação confiável (TCB).

O desafio central reside no passo de "citação" (quotation) necessário para extrair programas fracamente incorporados. A citação envolve traduzir um programa fracamente incorporado (onde os efeitos são representados por tipos mônicos) para uma árvore de sintaxe profundamente incorporada (deeply embedded) (uma representação concreta da linguagem alvo). Verificar este metaprogram de citação é um grande desafio aberto porque requer uma metateoria mecanizada para a linguagem de origem, e mesmo para sistemas maduros como o Rocq, a verificação de citação permanece não resolvida.

Abordagens anteriores para certificar a extração dependem fortemente da validação de tradução (translation validation), onde um metaprogram gera tanto o código extraído quanto uma prova de correção, que é então verificada pelo sistema de tipos. Embora isso reduza a TCB em comparação com a verificação do próprio metaprogram, ainda depende do metaprogram para gerar provas válidas, que podem falhar ou estar incorretas. Além disso, o trabalho existente foca primariamente na correção (preservação do comportamento funcional) em vez de segurança. Quando o código extraído é vinculado a um código adversarial não verificado, as garantias formais do programa original verificado podem ser comprometidas, levando à unsoundness ou violações de segurança.

2. Metodologia

Os autores introduzem o SEIO★, um framework para extrair programas F★ fracamente incorporados com I/O e tipos de refinamento para um cálculo lambda simplesmente tipado ( $\lambda_{io}$ ) profundamente incorporado. A metodologia divide o processo de extração em duas fases distintas para minimizar a dependência da validação de tradução:

Fase 1: Citação Relacional (Validação de Tradução)
Em vez de gerar diretamente o código alvo, o framework utiliza um metaprogram para gerar uma derivação de tipagem para o programa original fracamente incorporado.

Relação de Tipagem Relacional: Os autores definem uma relação de tipagem que caracteriza o subconjunto de F★ (chamado IO★) que está sendo extraído. Esta relação opera sobre "valores F★ abertos" (funções de ambientes de avaliação para valores) em vez de expressões sintáticas, permitindo lidar com variáveis livres em uma incorporação rasa.
Metaprogram: Um metaprogram simples percorre a estrutura do programa de origem e constrói uma derivação de tipagem correspondente.
Validação: A derivação gerada é verificada pelo sistema de tipos do F★. Como a relação de tipagem utiliza tipos dependentes, o verificador de tipos garante que a derivação corresponde sintática e semanticamente ao programa original. Este passo é a única parte que depende de validação de tradução.

Fase 2: Geração de Sintaxe Verificada
Uma vez obtida uma derivação de tipagem válida, uma função F★ pura e verificada percorre recursivamente a derivação para gerar a sintaxe $\lambda_{io}$ alvo.

Como a derivação de tipagem está estruturalmente ligada ao programa de origem via tipos dependentes, a função de geração de sintaxe tem a garantia de produzir código semanticamente relacionado ao original.
Este passo é totalmente verificado dentro do F★, eliminando a necessidade de validação de tradução na fase de geração de código.

Garantias de Segurança via Relações Lógicas
Para provar a segurança, os autores definem duas relações lógicas entre linguagens (cross-language) entre a origem (IO★) e o alvo ( $\lambda_{io}$ ):

Alvo-para-Origem: Relaciona um programa alvo a um programa de origem, garantindo que todo comportamento alvo tenha um comportamento de origem correspondente.
Origem-para-Alvo: Relaciona um programa de origem a um programa alvo, garantindo que todo comportamento de origem tenha um comportamento de alvo correspondente.

Estas relações são definidas sobre semânticas de produção de traço (trace-producing semantics), onde operações de I/O geram eventos (traços). Os autores provam que o SEIO★ satisfaz a Preservação de Hiperpropriedade Relacional Robusta (RrHP), o critério mais forte de compilação segura definido por Abate et al. [1]. A RrHP implica abstração total (preservação de equivalência observacional) e a preservação de propriedades de traço e hiperpropriedades (ex: não interferência) contra contextos adversariais arbitrários.

Lidando com Tipos de Refinamento
O framework é estendido para suportar tipos de refinamento (restrições lógicas sobre tipos). Como o F★ realiza o despacho de provas de refinamento usando solvers SMT sem produzir termos de prova explícitos, o metaprogram de citação relacional deve recomputar as pré-condições mais fracas (weakest preconditions) do zero durante a citação e re-prová-las para garantir que a derivação de tipagem permaneça válida.

3. Principais Contribuições

Citação Relacional: Uma nova técnica de validação de tradução que utiliza tipos dependentes para definir uma relação de tipagem para programas fracamente incorporados. Permite que um metaprogram gere uma derivação de tipagem que é verificada pelo sistema de tipos para garantir que corresponda ao programa de origem, evitando a necessidade de verificar o próprio metaprogram.
Framework SEIO★: Um framework de extração completo para programas F★ com I/O e tipos de refinamento, extraindo-os para um cálculo lambda profundamente incorporado.
Compilação Segura Formal: Uma prova verificada por máquina em F★ de que o SEIO★ satisfaz a RrHP. Este é o primeiro framework de extração para uma linguagem orientada a provas que fornece tais garantias de segurança fortes contra código adversarial arbitrário vinculado.
Relações Lógicas entre Linguagens: A definição e prova de duas relações lógicas assimétricas que unem o hiato entre uma linguagem fracamente incorporada com semântica de produção de traço e uma linguagem profundamente incorporada com semântica operacional padrão.
Suporte a Tipos de Refinamento: Uma extensão do framework para lidar com tipos de refinamento através da recomputação e re-verificação de pré-condições durante a citação.

4. Resultados

Os autores implementaram o SEIO★ em F★, incluindo mais de 900 definições de alto nível.
Eles extraíram com sucesso um exemplo funcional: um wrapper de validação para agentes de IA não verificados que lê um arquivo, chama um agente e verifica o resultado.
O framework foi testado com vários agentes (tanto corretos quanto maliciosos) escritos diretamente na linguagem alvo $\lambda_{io}$ .
A prova verificada por máquina confirma que a extração preserva propriedades de segurança mesmo quando vinculada com código não verificado arbitrário, satisfazendo a RrHP.
O artefato inclui um pipeline para compilar o código $\lambda_{io}$ extraído para OCaml usando o framework Peregrine e Malfunction, permitindo execução prática.

5. Significância e Alegações

O artigo afirma avançar o estado da arte em duas maneiras principais:

Minimização da Validação de Tradução: Ao restringir a validação de tradução à geração de uma derivação de tipagem (citação relacional) e verificar o passo subsequente de geração de sintaxe, o framework reduz a dependência de metaprogramas não verificados em comparação com trabalhos anteriores de extração certificada.
Segurança sobre Correção: Diferente de trabalhos anteriores que focavam em correção funcional, o SEIO★ fornece garantias de compilação segura formais. Ele garante que programas F★ verificados mantenham suas propriedades de segurança (como não interferência e propriedades de traço) mesmo quando vinculados a código arbitrário, não verificado ou adversarial.

Os autores observam que este trabalho vai além do estado da arte atual, que ainda não forneceu garantias de compilação segura tão fortes para a extração de linguagens orientadas a provas. Eles reconhecem limitações, como a atual falta de suporte para funções recursivas gerais e tipos dependentes completos, que são deixadas para trabalhos futuros. O artigo enfatiza que, embora o metaprogram de citação relacional não seja verificado, sua simplicidade e a verificação rigorosa dos passos subsequentes tornam a abordagem geral robusta.