Code et Signal AlphaProof : preuves de sécurité vérifiées du code machine et hypothèses de confiance

Ce que couvre cette vidéo

• Les agents IA produisent des épreuves candidates ; le noyau de Lean vérifie si elles établissent l'affirmation formelle approuvée par l'humain.
• La cible vérifiée est un harnais CLI libsignal compilé particulier, avec une sémantique et des contrats cryptographiques de confiance.
• Prouver le binaire compilé retire le compilateur Rust de la base de confiance pour les propriétés déclarées de ce binaire.
• Les chercheurs rapportent deux réintroductions isolées de bugs précédemment corrigés qui violent leur théorème de sécurité symbolique.
• Le comparateur vérifie le théorème et chaque définition dépendante par rapport à une spécification approuvée protégée ; les amendements passent par un processus d'examen distinct.

Transcription traduite

Traduit de la narration originale en anglais. L'audio et les sous-titres disponibles sont gérés par YouTube.

Qui vérifie une preuve de sécurité IA ?

0:00 Un audit de sécurité par IA ressemble toujours à faire confiance à un chatbot. Le nouveau résultat de Google sur Signal est accompagné de preuves mathématiques qu'un noyau séparé vérifie. Dans cette vidéo, qu'a prouvé Google ? Et comment empêchent-ils un agent de changer les règles du jeu ? Voici la réponse utile. Les modèles écrivent des épreuves candidates, et Lean vérifie les épreuves par rapport à une affirmation approuvée par l'humain concernant un code compilé sélectionné. Les humains possèdent toujours l'affirmation et les hypothèses.

0:21 Vous pouvez vérifier le résultat sans croire le discours de victoire du modèle. Une vérification séparée détecte le fait de changer discrètement la question. Nous allons suivre cela jusqu'aux définitions. Nous sommes le mardi 10 novembre, et voici The Daily Diff. AlphaProof Code est le cadre de Google pour l'écriture de spécifications logicielles avec l'orientation humaine et la génération de preuves vérifiées avec des agents IA. Cette étude cible libsignal, la bibliothèque Rust implémentant le protocole de messagerie de Signal, à l'intérieur d'un programme en ligne de commande particulier.

0:45 Google a annoncé le travail aujourd'hui. Son article indique que cinq chercheurs ont travaillé pendant quatre semaines. Les agents ont écrit les preuves, tandis que les humains ont consacré la majeure partie de leurs efforts aux spécifications. Les exigences ont trouvé un moyen de devenir des réunions encore plus coûteuses. La spécification indique ce que le programme doit faire,

Comment une revendication devient-elle une cible de preuve ?

0:59 ce qu'un attaquant contrôle et les hypothèses dont l'argument a besoin. Les réviseurs demandent si elle capture la sécurité qui intéresse les gens. Une réponse magnifiquement vérifiée à une question faible laisse cette question intacte. L'équipe s'appuie sur des recherches antérieures sur l'établissement de la liaison de Signal et son cliquet de clé de message. Des analyses formelles ont déjà étudié ces conceptions. L'affirmation de Google relie leurs arguments de sécurité à une implémentation compilée d'une bibliothèque de production non modifiée, où la conception doit survivre au contact avec le code réel. Le directeur de la technologie de Signal, Ehren Kret,

1:27 décrit une expansion au-delà des portées plus petites des vérifications antérieures. Les détails d'implémentation incluent des messages désordonnés et des sessions archivées pour les messages retardés. Un vrai logiciel conserve les reçus que votre élégant diagramme a jetés. Les chercheurs compilent la bibliothèque Rust non modifiée avec le compilateur standard

Pourquoi prouver le binaire compilé ?

1:41 dans un exécutable Arm soixante-quatre Linux. Leurs théorèmes décrivent ce binaire en utilisant un modèle d'instruction formel, franchissant l'écart entre le code source et le code machine optimisé. Une erreur de compilateur qui enfreint une propriété énoncée rendrait son théorème faux. Le compilateur quitte donc la base de confiance pour ce binaire. Vous faites toujours confiance au modèle d'instruction et au vérificateur de Lean. La limite de confiance a bougé, et elle a une adresse. Environ six millions et demi de lignes de preuve vérifiée reposent sur environ vingt-six

2:06 mille lignes de spécification et de sémantique d'instructions de confiance. Ce sont des décomptes d'artefacts. Les traiter comme des scores d'intelligence, c'est comme classer les développeurs par la taille de leur dossier de modules node.

Quelles propriétés de sécurité ont survécu à l'écart d'implémentation ?

