💻 computer science

Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

Este artigo introduz o Elton, uma lógica de separação de ordem superior que apresenta novos "recursos de urna" (urn resources) e mecanismos de amostragem atrasada para verificar formalmente limites de erro e propriedades de segurança em programas probabilísticos contendo código adversarial desconhecido, com todas as provas mecanizadas no assistente de prova Rocq.

Autores originais: Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Publicado 2026-07-16

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

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

O Detetive Digital e o Mistério do Alvo Móvel

Imagine que você está tentando provar que um código secreto é inquebrável. No mundo da segurança de computadores, você não está apenas testando o código contra uma fechadura estática; você está testando-o contra um hacker invisível e astuto que pode tentar qualquer coisa que desejar. Este campo é chamado de verificação formal, onde matemáticos e cientistas da computação usam lógica rigorosa para provar que um software se comporta exatamente como pretendido, mesmo quando atacado pelo pior inimigo possível.

Para fazer isso, eles frequentemente lidam com programas probabilísticos. Pense nestes não como calculadoras padrão que sempre dão a mesma resposta, mas como lançadores de dados digitais. Eles fazem escolhas aleatórias — como jogar uma moeda ou escolher um número de um chapéu — para fazer coisas como criptografar mensagens ou treinar inteligência artificial. A parte complicada é que, quando você mistura esses lançamentos de dados aleatórios com funções de ordem superior (que são como "funções que podem receber outras funções como ingredientes") e código desconhecido (a receita secreta do hacker), a matemática torna-se incrivelmente complexa. Você não pode apenas olhar para um possível resultado; você tem que raciocinar sobre toda a distribuição de possíveis resultados para garantir que o hacker não possa trapacear as probabilidades.

O Problema: O "Jogo de Adivinhação" Que Quebra a Lógica

Por anos, pesquisadores possuíam ferramentas para verificar esses programas, mas eles bateram em um muro quando a ordem dos eventos se tornava complicada. Imagine um jogo onde um computador escolhe um número secreto e, depois, um hacker tenta adivinhar esse número. Se o computador escolhe o número antes do hacker fazer seu movimento, é fácil provar que o hacker não pode vencer. Mas e se o hacker fizer seu movimento primeiro, e então o computador escolher o número baseado no que o hacker fez?

No mundo real, isso é como um mágico que pede para você escolher uma carta e, depois, embaralha o baralho para garantir que essa carta esteja no fundo. As ferramentas de lógica padrão tinham dificuldade com isso. Elas podiam lidar com a aleatoriedade ou com a interação complexa com o hacker, mas não com ambos ao mesmo tempo. Elas não conseguiam dizer: "Espere, o número secreto ainda é um mistério até o final, então vamos fingir que é uma nuvem de possibilidades que só esclareceremos depois que o hacker terminar". Sem essa habilidade, provar que um sistema de segurança é seguro contra um hacker inteligente e adaptativo era muitas vezes imposs empossível.

A Solução: Elton e os Urnas Mágicas

Entra em cena o Elton, um novo conjunto de ferramentas lógicas criado pelos pesquisadores Li, Aguirre, Haselwarter, Tassarotti e Birkedal. Eles construíram um sistema que trata números aleatórios não como resultados imediatos, mas como amostragens atrasadas.

Pense em um gerador de números aleatórios padrão como uma máquina de vendas que cospe um refrigerante no momento em que você pressiona um botão. O Elton muda o jogo: quando você pressiona o botão, em vez de um refrigerante, você recebe uma urna selada e mágica. Você ainda não sabe o que há dentro. Você pode carregar essa urna, passá-la para o hacker e até fazer cálculos sobre a ideia do refrigerante sem nunca abrir a urna. A urna representa uma "nuvem" de todos os refrigerantes que poderiam estar dentro, com chances iguais para cada um.

