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

Ce que cette vidéo couvre

• Les agents d'IA produisent des preuves candidates; le noyau de Lean vérifie si elles établissent la revendication 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 fiables.
• Prouver le binaire compilé retire le compilateur Rust de la base de confiance pour les propriétés énoncées de ce binaire.
• Les chercheurs rapportent deux réintroductions isolées de bogues 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 contrôlés par YouTube.

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

0:00 Un audit de sécurité par IA ressemble encore à 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'est-ce que Google a prouvé? Et comment empêchent-ils un agent de changer les règles du jeu? Voici la réponse utile. Les modèles écrivent des ébauches de preuves, et Lean vérifie les preuves par rapport à une affirmation approuvée par l'humain concernant le 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 distincte détecte le changement silencieux de question. Nous allons suivre cela jusqu'aux définitions. Nous sommes mardi 10 novembre, et voici The Daily Diff. AlphaProof Code est le cadre de Google pour la rédaction de spécifications logicielles avec une guidance 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 de ligne de commande particulier.

0:45 Google a annoncé les travaux 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 cela capture la sécurité dont les gens se soucient. 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 sa clé de message à rochet. Des analyses formelles ont déjà étudié ces conceptions. L'affirmation de Google relie leurs arguments de sécurité à une implémentation compilée non modifiée d'une bibliothèque de production, 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 de la vérification antérieure. Les détails de l'implémentation incluent les messages désordonnés et les sessions archivées pour les messages différés. Les logiciels réels conservent 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 64 bits Linux. Leurs théorèmes décrivent ce binaire à l'aide d'un modèle d'instruction formel, comblant 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 s'est déplacée, et elle a une adresse. Environ six millions et demi de lignes de preuve vérifiées reposent sur environ vingt-six mille

2:06 lignes de spécification et de sémantique d'instructions fiables. Ce sont des 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 de nœuds.

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 une confidentialité persistante et une sécurité post-compromission selon les modèles énoncés. Ces deux derniers décrivent les limites des dommages causés par une clé volée et la récupération après de nouveaux échanges. Chaque garantie a des conditions sur l'attaquant et la session. Les primitives cryptographiques sont derrière 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. Une preuve idéalise la cryptographie; l'autre raisonne sur les probabilités de succès de l'attaquant. les probabilités de succès de l'attaquant.

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

La spécification peut-elle rejeter un 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 compilation propre prend des heures et une mémoire substantielle. La lecture de l'annonce est considérablement plus facile sur un ordinateur portable. Le modèle matériel et les contrats de confiance nécessitent toujours 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 de sens. Changer 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 réservée que les agents de preuve ne peuvent pas modifier. Ils peuvent proposer des corrections par le biais d'un processus d'amendement distinct. L'affaiblissement de la sécurité est signalé comme un bogue potentiel. La déclaration de succès du prouveur n'a aucune autorité ici.

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

Qu'est-ce qui détecte les objectifs changeants?

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 silencieusement une définition auxiliaire modifie donc la chose à comparer. Une preuve acceptée doit établir la cible approuvée. Cela laisse toujours les humains responsables du choix d'une cible forte et d'hypothèses honnêtes. Pour votre propre flux de travail d'IA, maintenez les critères d'acceptation en dehors des permissions de modification de l'employé

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

Expédierais-je ce flux de travail de preuve?

4:54 J'expédierais ce flux de travail de preuve vérifiée parce que l'affirmation approuvée reste séparée de l'agent qui produit 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 estampillé différemment. Et c'est tout 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