Codi i senyal AlphaProof: proves de seguretat de codi màquina verificades i suposicions de confiança

Què cobreix aquest vídeo

• Els agents d'IA produeixen proves candidates; el nucli de Lean verifica si estableixen la afirmació formal aprovada per humans.
• L'objectiu verificat és una eina CLI de libsignal compilada particular, amb semàntiques i contractes criptogràfics de confiança.
• Provar el binari compilat elimina el compilador de Rust de la base de confiança per a les propietats declarades d'aquest binari.
• Els investigadors informen de dues reintroduccions aïllades de bugs prèviament corregits que violen el seu teorema de seguretat simbòlic.
• El comparador verifica el teorema i totes les definicions dependents respecte a una especificació aprovada protegida; les esmenes passen per un procés de revisió separat.

Transcripció traduïda

Traduït de la narració original en anglès. L'àudio i els subtítols disponibles estan controlats per YouTube.

Qui verifica una prova de seguretat d'IA?

0:00 Una auditoria de seguretat d'IA encara sona com confiar en un chatbot. El nou resultat de Signal de Google inclou proves matemàtiques que un nucli separat verifica. En aquest vídeo, què va provar Google? I com eviten que un agent "mogui els marcadors"? Aquí teniu la resposta útil. Els models escriuen proves candidates, i Lean verifica les proves respecte a una afirmació aprovada per humans sobre codi compilat seleccionat. Els humans encara són propietaris de l'afirmació i les suposicions.

0:21 Podeu comprovar el resultat sense creure el discurs de victòria del model. Una comprovació separada detecta el canvi silenciós de la pregunta. Seguirem fins a les definicions. És dimarts, deu de novembre, i això és The Daily Diff. AlphaProof Code és el framework de Google per escriure especificacions de programari amb guia humana i generar proves verificades amb agents d'IA. Aquest estudi s'enfoca en libsignal, la biblioteca de Rust que implementa el protocol de missatgeria de Signal, dins d'un programa de línia d'ordres particular.

0:45 Google va anunciar el treball avui. El seu article diu que cinc investigadors van treballar durant quatre setmanes. Els agents van escriure les proves, mentre que els humans van dedicar la major part del seu esforç a les especificacions. Els requisits han trobat una manera de convertir-se en reunions encara més cares. L'especificació diu què ha de fer el programa,

Com esdevé una afirmació un objectiu de prova?

0:59 què controla un atacant i quines suposicions necessita l'argument. Els revisors pregunten si capta la seguretat que interessa a la gent. Una resposta bellament verificada a una pregunta feble deixa aquesta pregunta intacta. L'equip es basa en investigacions anteriors sobre l'apretada de mans de Signal i el seu "message-key ratchet". Les anàlisis formals ja havien estudiat aquests dissenys. L'afirmació de Google connecta els seus arguments de seguretat amb una implementació compilada d'una biblioteca de producció no modificada, on el disseny ha de sobreviure al contacte amb el codi real. El director de tecnologia de Signal, Ehren Kret, descriu una expansió més enllà dels abasts més petits de la verificació anterior.

1:27 Els detalls d'implementació inclouen missatges fora d'ordre i sessions arxivades per a missatges endarrerits. El programari real guarda els rebuts que el vostre elegant diagrama va llençar. Els investigadors compilen la biblioteca de Rust no modificada amb el compilador estàndard en un executable Arm de seixanta-quatre bits de Linux.

Per què provar el binari compilat?

1:41 Els seus teoremes descriuen aquest binari utilitzant un model d'instruccions formal, arribant a través de la bretxa entre el codi font i el codi màquina optimitzat. Un error del compilador que trenqués una propietat declarada faria que el seu teorema fos fals. Per tant, el compilador abandona la base de confiança per a aquest binari. Encara confieu en el model d'instruccions i en el verificador de Lean. La frontera de confiança s'ha mogut i té una adreça. Al voltant de sis milions i mig de línies de prova verificada es basen en aproximadament vint-i-sis mil línies de especificació i semàntica d'instruccions de confiança.

2:06 Aquests són recomptes d'artefactes. Tractar-los com a puntuacions d'intel·ligència és com classificar els desenvolupadors per la mida de la seva carpeta de mòduls node. Els arguments cobreixen la confidencialitat i l'autenticació dels missatges,