2:16 Les arguments couvrent la confidentialité et l'authentification des messages, avec la confidentialité persistante et la sécurité post-compromission selon les modèles énoncés. Ces deux derniers décrivent les limites des dommages causés par des clés volées et la récupération après de nouveaux échanges. Chaque garantie est assortie de conditions sur l'attaquant et la session. Les primitives cryptographiques reposent sur des contrats de confiance. La preuve suppose que ces routines se comportent comme spécifié et repose sur des hypothèses de sécurité cryptographiques. L'une des preuves idéalise la cryptographie ; l'autre raisonne sur les probabilités de succès de l'attaquant.

2:42 Les deux ont des restrictions sur les scénarios qu'elles couvrent. Demandez quelle construction, quelle propriété et quelles hypothèses. Ce résultat concerne le harnais de ligne de commande des chercheurs. La messagerie de groupe est un travail futur, et le modèle computationnel exclut l'état multi-appareils. Affirmer que chaque installation de Signal est exempte de bugs sort du théorème. Les chercheurs ont réintroduit deux bugs de Signal précédemment corrigés dans

La spécification peut-elle rejeter du code défectueux ?

3:02 des copies isolées et les ont compilées. Des preuves vérifiées ont montré que ces binaires violaient le théorème de sécurité symbolique. Cela a testé si la spécification pouvait rejeter de réelles implémentations défectueuses. Votre coche verte a besoin d'un test rouge. Google publie les spécifications et les preuves avec des instructions de vérification. Le dépôt indique qu'une construction propre prend des heures et une mémoire substantielle. Lire l'annonce est considérablement plus facile sur l'ordinateur portable. Le modèle matériel et les contrats de confiance nécessitent encore un examen.

3:26 Je n'ai pas reconstruit l'énorme artefact pour cet épisode. Nous rapportons le résultat publié et ses limites. Les personnes extérieures ont un moyen de l'inspecter, ce qui m'importe plus qu'un autre tour de victoire de l'IA. Maintenant le piège.

Une preuve correcte peut-elle répondre à la mauvaise question ?

3:36 Lean peut accepter une preuve correcte d'une affirmation qui ne demande presque rien. Des hypothèses impossibles peuvent rendre un théorème vide. Modifier une définition enfouie sous le théorème principal peut affaiblir l'objectif. Le document conçoit des vérifications contre cela. Le gardien conserve une spécification approuvée mise de côté que les agents de preuve ne peuvent pas modifier. Ils peuvent proposer des corrections via un processus d'amendement distinct. L'affaiblissement de la sécurité est signalé comme un bug potentiel. La déclaration de succès du prouveur n'a aucune autorité ici.

4:00 Les humains arbitrent les changements apportés aux hypothèses de confiance, directement ou par leur politique, et examinent les amendements après chaque campagne. Le jugement des experts reste engagé. L'agent peut demander une affectation différente. Il ne peut pas s'attribuer une note de passage.

Qu'est-ce qui rattrape les objectifs mouvants ?

4:13 Voici la vérification promise. Le comparateur de Lean compare le théorème et chaque définition dont il dépend avec cette copie approuvée protégée. Il vérifie également les axiomes autorisés et rejoue la preuve dans un nouveau noyau. Affaiblir discrètement une définition d'aide modifie donc la chose qui est comparée. Une preuve acceptée doit établir la cible approuvée. Cela laisse toujours les humains responsables de choisir une cible solide et des hypothèses honnêtes. Pour votre propre flux de travail IA, maintenez les critères d'acceptation en dehors des

4:37 permissions de modification du travailleur et examinez les modifications proposées séparément. Le résultat de Google rend cette séparation concrète. Le rédacteur de preuves fait le travail ; la limite de vérification décide si cela compte. Si vous préférez lire cela plutôt que de m'entendre le dire, le "diff" arrive dans votre boîte de réception tous les matins, gratuitement sur the daily diff dot dev, lien ci-dessous. Le verdict d'aujourd'hui est donc EXPÉDIEZ-LE.

Expédièerais-je ce flux de travail de preuve ?

4:54 J'expédierais ce flux de travail de preuve vérifiée car l'affirmation approuvée reste séparée de l'agent produisant la réponse. Je conserverais la portée et les hypothèses attachées à chaque résultat. Abonnez-vous, appuyez sur la cloche et dites-moi dans les commentaires si vous l'auriez approuvé différemment. Et c'est le diff pour aujourd'hui. Je suis Niko d'Axrisi. Fusionnez de manière responsable.

Sources

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