Kód a signál AlphaProof: overené bezpečnostné dôkazy strojového kódu a dôveryhodné predpoklady

Čo toto video pokrýva

• Agenti AI produkujú kandidátske dôkazy; jadro Lean kontroluje, či potvrdzujú formálne tvrdenie schválené ľuďmi.
• Overený cieľ je konkrétny kompilovaný libsignal CLI harness, s dôveryhodnou sémantikou a kryptografickými kontraktmi.
• Dokázaním skompilovaného binárneho súboru sa odstráni kompilátor Rust z dôveryhodnej základne pre deklarované vlastnosti tohto binárneho súboru.
• Výskumníci hlásia dve izolované opätovné zavedenia predtým opravených chýb, ktoré porušujú ich symbolickú bezpečnostnú teorému.
• Komparátor kontroluje teorém a každú závislú definíciu oproti chránenej schválenej špecifikácii; zmeny prechádzajú samostatným recenzovaným procesom.

Preložený prepis

Preložené z pôvodného anglického rozprávania. Dostupný zvuk a titulky sú kontrolované službou YouTube.

Kto kontroluje bezpečnostný dôkaz AI?

0:00 Bezpečnostný audit AI stále znie ako dôverovať chatbotovi. Nový výsledok Googlu pre Signal prichádza s matematickými dôkazmi, ktoré kontroluje samostatné jadro. Čo Google v tomto videu dokázal? A ako zabránia agentovi, aby menil ciele? Tu je užitočná odpoveď. Modely píšu kandidátske dôkazy a Lean kontroluje dôkazy proti ľuďmi schválenému tvrdeniu o vybranom skompilovanom kóde. Ľudia stále vlastnia tvrdenie a predpoklady.

0:21 Výsledok si môžete overiť bez toho, aby ste verili víťaznému prejavu modelu. Samostatná kontrola zachytáva tiché zmeny otázky. Pôjdeme až k definíciám. Je utorok, desiateho novembra, a toto je The Daily Diff. AlphaProof Code je framework od Google na písanie softvérových špecifikácií s ľudským vedením a generovanie overených dôkazov s AI agentmi. Táto štúdia sa zameriava na libsignal, knižnicu Rust implementujúcu protokol Signal pre správy, v rámci konkrétneho programu príkazového riadku.

0:45 Google dnes túto prácu oznámil. V článku sa uvádza, že piati výskumníci pracovali štyri týždne. Agenti písali dôkazy, zatiaľ čo ľudia väčšinu svojho úsilia venovali špecifikáciám. Požiadavky si našli cestu k ešte drahším stretnutiam. Špecifikácia hovorí, čo musí program robiť,

Ako sa tvrdenie stane cieľom dôkazu?

0:59 čo ovláda útočník a aké predpoklady argument potrebuje. Recenzenti sa pýtajú, či zachytáva bezpečnosť, na ktorej ľuďom záleží. Nádherne skontrolovaná odpoveď na slabú otázku túto otázku necháva nedotknutú. Tím stavia na predchádzajúcom výskume Signal handshake a jeho kľúča správ ratchet. Formálne analýzy už tieto návrhy študovali. Tvrdenie spoločnosti Google spája ich bezpečnostné argumenty s neupravenou produkčnou implementáciou knižnice, kde návrh musí prežiť kontakt so skutočným kódom. Technický riaditeľ Signal, Ehren Kret,

1:27 opisuje rozšírenie nad rámec menších rozsahov predchádzajúcej verifikácie. Detaily implementácie zahŕňajú out-of-order správy a archivované relácie pre oneskorené správy. Skutočný softvér si uchováva účtenky, ktoré váš elegantný diagram zahodil preč. Výskumníci kompilujú neupravenú knižnicu Rust so štandardným

Prečo dokazovať skompilovaný binárny súbor?

1:41 kompilátorom do spustiteľného súboru Arm 64 Linux. Ich teorémy opisujú tento binárny súbor pomocou formálneho inštrukčného modelu, preklenujúceho medzeru medzi zdrojovým a optimalizovaným strojovým kódom. Chyba kompilátora, ktorá poruší deklarovanú vlastnosť, by spôsobila, že jej teorém bude nepravdivá. Kompilátor preto opúšťa dôveryhodnú základňu pre tento binárny súbor. Stále dôverujete inštrukčnému modelu a kontrole Lean. Hranica dôvery sa posunula a má adresu. Asi šesť a pol milióna riadkov overeného dôkazu spočíva na približne dvadsiatich šiestich

2:06 tisícoch dôveryhodných riadkov špecifikácie a sémantiky inštrukcií. Ide o počty artefaktov. Považovať ich za skóre inteligencie je ako radiť vývojárov podľa veľkosti ich priečinka node_modules.

Ktoré bezpečnostné vlastnosti prežili implementačnú medzeru?