É aqui que a principal inovação do artigo brilha: Recursos de Urna (Urn Resources).
Na lógica do Elton, essas urnas são objetos especiais sobre os quais o computador pode raciocinar. Os pesquisadores provaram que você pode realizar cálculos nessas "nuvens" de possibilidades. Por exemplo, se você tem uma urna contendo números de 0 a 10, e adiciona 1 a ela, a lógica sabe que agora você tem uma urna contendo de 1 a 11. Você pode até passar essa "urna matemática" para o hacker. O hacker pode tentar adivinhar o que há dentro, mas contanto que ele não espie, a urna permanece uma nuvem de possibilidades.

A mágica acontece no final do programa. Uma vez que o hacker terminou seus movimentos, a lógica permite que você resolva a urna. Isso é como finalmente abrir a caixa mágica para ver qual refrigerante realmente está dentro. Como os pesquisadores construíram um sistema especial de "amostragem atrasada", eles podem provar que abrir a urna no final fornece exatamente os mesmos resultados estatísticos como se você a tivesse aberto imediatamente. Isso permite que eles atrasem a decisão de "qual é o número aleatório?" até depois que o hacker fez todos os seus movimentos, tornando possível provar que o hacker não poderia ter manipulado o jogo.

O Que Eles Provaram e O Que Não Provaram

Os autores não apenas sugeriram que isso poderia funcionar; eles provaram. Eles construíram o Elton dentro de um assistente de prova poderoso chamado Rocq (anteriormente Coq), que atua como um professor de matemática super rigoroso que verifica cada passo da lógica para garantir que não haja erros.

Eles usaram o Elton para resolver vários enigmas de segurança complicados que as ferramentas anteriores não consegravam lidar:

O Lançamento Complicado: Eles provaram que, mesmo que um hacker tente manipular um lançamento de moeda chamando funções de ida e volta, a moeda permanece perfeitamente justa (50/50), desde que o hacker não consiga ver a moeda antes de começar.
A Adivinhação Interativa: Eles mostraram que, mesmo que um hacker tenha várias chances de adivinhar um número secreto, as chances de ele vencer permanecem baixas, mesmo que o hacker decida seu próximo palpite com base nos anteriores.
Funções de Hash: Eles verificaram que uma "oráculo aleatório" (uma função de hash perfeita) permanece segura contra um atacante que a consulta muitas vezes, provando que encontrar uma "colisão" (dois inputs que dão o mesmo output) é incrivelmente improvável.
Logaritmos Discretos: Eles forneceram a primeira prova formal para a segurança do problema do logaritmo discreto contra atacantes interativos no "modelo de grupo genérico", uma forma padrão de testar a força criptográfica.

No entanto, o artigo é honesto sobre seus limites. A versão atual do Elton é projetada especificamente para distribuições uniformes — onde cada resultado na urna é igualmente provável, como um dado justo. Os autores afirmam explicitamente que ainda não podem lidar com urnas "viesadas" (como uma moeda viciada) ou possibilidades infinitas sem fazer mudanças significativas em sua matemática. Eles também observam que, embora seu método seja poderoso, é complexo e "convoluto", o que significa que pode ser difícil escalá-lo para todo tipo de programa aleatório no futuro.

A Conclusão

O Elton é um avanço em um nicho específico da ciência da computação que lida com programas probabilísticos adversariais. Ele não diz apenas "este código provavelmente é seguro"; ele fornece uma prova rigorosa, verificada por máquina, de que o código é seguro mesmo quando um hacker inteligente e adaptativo tenta manipular o sistema. Ao introduzir o conceito de "amostragem atrasada" e "recursos de urna", os autores encontraram uma maneira de manter os números aleatórios em um "estado suspenso" até o final, permitindo que superassem as armadilhas lógicas que anteriormente impediam os pesquisadores de provar essas garantias de segurança. É um novo par de óculos que nos permite enxergar a justiça oculta em um mundo caótico e aleatório.

Resumo Técnico: Elton: Recursos de Urna para Raciocínio sobre Programas Probabilísticos Adversariais

