🤖 AI

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

Este artigo apresenta uma correção verificada por máquina de um framework de 2018 para semântica epistêmica de políticas de fluxo de informação, alcançada com o auxílio de um assistente de codificação de IA agêntica, para fornecer uma base robusta e geral para especificar e aplicar requisitos de segurança expressivos.

Autores originais: David A. Naumann

Publicado 2026-08-04

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: David A. Naumann

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

Os Guardiões de Segredos e o Sussurro Digital

Imagine um mundo onde cada programa de computador é uma cidade movimentada, e a informação é a moeda que flui por suas ruas. Nesta cidade, alguns segredos são tão valiosos — como uma chave mestra ou uma senha — que nunca devem sair de um cofre específico. Este é o reino da segurança de fluxo de informação, um ramo da ciência da computação dedicado a garantir que dados sensíveis não vazem acidentalmente (ou maliciosamente) para os olhos errados. Mas a vida nem sempre é preto no branco. Às vezes, um segredo precisa ser compartilhado, mas apenas sob condições muito específicas. Talvez um banco queira dizer a um cliente que sua conta está segura, mas apenas depois de ele responder corretamente a uma pergunta de segurança. Esse equilíbrio delicado é chamado de downgrading (rebaixamento): pegar um segredo de alto nível e diminuir cuidadosamente seu nível de proteção para que ele possa ser visto, mas apenas quando as regras permitirem.

Para dar sentido a essas regras complexas, os cientistas usam um ramo da lógica chamado lógica epistêmica. Pense nisso como a "lógica do conhecimento". Em vez de apenas perguntar "O que aconteceu?", ela pergunta "O que o observador sabe?". Se um hacker estiver vigiando a cidade, o que ele pode deduzir sobre os segredos no cofre com base no tráfego que ele vê? O desafio sempre foi escrever um livro de regras perfeito que diga exatamente quando um segredo pode ser compartilhado sem criar uma brecha. Por anos, pesquisadores tentaram construir uma estrutura matemática para isso, mas as plantas continuavam apresentando rachaduras. Se a matemática estiver errada, a segurança é uma ilusão.

Consertando a Planta com um Assistente Robô

Este artigo conta a história de como um pesquisador, David Naumann, uniu-se a um assistente de codificação de inteligência artificial para consertar uma planta quebrada para essas regras de segurança. A planta original, publicada em 2018, foi uma tentativa inteligente de definir exatamente quando um programa tem permissão para "desclassificar" um segredo. Ela utilizava um conceito chamado anotações relacionais, que são como notas adesivas colocadas no código dizendo: "É aceitável mostrar este segredo se o lançamento da moeda cair em cara". A ideia era que, se duas execuções diferentes do programa concordassem com o lançamento da moeda, elas poderiam concordar em mostrar o segredo.

No entanto, quando o artigo original foi apresentado, o autor percebeu que havia uma falha significativa em sua prova. Era como construir uma ponte que parecia robusta, mas desabava sob um tipo específico de vento. O autor havia esboçado uma correção, mas os detalhes estavam desorganizados e não verificados. Este artigo pega esse esboço e o transforma em uma estrutura sólida e inabalável.

A principal descoberta aqui é uma prova verificada por máquina. O autor não apenas escreveu a matemática no papel; ele a inseriu em um programa de computador chamado Rocq (um assistente de prova) que atua como um tutor de matemática hiperatento. Esse tutor robô verificou cada passo da lógica para garantir que não houvesse lacunas ocultas. O resultado é uma estrutura corrigida que prova: se um programa segue um conjunto específico de regras de "segurança" (que são fáceis de verificar enquanto o programa executa), então ele é matematicamente garantido como seguro de acordo com as complexas regras de "conhecimento".

O artigo descarta explicitamente a ideia de que a prova original de 2018 estava correta como escrita. Ele mostra que a definição anterior de "política de liberação" (o livro de regras para quando segredos podem ser compartilhados) era falha porque não considerava todas as formas pelas quais um programa poderia travar ou divergir. O autor argumenta que você não pode simplesmente confiar na intuição humana nesses cenários complexos de múltiplas execuções; você precisa que a máquina verifique todas as possibilidades.

O Detetive e o Álibi

Para entender como isso funciona, imagine um detetive (o sistema de segurança) tentando descobrir se um suspeito (o programa) está vazando segredos. O detetive tem duas ferramentas: Segurança (Safety) e Segurança (Security).

Security é o objetivo final: "O suspeito não contou nada a ninguém que não devesse saber". Isso é difícil de provar porque você tem que imaginar todos os cenários possíveis em que o suspeito poderia ter estado.
Safety é uma verificação local mais simples: "O suspeito seguiu as regras passo a passo conforme avançava?"

A grande descoberta do artigo é provar que Safety implica Security. Se o programa segue as regras de "Safety" (que são como um checklist de "álibis" para cada etapa), então a garantia complexa de "Security" automaticamente se mantém. É como provar que, se um motorista nunca passa em um sinal vermelho ou excede o limite de velocidade (Safety), ele nunca causará um tipo específico de acidente (Security).

O autor usou um assistente de codificação de IA agêntica (especificamente uma ferramenta chamada Claude Code) para ajudar a escrever o código para a prova em Rocq. Isso não foi apenas um corretor ortográfico; a IA ajudou a traduzir os esboços matemáticos desorganizados em um código rigoroso e até encontrou alguns dos próprios erros do autor. Por exemplo, a IA apontou que uma definição para "divergência" (quando um programa fica preso em um loop infinito) era estrita demais e precisava ser relaxada para fazer a prova funcionar. A IA também tentou "tornar as suposições mais fortes do que o necessário", mas o autor humano a detectou e corrigiu o curso.

O Resultado: Um Livro de Regras Verificado

O artigo conclui que a estrutura corrigida é sólida. A prova verificada por máquina confirma que a ideia original estava no caminho certo, mas os detalhes precisavam de uma revisão importante. A nova estrutura permite uma "política de liberação" que é claramente definida e separada da própria verificação de segurança. Isso significa que os desenvolvedores podem escrever seus códigos com declarações de "assuma" (como "assuma que o usuário está logado") e ter uma garantia matemática de que essas suposições controlam corretamente o que os segredos revelam.

O autor está muito seguro sobre este resultado porque ele foi verificado por máquina. Isso não é uma simulação ou uma sugestão; é uma prova formal de que a lógica se sustenta sob o escrutínio de um computador. Eles admitem, no entanto, que o código é atualmente um pouco desorganizado e precisa de uma limpeza humana para ser verdadeiramente legível, muito parecido com um rascunho brilhante em um guardanapo que precisa ser transcrito para um livro limpo.

No fim, este artigo é uma vitória para a precisão. Ele mostra que, mesmo no mundo abstrato da segurança de computação, onde a lógica pode se tornar incrivelmente emaranhada, podemos usar tanto a intuição humana quanto a assistência da IA para construir uma fundação que é matematicamente inquebrável. Ele transforma um esboço instável em uma fortaleza verificada, garantindo que, quando decidirmos compartilhar um segredo, o façamos exatamente quando pretendemos, e não um momento antes.

Resumo Técnico: Assumindo que Você Sabia: Corrigindo uma Semântica Epistêmica para Políticas de Fluxo Usando IA Agêntica

1. Declaração do Problema

Requisitos de segurança de alto nível relativos ao fluxo de informações, particularmente aqueles que envolvem o rebaixamento seletivo (desclassificação), são notoriamente difíceis de formalizar com precisão. Embora a lógica epistêmica tenha emergido como um arcabouço promissor para definir confidencialidade (o que um observador em um nível de privilégio específico tem permissão para saber), um arcabouço robusto e geral para políticas de fluxo expressivas permaneceu elusivo.