Quines propietats de seguretat van sobreviure a la bretxa d'implementació?

2:16 amb secret d'avançament i seguretat post-compromís sota models declarats. Aquests dos últims descriuen límits al dany de clau robada i la recuperació després de nous intercanvis. Cada garantia té condicions sobre l'atacant i la sessió. Els primitius criptogràfics es troben darrere de contractes de confiança. La prova assumeix que aquestes rutines es comporten segons l'especificat i es basa en suposicions de seguretat criptogràfica. Una prova idealitza la criptografia; l'altra raona sobre les probabilitats d'èxit de l'atacant. Ambdós tenen restriccions sobre els escenaris que cobreixen. Pregunta quina compilació, quina propietat i quines suposicions.

2:42 Aquest resultat es refereix a l'eina de línia d'ordres dels investigadors. La missatgeria de grup és un treball futur, i el model computacional exclou l'estat multidispositiu. Afirmar que cada instal·lació de Signal no té errors surt fora del teorema. Els investigadors van reintroduir dos errors de Signal prèviament corregits en còpies aïllades i les van compilar. Les proves verificades van demostrar que aquests binaris violaven el teorema de seguretat simbòlic.

Pot l'especificació rebutjar codi trencat?

3:02 Això va provar si l'especificació podia rebutjar implementacions trencades reals. El vostre vist verd necessita una prova vermella. Google publica les especificacions i les proves amb instruccions de verificació. El repositori diu que una compilació neta triga hores i una memòria substancial. Llegir l'anunci és considerablement més fàcil a l'ordinador portàtil. El model de hardware i els contractes de confiança encara necessiten revisió. No he reconstruït l'enorme artefacte per a aquest episodi. Estem informant del resultat publicat i els seus límits.

3:26 Els forasters tenen un camí per inspeccionar-lo, cosa que m'importa més que una altra volta de victòria de la IA. Ara la trampa. Lean pot acceptar una prova correcta d'una declaració que gairebé no demana res. Les suposicions impossibles poden fer que un teorema sigui buit.

Pot una prova correcta respondre a la pregunta equivocada?

3:36 Canviar una definició enterrada sota el teorema principal pot afeblir l'objectiu. El document dissenya comprovacions contra això. El guardià manté una especificació aprovada reservada a la qual els agents de prova no poden escriure. Poden proposar correccions a través d'un procés d'esmena separat. L'afebliment de la seguretat s'escala com un possible error. La declaració d'èxit del provador no té autoritat aquí. Els humans jutgen els canvis a les suposicions de confiança, directament o a través de la seva política, i revisen les esmenes després de cada campanya.

4:00 El judici expert es manté responsable. L'agent pot sol·licitar una assignació diferent. No es pot atorgar una qualificació d'aprovat. Aquí teniu la comprovació promesa. El comparador de Lean compara el teorema i totes les definicions de les quals depèn amb

Què atrapa els "moving goalposts"?

4:13 aquella còpia aprovada protegida. També verifica els axiomes permesos i reprodueix la prova en un nucli nou. Afeblir silenciosament una definició auxiliar, per tant, canvia allò que s'està comparant. Una prova acceptada ha d'establir l'objectiu aprovat. Això encara deixa els humans responsables de triar un objectiu sòlid i suposicions honestes. Per al vostre propi flux de treball d'IA, manteniu els criteris d'acceptació fora dels permisos d'edició del treballador i reviseu els canvis proposats per separat. El resultat de Google fa que aquesta separació sigui concreta.

4:37 L'escriptor de la prova fa la feina; el límit de verificació decideix si compta. Si preferiu llegir això que sentir-me dir-ho, la "diff" arriba a la vostra safata d'entrada cada matí, gratuïta a thedaily-diff.dev, enllaç a sota. Així que el veredicte d'avui és "SHIP IT". Enviaria aquest flux de treball de prova verificada perquè la reclamació aprovada es manté separada de l'agent que produeix la resposta.

Enviaria aquest flux de treball de prova?

4:54 Mantindria l'abast i les suposicions adjuntes a cada resultat. Subscriviu-vos, cliqueu la campana i digueu-me als comentaris si l'hauríeu segellat de manera diferent. I aquesta és la diferència d'avui. Sóc en Niko d'Axrisi. Fusiona amb responsabilitat. Fusiona amb responsabilitat. Fusiona amb responsabilitat.

Fonts

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