2:16 Argumenty pokrývajú dôvernosť a autentifikáciu správ, s doprednou tajnosťou a bezpečnosťou po kompromitácii v rámci stanovených modelov. Posledné dve opisujú obmedzenia škôd spôsobených ukradnutým kľúčom a obnovy po nových výmenách. Každá záruka má podmienky pre útočníka a reláciu. Kryptografické primitíva stoja za dôveryhodnými kontraktmi. Dôkaz predpokladá, že tieto rutiny sa správajú tak, ako je špecifikované, a spolieha sa na kryptografické bezpečnostné predpoklady. Jeden dôkaz idealizuje kryptografiu; druhý uvažuje o pravdepodobnostiach úspechu útočníka.

2:42 Oba majú obmedzenia v scenároch, ktoré pokrývajú. Opýtajte sa, ktorá zostava, ktorá vlastnosť a ktoré predpoklady. Tento výsledok sa týka príkazového riadku výskumníkov. Skupinové správy sú budúcou prácou a výpočtový model vylučuje stav viacerých zariadení. Povedať, že každá inštalácia Signal je bez chýb, je mimo teorému. Výskumníci znovu zaviedli dve predtým opravené chyby Signal do

Môže špecifikácia odmietnuť chybný kód?

3:02 izolovaných kópií a skompilovali ich. Overené dôkazy ukázali, že tieto binárne súbory porušujú symbolickú bezpečnostnú teorému. To testovalo, či špecifikácia dokáže odmietnuť skutočné chybné implementácie. Vaša zelená značka potrebuje červený test. Google publikuje špecifikácie a dôkazy s kontrolnými pokynmi. Repozitár uvádza, že čistá zostava trvá hodiny a vyžaduje značnú pamäť. Čítanie oznámenia je na notebooku podstatne jednoduchšie. Model hardvéru a dôveryhodné kontrakty stále vyžadujú preskúmanie.

3:26 Pre túto epizódu som obrovský artefakt neprestaval. Oznamujeme publikovaný výsledok a jeho hranice. Outsideri majú možnosť ho skontrolovať, čo je pre mňa dôležitejšie ako ďalšie víťazné kolo AI. Teraz pasca.

Môže správny dôkaz odpovedať na nesprávnu otázku?

3:36 Lean môže prijať správny dôkaz tvrdenia, ktoré si žiada takmer nič. Nemožné predpoklady môžu urobiť teorému prázdnou. Zmena definície, ktorá je pochovaná pod hlavným teorémom, môže oslabiť cieľ. V článku sú navrhnuté kontroly proti tomuto. Dozorca uchováva schválenú špecifikáciu, do ktorej agenti dôkazov nemôžu zapisovať. Môžu navrhovať opravy prostredníctvom samostatného procesu zmien. Oslabenie bezpečnosti sa eskaluje ako potenciálna chyba. Vyhlásenie dôkazcu o úspechu tu nemá žiadnu autoritu.

4:00 Ľudia rozhodujú o zmenách dôveryhodných predpokladov, priamo alebo prostredníctvom ich politiky, a revidujú zmeny po každej kampani. Odborný posudok zostáva v hre. Agent môže požiadať o iné priradenie. Nemôže si udeliť prechádzajúcu známku.

Čo zachytáva pohybujúce sa ciele?

4:13 Tu je sľubovaná kontrola. Komparátor Lean porovná teorému a každú definíciu, na ktorej závisí, s tou chránenou schválenou kópiou. Kontroluje tiež povolené axiómy a prehráva dôkaz v čerstvom jadre. Tiché oslabenie pomocnej definície preto mení to, čo sa porovnáva. Prijatý dôkaz musí stanoviť schválený cieľ. To stále ponecháva na ľuďoch zodpovednosť za výber silného cieľa a čestných predpokladov. Pre váš vlastný pracovný postup s AI, ponechajte kritériá prijatia mimo

4:37 oprávnení na úpravu pracovníka a samostatne preskúmajte navrhované zmeny. Výsledok spoločnosti Google toto oddelenie konkretizuje. Pisár dôkazov robí prácu; kontrolná hranica rozhoduje, či sa to počíta. Ak by ste si to radšej prečítali, než aby ste ma počuli, diff vám pristane v schránke každé ráno, zadarmo na the daily diff dot dev, odkaz nižšie. Takže dnešný verdikt je SHIP IT.

Nasledoval by som tento pracovný postup pre dôkazy?

4:54 Tento overený pracovný postup by som odoslal, pretože schválené tvrdenie zostáva oddelené od agenta produkujúceho odpoveď. Rozsah a predpoklady by som pridal ku každému výsledku. Prihláste sa na odber, stlačte zvonček a povedzte mi v komentároch, či by ste to razili inak. A to je diff pre dnešok. Som Niko z Axrisi. Zlučujte zodpovedne.

Zdroje

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