Código e Sinal AlphaProof: provas de segurança de código de máquina verificadas e suposições confiáveis

O que este vídeo aborda

• Agentes de IA produzem provas candidatas; o kernel do Lean verifica se elas estabelecem a reivindicação formal aprovada por humanos.
• O alvo verificado é um "harness" CLI libsignal compilado específico, com semântica e contratos criptográficos confiáveis.
• Provar o binário compilado remove o compilador Rust da base confiável para as propriedades declaradas desse binário.
• Os pesquisadores relatam duas reintroduções isoladas de bugs previamente corrigidos que violam seu teorema de segurança simbólico.
• O comparador verifica o teorema e cada definição dependente em relação a uma especificação aprovada protegida; as emendas passam por um processo revisado separado.

Transcrição traduzida

Traduzido da narração original em inglês. Áudio e legendas disponíveis são controlados pelo YouTube.

Quem verifica uma prova de segurança de IA?

0:00 Uma auditoria de segurança de IA ainda soa como confiar em um chatbot. O novo resultado do Google sobre o Signal vem com provas matemáticas que um kernel separado verifica. Neste vídeo, o que o Google provou? E como eles impedem que um agente mude as metas? Aqui está a resposta útil. Os modelos escrevem provas candidatas, e o Lean verifica as provas contra uma reivindicação aprovada por humanos sobre código compilado selecionado. Os humanos ainda possuem a reivindicação e as suposições.

0:21 Você pode verificar o resultado sem acreditar no discurso de vitória do modelo. Uma verificação separada impede que a pergunta seja alterada silenciosamente. Vamos seguir até as definições. É terça-feira, dez de novembro, e este é The Daily Diff. AlphaProof Code é a estrutura do Google para escrever especificações de software com orientação humana e gerar provas verificadas com agentes de IA. Este estudo visa o libsignal, a biblioteca Rust que implementa o protocolo de mensagens do Signal, dentro de um programa de linha de comando específico.

0:45 O Google anunciou o trabalho hoje. Seu artigo diz que cinco pesquisadores trabalharam por quatro semanas. Os agentes escreveram as provas, enquanto os humanos dedicaram a maior parte de seu esforço às especificações. Os requisitos encontraram uma maneira de se tornar reuniões ainda mais caras. A especificação diz o que o programa deve fazer,

Como uma reivindicação se torna um alvo de prova?

0:59 o que um atacante controla e quais suposições o argumento precisa. Os revisores perguntam se ele captura a segurança que as pessoas se importam. Uma resposta lindamente verificada a uma pergunta fraca deixa essa pergunta intacta. A equipe se baseia em pesquisas anteriores sobre o handshake do Signal e seu mecanismo de "ratchet" de chave de mensagem. Análises formais já estudaram esses designs. A reivindicação do Google conecta seus argumentos de segurança a uma biblioteca de produção não modificada implementação compilada, onde o design precisa sobreviver ao contato com código real. O diretor de tecnologia do Signal, Ehren Kret,

1:27 descreve uma expansão além dos escopos menores de verificação anteriores. Detalhes de implementação incluem mensagens fora de ordem e sessões arquivadas para mensagens atrasadas. O software real guarda os recibos que seu diagrama elegante jogou fora. Os pesquisadores compilam a biblioteca Rust não modificada com o compilador padrão

Por que provar o binário compilado?

1:41 em um executável Arm de sessenta e quatro bits para Linux. Seus teoremas descrevem esse binário usando um modelo de instrução formal, atravessando a lacuna entre o código fonte e o código de máquina otimizado. Um erro do compilador que quebra uma propriedade declarada tornaria seu teorema falso. O compilador, portanto, sai da base confiável para este binário. Você ainda confia no modelo de instrução e no verificador do Lean. O limite de confiança mudou e tem um endereço. Cerca de seis milhões e meio de linhas de prova verificada repousam sobre aproximadamente vinte e seis

2:06 mil linhas de especificação e semântica de instrução confiáveis. Estes são contagens de artefatos. Tratá-los como pontuações de inteligência é como classificar desenvolvedores pelo tamanho de sua pasta de módulos node.

Quais propriedades de segurança sobreviveram à lacuna de implementação?

