Resumo Técnico: Pureza Certificada para Executores de Fluxos de Trabalho Cognitivos

1. O Problema: A Lacuna de Pureza em Fluxos de Trabalho Cognitivos

Sistemas de fluxo de trabalho cognitivo (orquestrando inferência de IA, uso de ferramentas e raciocínio) operam cada vez mais em domínios de alto risco. Trabalhos anteriores (McCann [2026e]) estabeleceram uma arquitetura de governança de três camadas que garante Completude da Governança, Completude da Proveniência e a Impossibilidade de Efeitos Não Governados. No entanto, esses teoremas de segurança baseavam-se em uma premissa crítica: a Restrição de Módulo Puro, que exige que os módulos executores não possam realizar efeitos de E/S e apenas retornem diretivas declarativas.

Na implementação anterior, essa restrição era imposta por meio de análise estática do gráfico de importação de módulos na máquina virtual BEAM (Erlang/OTP). Embora mais forte que a governança baseada em convenções, esse mecanismo é insuficiente contra contornamentos adversariais. Os recursos dinâmicos do BEAM permitem cinco classes distintas de contornamento que a análise estática não pode prevenir de forma confiável:

1. Dispersão Dinâmica: Uso de :erlang.apply/3 para invocar funções arbitrárias sem importações estáticas.
2. Avaliação de Código: Uso de Code.eval_string/1 para executar código arbitrário em tempo de execução.
3. Funções Implementadas Nativamente (NIFs): Carregamento de bibliotecas compartilhadas com acesso irrestrito ao sistema.
4. Portas: Inicialização de processos externos via :erlang.open_port/2.
5. Carregamento Dinâmico de Módulos: Carregamento de bytecode arbitrário em tempo de execução via :code.load_binary/3.

Devido ao Teorema de Rice, nenhuma análise estática pode decidir a propriedade semântica não trivial de "nenhum efeito de E/S" para todos os programas possíveis. Uma superaproximação sonora rejeitaria a maioria dos códigos idiomáticos legítimos em Elixir. Isso cria uma lacuna de pureza: o modelo formal assume pureza, mas o mecanismo de imposição (análise estática) não pode garantir estruturalmente essa pureza contra um adversário determinado.

2. Metodologia: Da Detecção à Prevenção Estrutural

Este artigo propõe uma Arquitetura de Pureza Certificada que converte a restrição de módulo puro de uma convenção imposta por análise em uma fronteira de capacidade estrutural imposta pelo ambiente de execução. A metodologia baseia-se em quatro mecanismos centrais:

A. Alvo de Compilação Restrito (WebAssembly)

Os executores são compilados para um alvo WebAssembly (WASM) restrito. O modelo de capacidades do WASM é aproveitado para eliminar estruturalmente todas as cinco classes de contornamento do BEAM:

• Sem Dispersão Dinâmica: O WASM carece de instruções para resolver chamadas de função por nomes de strings/átomos em tempo de execução; as chamadas são restritas a índices estáticos em uma tabela de funções.
• Sem Avaliação de Código: O WASM executa bytecode pré-compilado; não há mecanismo para gerar ou carregar novo código em tempo de execução.
• Sem NIFs/Portas: Módulos WASM são executados em uma VM em sandbox sem acesso a sistemas de arquivos do host, bibliotecas compartilhadas ou inicialização de processos.
• Sem Carregamento Dinâmico: A instanciação de módulos é controlada inteiramente pelo host; módulos não podem carregar outros módulos.

B. A Lista Branca de Funções do Host ($W$)

O módulo WASM pode invocar apenas funções explicitamente declaradas em sua seção de importação. Essas importações são restritas a uma Lista Branca ($W$) finita e enumerada:

• $W_{data}$: Operações de dados puros (gerenciamento de memória, manipulação de strings, aritmética, serialização JSON, leituras de contexto).
• $W_{dir}$: Construtores de diretivas (funções que constroem estruturas de dados representando efeitos pretendidos, como directive_http_request, mas que não os executam).
• Exclusão: Importações do WASI (WebAssembly System Interface), que concedem capacidades de efeito, são explicitamente excluídas.

C. Certificados de Pureza

Um Certificado de Pureza é um artefato de prova criptográfica que vincula um binário de executor à sua classificação de pureza.

• Estrutura: Contém o hash SHA-256 do binário do executor, o hash da prova de pureza (lista de importações + classificação) e uma assinatura Ed25519 sobre esses hashes.
• Integridade: Devido à resistência a colisões do SHA-256 e à inforgeabilidade do Ed25519, um certificado não pode ser transferido para um artefato modificado.