Enunciado do Problema
A verificação formal de programas probabilísticos é crítica para aplicações em algoritmos randomized, aprendizado de máquina, privacidade diferencial e segurança criptográfica. Um desafio específico surge na segurança criptográfica, onde se deve estabelecer propriedades que se mantêm na presença de código adversário arbitrário e desconhecido. Embora lógicas de separação de ordem superior tenham tido sucesso ao modelar interações adversárias em ambientes não probabilísticos, estender isso para programas probabilísticos é difícil. A dificuldade central reside em raciocinar sobre a combinação de escolha probabilística, funções de ordem superior e estado local quando o comportamento do adversário é desconhecido.

As técnicas de verificação existentes enfrentam um trilema:

Lógicas Distribucionais: Permitem que predicados descrevam distribuições de estados (úteis para invariantes como "o valor é uniformemente distribuído"), mas frequentemente carecem das características expressivas (funções de ordem superior, referências gerais) necessárias para modelar interações adversárias complexas.
Lógicas Baseadas em Levantamento (Lifting-Based): Mantêm predicados padrão baseados em estado e os elevam para distribuições (mais fáceis de estender com recursos de ordem superior), mas têm dificuldade em expressar invariantes distribucionais, como os necessários para provar que um adversário não pode enviesar um bit aleatório.
Raciocínio Adversarial: As abordagens existentes frequentemente falham em lidar com a combinação simultânea de código desconhecido, estado de ordem superior e invariantes distribucionais. Por exemplo, as "variáveis de profecia" (prophecy variables) ou "fitas de pré-amostragem" (presampling tapes) padrão (usadas em lógicas como o Clutch) não podem prever sonoramente o resultado do código de um adversário desconhecido, nem podem facilmente lidar com casos em que a ordem da amostragem aleatória e das chamadas adversárias é invertida.

Metodologia
Os autores apresentam o Elton, uma lógica de separação de ordem superior projetada para raciocinar sobre a segurança robusta de programas probabilísticos na presença de código adversário desconhecido. O Elton adota uma abordagem "mista", combinando os benefícios estruturais de lógicas baseadas em levantamento (construídas sobre o framework Iris) com mecanismos inovadores para capturar propriedades distribucionais.

A metodologia baseia-se em duas extensões primárias:

Amostragem Adiada (Semântica Operacional):
O Elton introduz uma variante da linguagem (RandML) que apresenta uma primitiva drand. Diferente da amostragem aleatória padrão (rand), o drand não resolve imediatamente para um valor. Em vez disso, ele cria uma "urna" simbólica (um conjunto de valores possíveis) e retorna um "rótulo de urna". Computações envolvendo esses rótulos produzem "valores atrasados" (expressões simbólicas). Isso permite que a lógica adie a resolução da aleatoriedade até que o adversário tenha interagido com o sistema. A semântica operacional garante que essas computações atrasadas possam ser sonoramente apagadas (erased) de volta para a semântica de chamada por valor probabilística padrão.
Recursos de Urna (Facilidades Lógicas):
No nível da lógica, o Elton introduz recursos de urna (denotados por $\iota \sim s$ ), que afirmam que uma variável de amostragem atrasada $\iota$ é uniformemente distribuída sobre um conjunto $s$ . Isso permite que a lógica raciocine sobre a distribuição de estados sem abandonar o poder expressivo da lógica de separação.
O processo de prova para recursos de urna segue um ciclo de vida de três fases:
- Criação: A primitiva drand cria um recurso de urna.
- Resolução: A lógica pode "resolver" um recurso de urna, dividindo-o em subconjuntos (por exemplo, evitando um valor específico adivinhado por um adversário) enquanto distribui "créditos de erro" (limites probabilísticos) adequadamente. Isso é governado por regras como ht-resolve-partial.
- Promoção: Uma vez que a interação do adversário é concluída e as propriedades distribucionais são estabelecidas, os "valores atrasados" são promovidos a valores concretos usando o predicado de promoção de atualização ( $v \mapsto [R] w$ ), que afirma equivalência semântica sob os recursos de urna atuais.