2:16 Os argumentos cobrem confidencialidade e autenticação de mensagens, com sigilo de encaminhamento e segurança pós-comprometimento sob modelos declarados. Os dois últimos descrevem limites para danos por chaves roubadas e recuperação após novas trocas. Cada garantia tem condições sobre o atacante e a sessão. Primitivas criptográficas ficam por trás de contratos confiáveis. A prova assume que essas rotinas se comportam conforme especificado e depende de suposições de segurança criptográficas. Uma prova idealiza a criptografia; a outra raciocina sobre probabilidades de sucesso do atacante.

2:42 Ambos têm restrições sobre os cenários que cobrem. Pergunte qual "build", qual propriedade e quais suposições. Este resultado diz respeito ao "harness" de linha de comando dos pesquisadores. Mensagens em grupo são trabalho futuro, e o modelo computacional exclui o estado de vários dispositivos. Chamar cada instalação do Signal de livre de bugs sai do teorema. Os pesquisadores reintroduziram dois bugs do Signal previamente corrigidos em

A especificação pode rejeitar código quebrado?

3:02 cópias isoladas e os compilaram. Provas verificadas mostraram que esses binários violavam o teorema de segurança simbólico. Isso testou se a especificação poderia rejeitar implementações quebradas reais. Seu visto verde precisa de um teste vermelho. O Google publica as especificações e provas com instruções de verificação. O repositório diz que uma "build" limpa leva horas e memória substancial. Ler o anúncio é consideravelmente mais fácil no laptop. O modelo de hardware e os contratos confiáveis ainda precisam de revisão.

3:26 Não reconstruí o enorme artefato para este episódio. Estamos relatando o resultado publicado e seus limites. Pessoas de fora têm um caminho para inspecioná-lo, o que importa mais para mim do que outra volta da vitória da IA. Agora a armadilha.

Uma prova correta pode responder à pergunta errada?

3:36 O Lean pode aceitar uma prova correta de uma afirmação que pede quase nada. Suposições impossíveis podem tornar um teorema vazio. Alterar uma definição enterrada sob o teorema principal pode enfraquecer o objetivo. O artigo projeta verificações contra isso. O guardião mantém uma especificação aprovada separada para a qual os agentes de prova não podem escrever. Eles podem propor correções por meio de um processo de emenda separado. O enfraquecimento da segurança é escalado como um bug potencial. A declaração de sucesso do provador não tem autoridade aqui.

4:00 Os humanos julgam as mudanças nas suposições confiáveis, diretamente ou por meio de sua política, e revisam as emendas após cada campanha. O julgamento de especialistas permanece em jogo. O agente pode solicitar uma atribuição diferente. Ele não pode se dar uma nota de aprovação.

O que impede que as metas mudem?

4:13 Aqui está a verificação prometida. O comparador do Lean compara o teorema e todas as definições das quais ele depende com essa cópia aprovada protegida. Ele também verifica axiomas permitidos e reproduz a prova em um novo kernel. Enfraquecer silenciosamente uma definição auxiliar, portanto, altera o que está sendo comparado. Uma prova aceita tem que estabelecer o alvo aprovado. Isso ainda deixa os humanos responsáveis por escolher um alvo forte e suposições honestas. Para seu próprio fluxo de trabalho de IA, mantenha os critérios de aceitação fora das

4:37 permissões de edição do trabalhador e revise as alterações propostas separadamente. O resultado do Google torna essa separação concreta. O escritor da prova faz o trabalho; o limite de verificação decide se isso conta. Se você preferir ler isso a me ouvir dizer, o "diff" chega à sua caixa de entrada todas as manhãs, gratuitamente em the daily diff dot dev, link abaixo. Então o veredito de hoje é SHIP IT.

Eu usaria este fluxo de trabalho de prova?

4:54 Eu enviaria este fluxo de trabalho de prova verificada porque a reivindicação aprovada permanece separada do agente que produz a resposta. Eu manteria o escopo e as suposições anexados a cada resultado. Inscreva-se, ative o sino e me diga nos comentários se você teria carimbado diferentemente. E esse é o "diff" de hoje. Sou Niko da Axrisi. Mesclar com responsabilidade.

Fontes

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub