AlphaProof Code und Signal: überprüfte maschinencode-Sicherheitsnachweise und vertrauenswürdige Annahmen

Was dieses Video behandelt

• KI-Agenten erstellen Kandidatenbeweise; Leans Kernel überprüft, ob sie den von Menschen genehmigten formalen Anspruch belegen.
• Das verifizierte Ziel ist ein bestimmtes kompiliertes libsignal CLI-Harness mit vertrauenswürdiger Semantik und kryptografischen Verträgen.
• Der Beweis des kompilierten Binärprogramms entfernt den Rust-Compiler für die angegebenen Eigenschaften dieses Binärprogramms aus der vertrauenswürdigen Basis.
• Die Forscher berichten über zwei isolierte Wiedereinführungen zuvor behobener Fehler, die ihr symbolisches Sicherheitstheorem verletzen.
• Der Komparator überprüft das Theorem und jede abhängige Definition anhand einer geschützten, genehmigten Spezifikation; Änderungen durchlaufen einen separaten überprüften Prozess.

Übersetztes Transkript

Aus der englischen Originalerzählung übersetzt. Verfügbare Audio- und Untertitel werden von YouTube gesteuert.

Wer prüft einen KI-Sicherheitsbeweis?

0:00 Ein KI-Sicherheitsaudit klingt immer noch so, als würde man einem Chatbot vertrauen. Googles neues Signal-Ergebnis kommt mit mathematischen Beweisen, die ein separater Kernel überprüft. Was hat Google in diesem Video bewiesen? Und wie verhindern sie, dass ein Agent die Ziele verschiebt? Hier ist die nützliche Antwort. Modelle schreiben Kandidatenbeweise, und Lean überprüft die Beweise anhand einer von Menschen genehmigten Behauptung über ausgewählten kompilierten Code. Menschen besitzen immer noch die Behauptung und die Annahmen.

0:21 Sie können das Ergebnis überprüfen, ohne der Siegesrede des Modells zu glauben. Eine separate Überprüfung fängt das stille Ändern der Frage ab. Wir werden es bis zu den Definitionen verfolgen. Es ist Dienstag, der zehnte November, und dies ist The Daily Diff. AlphaProof Code ist Googles Framework zum Schreiben von Softwarespezifikationen mit menschlicher Anleitung und zum Generieren überprüfter Beweise mit KI-Agenten. Diese Studie zielt auf libsignal ab, die Rust-Bibliothek, die Signals Nachrichtenprotokoll in einem bestimmten Kommandozeilenprogramm implementiert.

0:45 Google hat die Arbeit heute angekündigt. Das Paper besagt, dass fünf Forscher vier Wochen lang gearbeitet haben. Agenten schrieben die Beweise, während die Menschen den Großteil ihrer Anstrengungen auf die Spezifikationen konzentrierten. Anforderungen haben einen Weg gefunden, noch teurere Besprechungen zu werden. Die Spezifikation besagt, was das Programm tun muss,

Wie wird ein Anspruch zum Beweisziel?

0:59 was ein Angreifer kontrolliert und welche Annahmen das Argument benötigt. Gutachter fragen, ob es die Sicherheit erfasst, die den Menschen wichtig ist. Eine wunderschön überprüfte Antwort auf eine schwache Frage lässt diese Frage intakt. Das Team baut auf früheren Forschungen zum Signal-Handshake und seiner Nachrichten-Schlüssel- Ratsche auf. Formale Analysen hatten diese Designs bereits untersucht. Googles Behauptung verbindet ihre Sicherheitsargumente mit einer unmodifizierten Implementierung einer Produktionsbibliothek, wo das Design den Kontakt mit tatsächlichem Code überleben muss. Signals Chief Technology Officer, Ehren Kret,

1:27 beschreibt eine Erweiterung über frühere, kleinere Verifikationsbereiche hinaus. Implementierungsdetails umfassen Nachrichten, die nicht in der richtigen Reihenfolge eintreffen, und archivierte Sitzungen für verzögerte Nachrichten. Echte Software bewahrt die Belege auf, die Ihr elegantes Diagramm weggeworfen hat. Die Forscher kompilieren die unmodifizierte Rust-Bibliothek mit dem Standard-

Warum das kompilierte Binärprogramm beweisen?

1:41 Compiler zu einem Arm 64-Bit Linux-Executable. Ihre Theoreme beschreiben dieses Binärprogramm mithilfe eines formalen Befehlsmodells, das die Lücke zwischen Quellcode und optimiertem Maschinencode überbrückt. Ein Compilerfehler, der eine angegebene Eigenschaft verletzt, würde das Theorem falsch machen. Der Compiler verlässt daher die vertrauenswürdige Basis für dieses Binärprogramm. Sie vertrauen immer noch dem Befehlsmodell und Leans Checker. Die Vertrauensgrenze hat sich verschoben und hat eine Adresse. Etwa sechseinhalb Millionen Zeilen überprüften Beweises basieren auf ungefähr sechsundzwanzigtausend

2:06 vertrauenswürdigen Spezifikations- und Befehlssemantik-Zeilen. Dies sind Artefaktzählungen. Sie als Intelligenzwerte zu behandeln, ist wie die Rangliste von Entwicklern nach der Größe ihres Node-Module-Ordners.

Welche Sicherheitseigenschaften haben die Implementierungslücke überstanden?

