Kód a signál AlphaProof: prověřené bezpečnostní důkazy strojového kódu a důvěryhodné předpoklady

Co toto video pokrývá

• Agenti umělé inteligence vytvářejí kandidátské důkazy; jádro Lean kontroluje, zda prokazují lidmi schválený formální nárok.
• Ověřeným cílem je konkrétní kompilovaný nástroj libsignal CLI s důvěryhodnou sémantikou a kryptografickými kontrakty.
• Dokazování kompilovaného binárního souboru odstraňuje kompilátor Rust z důvěryhodné základny pro uvedené vlastnosti tohoto binárního souboru.
• Výzkumníci hlásí dvě izolovaná znovuzavedení dříve opravených chyb, které porušují jejich symbolický bezpečnostní teorém.
• Komparátor kontroluje teorém a každou závislou definici proti chráněné schválené specifikaci; změny procházejí samostatným procesem revize.

Přeložený přepis

Přeloženo z původního anglického vyprávění. Dostupné audio a titulky jsou řízeny YouTube.

Kdo kontroluje bezpečnostní důkaz AI?

0:00 Bezpečnostní audit AI stále zní jako důvěřovat chatbotovi. Nový výsledek Google Signal přichází s matematickými důkazy, které samostatné jádro kontroluje. Co Google v tomto videu dokázal? A jak zabrání agentovi měnit cíle? Zde je užitečná odpověď. Modely píší kandidátské důkazy a Lean kontroluje důkazy proti lidsky schválenému tvrzení o vybraném kompilovaném kódu. Lidé stále vlastní tvrzení a předpoklady.

0:21 Výsledek můžete zkontrolovat, aniž byste věřili vítěznému projevu modelu. Samostatná kontrola zachytí tiché změny otázky. Půjdeme až k definicím. Je úterý, desátého listopadu, a toto je The Daily Diff. AlphaProof Code je framework společnosti Google pro psaní softwarových specifikací s lidským vedením a generování ověřených důkazů pomocí AI agentů. Tato studie se zaměřuje na libsignal, knihovnu Rust implementující protokol pro zasílání zpráv Signal, uvnitř konkrétního programu příkazového řádku.

0:45 Google dnes práci oznámil. V jeho článku se píše, že pět výzkumníků pracovalo přes čtyři týdny. Agenti psali důkazy, zatímco lidé většinu svého úsilí věnovali specifikacím. Požadavky našly způsob, jak se stát ještě dražšími schůzkami. Specifikace říká, co program musí dělat,

Jak se tvrzení stane cílem důkazu?

0:59 co útočník ovládá a jaké předpoklady argument potřebuje. Recenzenti se ptají, zda zachycuje bezpečnost, o kterou se lidé starají. Krásně zkontrolovaná odpověď na slabou otázku ponechává tuto otázku beze změny. Tým navazuje na dřívější výzkum handshake Signal a jeho message-key ratchetu. Formální analýzy již tyto návrhy studovaly. Tvrzení společnosti Google spojuje jejich bezpečnostní argumenty s nemodifikovanou produkční kompilovanou implementací knihovny, kde návrh musí přežít kontakt se skutečným kódem. Technický ředitel Signal, Ehren Kret,

1:27 popisuje rozšíření nad rámec menších rozsahů dřívějšího ověřování. Detaily implementace zahrnují zprávy doručované mimo pořadí a archivované relace pro zpožděné zprávy. Skutečný software uchovává účtenky, které váš elegantní diagram zahodil. Výzkumníci kompilují nemodifikovanou knihovnu Rust se standardním

Proč dokazovat kompilovaný binární soubor?

1:41 kompilátorem do spustitelného souboru Arm 64 Linux. Jejich teorémy popisují tento binární soubor pomocí formálního instrukčního modelu, překlenující mezeru mezi zdrojovým a optimalizovaným strojovým kódem. Chyba kompilátoru, která by porušila deklarovanou vlastnost, by způsobila, že její teorém bude nepravdivý. Kompilátor proto opouští důvěryhodnou základnu pro tento binární soubor. Stále důvěřujete instrukčnímu modelu a kontroloru Lean. Hranice důvěry se posunula a má adresu. Přibližně šest a půl milionu řádků ověřeného důkazu spočívá na zhruba dvaceti šesti

2:06 tisících důvěryhodných řádcích specifikace a sémantiky instrukcí. Toto jsou počty artefaktů. Zacházení s nimi jako s inteligenčními skóre je jako řadit vývojáře podle velikosti jejich složky node_modules.

Které bezpečnostní vlastnosti přežily mezeru v implementaci?

