AlphaProof Code og Signal: sjekkede maskinkodesikkerhetsbevis og klarerte antagelser

Hva denne videoen dekker

• AI-agenter produserer kandidatbevis; Leans kjerne sjekker om de etablerer det menneskegodkjente formelle kravet.
• Det verifiserte målet er en spesifikk kompilert libsignal CLI-sele, med klarert semantikk og kryptografiske kontrakter.
• Å bevise den kompilerte binære fjerner Rust-kompilatoren fra den klarerte basen for den binærens angitte egenskaper.
• Forskerne rapporterer to isolerte gjeninnføringer av tidligere fiksete feil som bryter med deres symbolske sikkerhetsteorem.
• Komparatoren sjekker teoremet og hver avhengige definisjon mot en beskyttet godkjent spesifikasjon; endringer går gjennom en separat vurdert prosess.

Oversatt transkripsjon

Oversatt fra den originale engelske fortellingen. Tilgjengelig lyd og undertekster kontrolleres av YouTube.

Hvem sjekker et AI-sikkerhetsbevis?

0:00 En AI-sikkerhetsrevisjon høres fortsatt ut som å stole på en chatbot. Googles nye Signal-resultat kommer med matematiske bevis en separat kjerne sjekker. I denne videoen, hva beviste Google? Og hvordan hindrer de en agent fra å flytte målstreken? Her er det nyttige svaret. Modeller skriver kandidatbevis, og Lean sjekker bevisene mot et menneskegodkjent krav om utvalgt kompilert kode. Mennesker eier fortsatt kravet og antagelsene.

0:21 Du kan sjekke resultatet uten å tro på modellens seierstale. En separat sjekk fanger stille endring av spørsmålet. Vi vil følge det ned til definisjonene. Det er tirsdag, tiende november, og dette er The Daily Diff. AlphaProof Code er Googles rammeverk for å skrive programvare-spesifikasjoner med menneskelig veiledning og generere sjekkede bevis med AI-agenter. Denne studien er rettet mot libsignal, Rust-biblioteket som implementerer Signals meldingsprotokoll, inne i et bestemt kommandolinjeprogram.

0:45 Google kunngjorde arbeidet i dag. Deres artikkel sier fem forskere jobbet over fire uker. Agenter skrev bevisene, mens mennesker brukte mesteparten av sin innsats på spesifikasjonene. Krav har funnet en måte å bli enda dyrere møter. Spesifikasjonen sier hva programmet skal gjøre,

Hvordan blir et krav et beivismål?

0:59 hva en angriper kontrollerer, og hvilke antagelser argumentet trenger. Anmelderne spør om det fanger opp sikkerheten folk bryr seg om. Et vakkert sjekket svar på et svakt spørsmål lar det spørsmålet være intakt. Teamet bygger på tidligere forskning på Signals håndtrykk og dets meldingsnøkkel-ratchet. Formelle analyser har allerede studert disse designene. Googles påstand kobler deres sikkerhetsargumenter til en uendret produksjonsbiblioteks kompilerte implementering, der designet må overleve kontakt med faktisk kode. Signals teknologidirektør, Ehren Kret,

1:27 beskriver en utvidelse utover tidligere verifikasjoners mindre omfang. Implementeringsdetaljer inkluderer meldinger som kommer ut av rekkefølge og arkiverte sesjoner for forsinkede meldinger. Ekte programvare beholder kvitteringene ditt elegante diagram kastet bort. Forskerne kompilerer det umodifiserte Rust-biblioteket med standard

Hvorfor bevise den kompilerte binære?

1:41 kompilatoren til en Arm sekstifire Linux-kjørbar fil. Deres teoremer beskriver den binære filen ved hjelp av en formell instruksjonsmodell, som når over gapet mellom kilde og optimalisert maskinkode. En kompilatorfeil som bryter en angitt egenskap vil gjøre teoremet falskt. Kompilatoren forlater derfor den klarerte basen for denne binære filen. Du stoler fortsatt på instruksjonsmodellen og Leans sjekker. Tillitsgrensen flyttet seg, og den har en adresse. Omtrent seks og en halv million linjer med sjekket bevis hviler på omtrent tjueseks

2:06 tusen klarerte spesifikasjons- og instruksjonssemantikklinjer. Dette er artefakttall. Å behandle dem som intelligensscore er som å rangere utviklere etter størrelsen på deres node modules-mappe.

Hvilke sikkerhetsegenskaper overlevde implementeringsgapet?