O Elton herda o mecanismo de créditos de erro de seu predecessor, o Eris, para limitar as probabilidades de erro, e utiliza relações lógicas para derivar especificações para adversários de ordem superior bem tipados baseando-se apenas em seus tipos.

Principais Contribuições
O artigo reivindica as seguintes contribuições:

Primeira Lógica de Separação de Ordem Superior Probabilística: O Elton é a primeira lógica capaz de lidar com a combinação de código adversário desconhecido, estado local de ordem superior e invariantes distribucionais simultaneamente.
Semântica Operacional Inovadora: Uma semântica que suporta amostragens atrasadas e execução simbólica de valores suspensos, provada como sonora via apagamento para semânticas de chamada por valor probabilística padrão.
Recursos de Urna: Um novo recurso de lógica de separação para raciocinar sobre distribuições de estados decorrentes de amostragens atrasadas.
Sonoridade e Adequação: Uma prova de sonoridade formal conectando a semântica de amostragem atrasada às semânticas padrão, garantindo que provar propriedades na versão atrasada implica limites de erro na versão padrão.
Estudos de Caso Mecanizados: Todos os resultados foram mecanizados no assistente de provas Rocq (utilizando o framework Iris e a biblioteca Coquelicot). O artigo demonstra a expressividade da lógica através de vários exemplos complexos:
- Adivinhação Interativa (Interactive Guessing): Provando limites de erro para um adversário com múltiplas tentativas de adivinhar um segredo, onde o número de tentativas é desconhecido.
- Flip Complicado (Complicated Flip): Verificando que um programa retorna um bit uniformemente distribuído mesmo quando um adversário pode manipular o estado via closures, desde que não possa ler o estado diretamente.
- Resistência de Pré-imagem: Formalizando a resistência de pré-imagem do modelo de hash de oráculo aleatório contra um adversário interativo.
- Desvinculabilidade (Unlinkability): Verificando a propriedade de desvinculabilidade do protocolo Basic Hash.
- Logaritmo Discreto: Fornecendo a primeira prova mecanizada formal de limites de erro para o problema do logaritmo discreto no modelo de grupo genérico contra algoritmos genéricos interativos.

Resultos
Os autores demonstram que o Elton pode provar limites de erro para uma ampla gama de exemplos de segurança que estavam fora do alcance de técnicas existentes. Especificamente:

O Elton lida com sucesso com cenários onde a ordem da amostragem aleatória e das chamadas adversárias é invertida (ex: guess2), um caso onde as regras padrão do Eris falham.
Ele verifica propriedades envolvendo estado local alocado dinamicamente e raciocínio probabilístico complexo, como a desvinculabilidade do protocolo Basic Hash.
Fornece uma prova formal para o problema do logaritmo discreto no modelo de grupo genérico, correspondendo aos limites de erro estabelecidos por Shoup, mas dentro de uma semântica operacional precisa para programas interativos.

Significância
O artigo posiciona o Elton como um avanço significativo na verificação formal de protocolos criptográficos. Ao unir a lacuna entre lógicas de levantamento (que lidam com recursos complexos de linguagem) e lógicas distribucionais (que lidam com invariantes probabilísticas), o Elton permite a verificação de propriedades de segurança na presença de adversários desconhecidos sem recorrer a modelos simplificados ou restrições sintáticas ad-hoc. Os autores observam que, embora a abordagem seja atualmente limitada a distribuições uniformes e exija modificações significativas para suportar distribuições mais complexas (ex: não uniformes ou infinitas), ela estabelece uma fundação promissora para expressar propriedades distribucionais dentro de um framework de lógica de levantamento. O trabalho é totalmente mecanizado, proporcionando um alto grau de confiança nas garantias de segurança derivadas.