D. Portão de Verificação em Tempo de Execução

Antes de um executor entrar no pipeline de governança, um Portão de Verificação realiza:

1. Verificação de Assinatura: Valida a assinatura Ed25519.
2. Vinculação de Artefato: Confirma que o hash do binário corresponde ao certificado.
3. Derivação Independente de Prova: Analisa a seção de importação do binário WASM de novo e verifica se corresponde à prova de pureza reivindicada contra a lista branca atual.
4. Validação de Classificação: Garante que todas as importações sejam classificadas como puras.

Apenas executores que passam por esse portão são instanciados. Esse portão atua como uma pré-condição estrutural, garantindo que nenhum executor sem um certificado de pureza válido possa ser executado.

3. Contribuições Principais

1. Modelo de Ameaça Formal: Uma caracterização rigorosa das cinco classes de contornamento do BEAM e dos limites teóricos da análise estática (Teorema de Rice) neste contexto.
2. Pureza Estrutural por Construção: Uma prova (Teorema 4.5) de que a compilação para o alvo WASM restrito satisfaz a restrição de módulo puro por construção, independentemente do conteúdo do código do executor.
3. Eliminação de Contornamentos: Provas formais (Teorema 5.5) de que cada uma das cinco classes de contornamento do BEAM é estruturalmente impossível no ambiente WASM restrito.
4. Atestação Criptográfica: Um esquema para Certificados de Pureza e Registros de Atestação Remota que permite a verificação portátil e interorganizacional da pureza do executor sem acesso ao código-fonte.
5. Definição da Base de Computação Confiável (TCB): Uma definição explícita dos cinco componentes necessários para a garantia (runtime WASM, funções do host, lista branca, portão de verificação, interpretador de diretivas), reduzindo a superfície de confiança do código do executor ilimitado para um conjunto delimitado e auditável.
6. Níveis de Confiança Graduais: Uma arquitetura de implementação que suporta três níveis (Pureza Verificada, Análise Estática, Experimental) para permitir adoção incremental.

4. Resultados e Avaliação

A arquitetura foi avaliada em quatro executores implementados (baseados em Rust, compilados para WASM) executando em um processador Apple série M com o backend JIT Wasmtime.

• Latência de Verificação: O portão de verificação leva 39–42 µs (mediana) para executores de produção. Com cache baseado em hash, o custo amortizado aproxima-se de zero para invocações repetidas.
• Sobrecarga em Tempo de Execução: O ciclo completo do plano (instanciação, execução, desserialização) é concluído em 256–398 µs. Isso representa uma sobrecarga de <0,4% em uma solicitação HTTP de 100 ms e <0,05% em uma chamada típica de LLM de 800 ms.
• Determinismo: Zero divergências foram observadas em 40 invocações repetidas com entradas idênticas, confirmando a natureza determinística do ambiente de execução WASM.
• Tamanho do Certificado: Os certificados são compactos (~1,3 KB), bem dentro dos orçamentos de largura de banda.
• Correção: Todos os executores produziram as formas de diretiva esperadas, e o sistema manteve saídas idênticas em bytes entre execuções.

5. Significado e Reivindicações

O artigo reivindica uma mudança fundamental no status epistemológico das garantias de governança:

• Da Detecção à Prevenção: Abordagens anteriores baseavam-se em detectar padrões de contornamento conhecidos por meio de análise estática. Esta arquitetura previne o contornamento tornando as capacidades de produção de efeitos estruturalmente ausentes.
• Fortalecimento de Teoremas Existentes: Os teoremas de segurança de McCann [2026e] (Completude da Governança, Completude da Proveniência, Sem Efeitos Não Governados) permanecem formalmente idênticos. No entanto, sua premissa fundamental é descarregada mecanicamente em vez de assumida. A garantia agora repousa nas propriedades matemáticas do modelo de capacidades do WASM e em primitivas criptográficas (SHA-256, Ed25519) em vez das limitações de um analisador estático.
• Confiança Portátil: Ao converter provas locais de pureza em registros de atestação portáteis, a arquitetura permite a composição de governança interorganizacional, permitindo que a Organização A verifique criptograficamente a pureza dos executores da Organização B sem revisão de código-fonte.

O artigo observa explicitamente que isso não é uma prova mecanizada no sentido de Rocq ou Lean (o que é reservado para a lógica de governança subjacente em artigos companheiros), mas uma garantia estrutural verificada em tempo de execução. A contribuição é a redução da superfície de confiança de "todo o código do executor" para uma pequena Base de Computação Confiável explicitamente definida.