Google DeepMind využívá agenty umělé inteligence k ověření strojového kódu jádra Signalu

Google DeepMind představil AlphaProof Code 10. listopadu 2026. Týmy agentů umělé inteligence při tom vytvořily strojově ověřitelné důkazy v Lean pro stanovené bezpečnostní vlastnosti zkompilovaného kódu libsignal používaného aplikací Signal. Pětičlenný výzkumný tým dokončil práci na důkazech za čtyři týdny a zveřejnil specifikace i artefakty potřebné k ověření, aby je mohli posoudit externí odborníci.

Práce překročila rámec abstraktního modelu návrhu protokolu Signalu a zaměřila se na jeho zkompilovanou implementaci. Výzkumníci zabalili neupravené balíčky libsignal v0.105.4 a SPQR v1.6.0 do malého nástroje příkazového řádku a pomocí standardního překladače rustc pak sestavili staticky slinkovaný spustitelný soubor pro AArch64 Linux. Odborná studie popisuje výsledek jako první bezpečnostní důkazy na úrovni protokolu pro neupravený kód široce nasazené implementace kryptografického protokolu.

Jak AlphaProof Code rozdělil práci

Pět výzkumníků věnovalo práci na důkazech čtyři týdny. Agenti během této doby nepřetržitě běželi na jejich pracovních stanicích a výzkumníci souběžně pracovali na symbolických i výpočetních důkazech. Studie uvádí, že agenti vygenerovali přibližně 6,5 milionu řádků strojově ověřitelného kódu důkazů v Lean, který vycházel z přibližně 26 000 řádků důvěryhodných specifikací a sémantiky AArch64.

Lidé vybírali vlastnosti, řešili nejednoznačnosti a kompromisy v oblasti bezpečnosti, posuzovali specifikace a ponechali si konečné schvalovací pravomoci. Agenti využívající Gemini 4 Carbon a Claude Opus 5.5 tyto specifikace připravovali a kontrolovali; kontrolu prováděl i model z jiné rodiny. Týmy agentů Gemini 4 Carbon následně vytvořily veškerý kód důkazů; žádný z autorů žádný kód důkazů nenapsal. Při typických bězích pracovalo na jednom počítači po dobu 24 až 72 hodin 40 až 80 agentů. Orchestrátor a vedoucí týmů koordinovali agenty vytvářející důkazy, zatímco architekt a integrátor udržovali společnou základnu důkazů.

Kontrolní mechanismus přijal důkaz teprve poté, co jej ověřilo jádro Lean a porovnávací nástroj potvrdil, že odpovídá odložené specifikaci schválené člověkem, včetně všech tranzitivních definic, a že používá pouze standardní axiomy Lean. Když důkazy odhalily problémy ve specifikacích, mohli agenti navrhnout drobné úpravy; změny důvěryhodných předpokladů však vyžadovaly schválení člověkem nebo zásady nastavené uživatelem a byly zaznamenány spolu s odůvodněním. Toto opatření řeší zdokumentované riziko důkazů vytvořených agenty: specifikaci lze nepřímo oslabit prostřednictvím některé z jejích definic.

Rozsah ověření zabezpečení a testy historických chyb

Ověřovaný cíl tvořil kód relací typu one-to-one zahrnující navázání spojení PQXDH a zasílání zpráv pomocí Triple Ratchet. Výzkumníci uvádějí dva nezávislé důkazy: deset symbolických vět za idealizovaných kryptografických předpokladů a výpočetní důkaz, který pomocí kryptografických předpokladů a statistických členů stanovuje horní mez výhody útočníka. Mezi ověřované vlastnosti patří dopředné utajení, které chrání dřívější zprávy i po odcizení aktuálního stavu; autentizace; zabezpečení po kompromitaci, tedy zotavení po narušení bezpečnosti; a utajení při navazování spojení. Symbolický důkaz navíc zahrnuje utajení při navazování spojení i po pozdějším prolomení Diffieho–Hellmanovy výměny klíčů.

Aby tým ověřil, zda specifikace dokážou odhalit skutečné chyby, vrátil opravy dvou dříve odstraněných chyb v libsignal, známých jako weak state a small subgroup, a znovu zkompiloval takto pozměněné binární soubory. V obou případech vytvořil důkazy v Lean, že symbolická věta o bezpečnosti neplatí. Veřejné úložiště pro ověřování odděluje materiály k výpočetním a symbolickým důkazům, společný binární soubor a sémantiku AArch64 a popisuje, jak důkazy znovu sestavit a nezávisle ověřit.

Technologický ředitel Signalu Ehren Kret uvedl, že tato práce „nám dává ještě větší jistotu v záruky ochrany soukromí, které náš kód poskytuje“.

Omezení a další kroky

Tyto záruky zdaleka nepotvrzují bezpečnost všech aplikací Signalu. Týkají se sestavení libsignal-cli, které výzkumníci vytvořili a které běží jako nově spuštěný proces; generování klíčů ověřeno nebylo, skupinové zprávy zůstaly předmětem budoucí práce a scénář nezahrnuje postranní kanály ani stav na více zařízeních. Nízkoúrovňové kryptografické primitivy a vybrané výstupní a knihovní rutiny jsou popsány jako důvěryhodné kontrakty, takže výsledek závisí také na těchto kontraktech, schválených specifikacích, jádru Lean, sémantice AArch64 a předpokladech týkajících se primitiv.

Studie uvádí, že ani jeden z důkazů nepotvrzuje postkvantové zotavení, které má SPQR zajistit: výpočetní věta se vztahuje na klasické útočníky, zatímco symbolické věty o ratchetu umožňují útočníkovi zvolit klíče SPQR. Výpočetní model navíc omezuje několik akcí útočníka a při dostatečně velkém počtu zpráv a relací se stává triviálně pravdivým. Tato omezení vymezují, čemu musí externí odborník důvěřovat, než bude strojově ověřené důkazy považovat za záruku bezpečnosti konkrétního nasazení.

Výzkumníci uvádějí, že jejich dalšími kroky jsou posílení vět, zmenšení důvěryhodné základny ověřením dalších napojených rutin a propojením kryptografických kontraktů s ověřenými implementacemi a rozšíření pokrytí na skupinové zprávy, Sealed Sender a protokoly na straně serveru. Jejich cílem je ověřovat nové verze libsignal ještě před vydáním; jde o výzkumný záměr, nikoli o oznámené nasazení.

Bezprostřední význam výsledku spočívá v rozdělení práce, které dokládá: agenti zajišťovali konstrukci důkazů, zatímco jistota správnosti se nadále opírá o specifikace zkontrolované lidmi a výslovně uvedené předpoklady. Zveřejnění důkazů a kontrolních postupů umožňuje externím recenzentům ověřit tento základ, zatímco se výzkumníci snaží začlenit tento pracovní postup do průběžného vývoje libsignal.