2:16 Die Argumente umfassen die Vertraulichkeit und Authentifizierung von Nachrichten, mit Vorwärtsgeheimnis und Post-Kompromiss-Sicherheit unter den angegebenen Modellen. Die letzten beiden beschreiben Grenzen für gestohlene Schlüssel und die Wiederherstellung nach frischen Austauschen. Jede Garantie hat Bedingungen für den Angreifer und die Sitzung. Kryptografische Primitive liegen hinter vertrauenswürdigen Verträgen. Der Beweis geht davon aus, dass diese Routinen wie spezifiziert funktionieren und stützt sich auf kryptografische Sicherheitsannahmen. Ein Beweis idealisiert die Kryptografie; der andere argumentiert über Angriffserfolgswahrscheinlichkeiten.

2:42 Beide haben Einschränkungen bezüglich der Szenarien, die sie abdecken. Fragen Sie, welcher Build, welche Eigenschaft und welche Annahmen. Dieses Ergebnis betrifft das Kommandozeilen-Harness der Forscher. Gruppen-Messaging ist zukünftige Arbeit, und das Rechenmodell schließt den Multi-Geräte-Zustand aus. Jede Signal-Installation als fehlerfrei zu bezeichnen, geht über das Theorem hinaus. Die Forscher führten zwei zuvor behobene Signal-Bugs in

Kann die Spezifikation fehlerhaften Code ablehnen?

3:02 isolierte Kopien wieder ein und kompilierten sie. Überprüfte Beweise zeigten, dass diese Binärdateien das symbolische Sicherheitstheorem verletzten. Das testete, ob die Spezifikation tatsächlich fehlerhafte Implementierungen ablehnen konnte. Ihr grünes Häkchen braucht einen roten Test. Google veröffentlicht die Spezifikationen und Beweise mit Prüfanweisungen. Das Repository besagt, dass ein sauberer Build Stunden und erheblichen Speicher benötigt. Das Lesen der Ankündigung ist auf dem Laptop wesentlich einfacher. Das Hardwaremodell und vertrauenswürdige Verträge müssen noch überprüft werden.

3:26 Ich habe das enorme Artefakt für diese Episode nicht neu aufgebaut. Wir berichten über das veröffentlichte Ergebnis und seine Grenzen. Außenstehende haben die Möglichkeit, es zu überprüfen, was mir wichtiger ist als eine weitere KI- Siegesrunde. Nun die Falle.

Kann ein korrekter Beweis die falsche Frage beantworten?

3:36 Lean kann einen korrekten Beweis einer Aussage akzeptieren, die fast nichts verlangt. Unmögliche Annahmen können ein Theorem leer machen. Das Ändern einer Definition, die unter dem Überschriftsttheorem vergraben ist, kann das Ziel schwächen. Das Paper entwirft Prüfungen dagegen. Der Gatekeeper bewahrt eine zurückgehaltene, genehmigte Spezifikation auf, in die Beweisagenten nicht schreiben können. Sie können Korrekturen über einen separaten Änderungs-Prozess vorschlagen. Sicherheitsschwächung wird als potenzieller Fehler eskaliert. Die Erfolgserklärung des Prüfers hat hier keine Autorität.

4:00 Menschen entscheiden über Änderungen an vertrauenswürdigen Annahmen, direkt oder durch ihre Richtlinien, und überprüfen Änderungen nach jeder Kampagne. Expertenurteil bleibt in der Verantwortung. Der Agent kann eine andere Zuweisung anfordern. Es kann sich selbst keine bestandene Note geben.

Was fängt die sich bewegenden Ziele ab?

4:13 Hier ist der versprochene Check. Leans Komparator vergleicht das Theorem und jede Definition, von der es abhängt, mit dieser geschützten, genehmigten Kopie. Er überprüft auch erlaubte Axiome und spielt den Beweis in einem neuen Kernel ab. Das leise Schwächen einer Helferdefinition ändert daher das, was verglichen wird. Ein akzeptierter Beweis muss das genehmigte Ziel etablieren. Das lässt die Menschen immer noch dafür verantwortlich, ein starkes Ziel und ehrliche Annahmen zu wählen. Für Ihren eigenen KI-Workflow halten Sie die Akzeptanzkriterien außerhalb der

4:37 Bearbeitungsberechtigungen des Mitarbeiters und überprüfen Sie vorgeschlagene Änderungen separat. Googles Ergebnis macht diese Trennung konkret. Der Beweisverfasser erledigt die Arbeit; die Prüfgrenze entscheidet, ob es zählt. Wenn Sie dies lieber lesen als mich es sagen zu hören, landet der Diff jeden Morgen kostenlos in Ihrem Posteingang unter thedailydiff.dev, Link unten. Das heutige Urteil lautet also SHIP IT.

Würde ich diesen Beweis-Workflow ausliefern?

4:54 Ich würde diesen Workflow für überprüfte Beweise ausliefern, weil die genehmigte Behauptung getrennt von dem Agenten bleibt, der die Antwort erzeugt. Ich würde den Umfang und die Annahmen an jedes Ergebnis anfügen. Abonnieren Sie, klicken Sie auf die Glocke und sagen Sie mir in den Kommentaren, ob Sie es anders gestempelt hätten. Und das ist der Diff für heute. Ich bin Niko von Axrisi. Verantwortungsbewusst mergen.

Quellen

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