Um trabalho anterior, referido como CN (Naumann et al., CSF 2018), tentou fornecer um arcabouço unificador para modelos de programas reativos. Em CN, as políticas eram expressas via declarações assume dentro do código, enquanto a política de liberação derivada era expressa exclusivamente em termos de fluxos de entrada. No entanto, a formalização em CN continha uma falha significativa em sua prova, anunciada durante a apresentação na conferência. A definição original da política de liberação e a prova subsequente de que a segurança implica segurança foram imprecisas e incorretas. Além disso, adaptações existentes verificadas por máquina (por exemplo, Murray et al. para programas C concorrentes) frequentemente dependem de propriedades fortes como execução em tempo constante, o que trivializa as complexidades de alinhar múltiplas execuções necessárias para o raciocínio epistêmico.

O desafio central é fornecer uma formalização corrigida e verificada por máquina que:

Revise a semântica epistêmica para lidar corretamente com o rebaixamento dependente de estado.
Defina explicitamente a semântica de uma política de liberação derivada de anotações de código.
Prove que uma propriedade orientada ao programa chamada segurança implica a propriedade epistêmica de segurança de informação.

2. Metodologia

O autor emprega uma abordagem de verificação formal usando o assistente de prova Rocq (anteriormente Coq). A metodologia envolve:

Modelo de Programa: Uma linguagem reativa imperativa pequena com manipuladores de entrada para níveis de segurança específicos. Programas consomem fluxos de entrada e produzem saídas.
Anotações: O arcabouço utiliza asserções relacionais (assert) e suposições (assume) para especificar requisitos de fluxo de informação. Essas anotações permitem fluxos condicionais que se desviam da política base de não-interferência.
Semântica Epistêmica: A segurança é definida em termos do conhecimento de um observador. Um observador no nível $\ell$ conhece um conjunto de históricos de entrada possíveis consistentes com suas observações visíveis (entradas e saídas nos níveis $\ell' \sqsubseteq \ell$ ).
Política de Liberação ( $RP_\ell$ ): Definida como o conjunto de listas de entrada que um observador é permitido a aprender, derivada das declarações assume no código. Esta política é interpretada via alinhamentos entre uma pré-execução "maior" (execução real) e pré-execuções "menores" (possíveis execuções com diferentes entradas).
Condição de Segurança: Uma propriedade orientada ao programa definida pela ausência de "falhas" (falhas de asserção, falhas de alinhamento) ou pela presença de "fiats" específicos (fiats de suposição, fiats de divergência) ao comparar uma execução maior contra todas as possíveis execuções menores.
IA Agêntica de Assistência: A formalização foi desenvolvida com o auxílio do Claude Code, um assistente de codificação de IA agêntica. A IA foi guiada para traduzir definições LaTeX em especificações Rocq e auxiliar na construção de provas, embora tenha exigido curadoria humana significativa para corrigir erros lógicos, refinar definições e gerenciar a estratégia de prova.

3. Contribuições Principais

A. Semântica Epistêmica Corrigida

O artigo apresenta uma revisão da formalização da semântica epistêmica para políticas de fluxo. As principais revisões técnicas incluem:

Definição da Política de Liberação: A definição da política de liberação $RP_\ell(gs)$ é corrigida para ser um predicado sobre pré-execuções (prefixos de execução finitos) em vez de apenas traços de eventos observados. Ela é definida via semiconformidade: uma relação entre uma pré-execução maior e pré-execuções menores que as alinha em pontos de anotação específicos.
Segurança Insensível ao Progresso: O arcabouço adota uma definição de segurança insensível ao progresso. Ele utiliza uma noção de conhecimento de progresso ( $k_\ell^\to$ ) para lidar com a divergência, garantindo que as garantias de segurança se mantenham mesmo se o programa divergir, desde que a própria divergência não vaze informações sobre entradas ocultas.
Programas Bem Especificados: O autor introduz "anotações de boilerplate" (suposições no início dos manipuladores e asserções antes das saídas) para simplificar a formalização e garantir que as políticas base sejam codificadas sem alterar o comportamento observável.

B. Segurança Implica Segurança

O resultado teórico central é o Teorema 2: Para todos os níveis $\ell$ , qualquer pré-execução que seja segura para $\ell$ é segura para $\ell$ .

Segurança é definida pela ausência de falhas de asserção/alinhamento e pela presença de fiats válidos (suposição ou divergência) para qualquer lista de entrada alternativa.
A prova demonstra que, se um programa é seguro, o conjunto de entradas que um observador aprende ( $k_\ell$ ) é um subconjunto das entradas permitidas pela política de liberação ( $RP_\ell$ ), interceptado com o conhecimento de progresso.
Este resultado valida a abordagem de impor segurança via verificação relacional de anotações de programa em vez de monitoramento complexo de tempo de execução de todas as execuções possíveis.

C. Verificação Verificada por Máquina

Todo o desenvolvimento, incluindo as definições corrigidas e o teorema principal, foi verificado por máquina em Rocq. Isso confirma que as correções para o artigo CN são fundamentalmente sólidas, ao mesmo tempo em que revela detalhes sutis nas provas que foram perdidos na original escrita por humanos.

D. Experiência com IA Agêntica

O artigo documenta o uso de uma IA agêntica (Claude Code) no processo de formalização. O autor observa que, embora a IA fosse capaz de gerar infraestrutura não trivial e provas rotineiras, ela exigiu supervisão humana para:

Corrigir formalizações falhas de lemas (ex: Lema 3).
Identificar e corrigir lacunas lógicas na definição de "divergence fiat".
Refinar as definições de conhecimento ( $k_\ell$ ) para usar prefixos em vez de igualdade, uma mudança necessária devido a contraexemplos encontrados pela IA.
Impedir que a IA reforçasse excessivamente as suposições ou introduzisse hipóteses de decidibilidade desnecessárias.

4. Resultados

Corretude Formal: A prova verificada por máquina confirma que a condição de segurança revisada implica corretamente a propriedade de segurança epistêmica para o modelo de programa reativo.
Resolução das Falhas de CN: As falhas específicas na prova de CN de 2018 em relação ao alinhamento de execuções e à definição da política de liberação foram resolvidas.
Viabilidade de Formalização Assistida por IA: O estudo demonstra que a IA agêntica pode auxiliar efetivamente na tradução de especificações matemáticas complexas em provas verificadas por máquina, desde que o especialista humano guie ativamente a ferramenta, corrija seus erros lógicos e gerencie a arquitetura geral da prova.

5. Significância e Alegações

O artigo reivindica contribuições modestas, mas significativas:

Arcabouço Unificador: Oferece um arcabouço corrigido e geral para expressar e verificar políticas de fluxo expressivas usando lógica epistêmica e anotações relacionais.
Verificação Prática: Ao mostrar que a segurança (uma propriedade passível de monitoramento em tempo de execução e prova indutiva) implica segurança, o trabalho preenche a lacuna entre especificações de política de alto nível e propriedades de programa aplicáveis.
Confiabilidade da Verificação por Máquina: O trabalho ressalta a necessidade de verificação por máquina, mesmo para desenvolvimentos teóricos em ambientes idealizados, pois ela expõe erros sutis que a revisão humana pode perder.
IA em Métodos Formais: Fornece um estudo de caso concreto do uso de IA agêntica para desenvolvimentos formais substanciais, destacando tanto o potencial para ganhos de eficiência quanto a necessidade crítica de expertise humana para garantir o rigor lógico.

O autor afirma explicitamente que o desenvolvimento de regras de prova composicionais para a condição de segurança permanece um problema em aberto e que o trabalho atual foca na semântica fundamental e no teorema de implicação principal. O artigo é dedicado a David Basin, reconhecendo seu papel pioneiro na formalização verificada por máquina.