2:16 Argumenty pokrývají důvěrnost a autentizaci zpráv, s dopřednou tajností a bezpečností po kompromitaci podle uvedených modelů. Tyto poslední dvě popisují omezení poškození ukradeným klíčem a obnovu po nových výměnách. Každá záruka má podmínky pro útočníka a relaci. Kryptografické primitivy jsou za důvěryhodnými kontrakty. Důkaz předpokládá, že tyto rutiny se chovají podle specifikace a spoléhá na kryptografické bezpečnostní předpoklady. Jeden důkaz idealizuje kryptografii; druhý uvažuje o pravděpodobnostech úspěchu útočníka.

2:42 Oba mají omezení na scénáře, které pokrývají. Zeptejte se, jaká sestava, jaká vlastnost a jaké předpoklady. Tento výsledek se týká nástroje příkazového řádku výzkumníků. Skupinové zasílání zpráv je budoucí práce a výpočetní model vylučuje stav více zařízení. Nazvat každou instalaci Signal bezchybnou je mimo teorém. Výzkumníci znovu zavedli dvě dříve opravené chyby Signal do

Může specifikace odmítnout vadný kód?

3:02 izolovaných kopií a zkompilovali je. Ověřené důkazy ukázaly, že tyto binární soubory porušovaly symbolický bezpečnostní teorém. To testovalo, zda specifikace dokáže odmítnout skutečné nefunkční implementace. Vaše zelená fajfka potřebuje červený test. Google zveřejňuje specifikace a důkazy s instrukcemi pro ověření. Úložiště uvádí, že čistá sestava trvá hodiny a značné množství paměti. Čtení oznámení je na notebooku podstatně snazší. Hardwarový model a důvěryhodné kontrakty stále vyžadují revizi.

3:26 Pro tuto epizodu jsem nepřestavěl ten obrovský artefakt. Informujeme o publikovaném výsledku a jeho hranicích. Outsideri mají cestu k jeho prozkoumání, což je pro mě důležitější než další vítězné kolo AI. Nyní past.

Může správný důkaz odpovědět na špatnou otázku?

3:36 Lean může přijmout správný důkaz tvrzení, které požaduje téměř nic. Nemožné předpoklady mohou učinit teorém prázdným. Změna definice pohřbené pod hlavním teorémem může oslabit cíl. Článek navrhuje kontroly proti tomuto. Dozorce udržuje vyhrazenou schválenou specifikaci, do které agenti důkazu nemohou zapisovat. Mohou navrhovat opravy prostřednictvím samostatného procesu změn. Oslabení bezpečnosti je eskalováno jako potenciální chyba. Prohlášení prokazovatele o úspěchu zde nemá žádnou autoritu.

4:00 Lidé posuzují změny důvěryhodných předpokladů, přímo nebo prostřednictvím své politiky, a revidují změny po každé kampani. Odborný úsudek zůstává v sázce. Agent může požádat o jiné zadání. Nemůže si sám udělit prospěch.

Co zachytí pohyblivé cíle?

4:13 Zde je slíbená kontrola. Komparátor Lean porovnává teorém a každou definici, na které závisí, s touto chráněnou schválenou kopií. Kontroluje také povolené axiomy a přehrává důkaz v novém jádře. Tiché oslabení pomocné definice proto mění to, co se porovnává. Přijatý důkaz musí prokázat schválený cíl. To stále ponechává na lidech odpovědnost za výběr silného cíle a poctivé předpoklady. Pro váš vlastní pracovní postup AI udržujte kritéria přijetí mimo

4:37 oprávnění k úpravám pracovníka a navrhované změny revidujte samostatně. Výsledek společnosti Google tuto separaci konkretizuje. Tvůrce důkazů vykonává práci; hranice kontroly rozhoduje, zda se počítá. Pokud byste si to raději přečetli, než abyste to slyšeli ode mě, The Daily Diff přistává ve vaší schránce každé ráno, zdarma na thedailydiff.dev, odkaz níže. Takže dnešní verdikt je SHIP IT.

Nasazoval bych tento pracovní postup důkazů?

4:54 Tento pracovní postup s ověřeným důkazem bych nasadil, protože schválené tvrzení zůstává oddělené od agenta produkujícího odpověď. Rozsah a předpoklady bych uchoval u každého výsledku. Přihlaste se k odběru, stiskněte zvoneček a dejte mi vědět v komentářích, zda byste to označili jinak. A to je pro dnešek The Daily Diff. Jsem Niko z Axrisi. Sloučit zodpovědně.

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