2:16 Argumentene dekker meldingskonfidensialitet og autentisering, med fremoverhemmelighet og sikkerhet etter kompromiss under angitte modeller. De to siste beskriver grenser for skader fra stjålne nøkler og gjenoppretting etter nye utvekslinger. Hver garanti har betingelser for angriperen og sesjonen. Kryptografiske primitiver sitter bak klarerte kontrakter. Beviset antar at disse rutinene oppfører seg som spesifisert og er avhengig av kryptografiske sikkerhetsantagelser. Ett bevis idealiserer kryptografi; det andre resonnerer om angriperens suksesssannsynligheter.

2:42 Begge har restriksjoner på scenariene de dekker. Spør hvilken bygg, hvilken egenskap, og hvilke antagelser. Dette resultatet gjelder forskernes kommandolinjesele. Gruppemeldinger er fremtidig arbeid, og den beregningsmodellen utelukker flerenhetstilstand. Å kalle hver Signal-installasjon feilfri, vandrer utenfor teoremet. Forskerne gjeninnførte to tidligere fiksete Signal-feil i

Kan spesifikasjonen avvise ødelagt kode?

3:02 isolerte kopier og kompilerte dem. Sjekkede bevis viste at disse binære filene brøt med det symbolske sikkerhetsteoremet. Det testet om spesifikasjonen kunne avvise ekte ødelagte implementasjoner. Ditt grønne hake trenger en rød test. Google publiserer spesifikasjonene og bevisene med sjekkinstruksjoner. Repositoryet sier en ren bygging tar timer og betydelig minne. Å lese kunngjøringen er betydelig enklere på laptopen. Maskinvaremodellen og klarerte kontrakter trenger fortsatt gjennomgang.

3:26 Jeg har ikke bygget om den enorme artefakten for denne episoden. Vi rapporterer det publiserte resultatet og dets grenser. Utenforstående har en vei til å inspisere det, noe som betyr mer for meg enn en ny AI seiersrunde. Nå fellen.

Kan et korrekt bevis svare på feil spørsmål?

3:36 Lean kan akseptere et korrekt bevis for en påstand som ber om nesten ingenting. Umulige antagelser kan gjøre et teorem tomt. Å endre en definisjon begravd under hovedteoremet kan svekke målet. Artikkelen designer sjekker mot dette. Portvakten holder en holdt-ut godkjent spesifikasjon som bevisagenter ikke kan skrive til. De kan foreslå korreksjoner gjennom en separat endringsprosess. Sikkerhetssvekkelse blir eskalert som en potensiell feil. Bevisførerens erklæring om suksess har ingen autoritet her.

4:00 Mennesker bedømmer endringer i klarerte antagelser, direkte eller gjennom deres politikk, og gjennomgår endringer etter hver kampanje. Ekspertvurdering forblir på kroken. Agenten kan be om en annen oppgave. Den kan ikke gi seg selv en bestått karakter.

Hva fanger de flyttbare målene?

4:13 Her er den lovede sjekken. Leans komparator sammenligner teoremet og hver definisjon det er avhengig av med den beskyttede godkjente kopien. Den sjekker også tillatte aksiomer og spiller av beviset i en fersk kjerne. Stille svekkelse av en hjelpedefinisjon endrer derfor det som blir sammenlignet. Et akseptert bevis må etablere det godkjente målet. Det overlater fortsatt mennesker ansvar for å velge et sterkt mål og ærlige antagelser. For din egen AI-arbeidsflyt, hold akseptkriteriene utenfor

4:37 arbeiderens redigeringstillatelser og gjennomgå foreslåtte endringer separat. Googles resultat gjør denne separasjonen konkret. Bevisskriveren gjør jobben; sjekkegrensen bestemmer om det teller. Hvis du heller vil lese dette enn å høre meg si det, lander diffen i innboksen din hver morgen, gratis på the daily diff dot dev, lenke nedenfor. Så dagens dom er SHIP IT.

Ville jeg implementert denne bevisarbeidsflyten?

4:54 Jeg ville implementert denne sjekkede bevis-arbeidsflyten fordi det godkjente kravet forblir atskilt fra agenten som produserer svaret. Jeg ville holdt omfanget og antagelsene knyttet til hvert resultat. Abonner, trykk på bjellen, og fortell meg i kommentarene om du ville ha stemplet det annerledes. Og det er diffen for i dag. Jeg er Niko fra Axrisi. Slå sammen ansvarlig.

Kilder

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