AI od Google DeepMind prokázala bezpečnostní záruky protokolu Signal

Výzkumníci z Google DeepMind, divize společnosti Alphabet Inc. ↘ 0.21%, využili nový rámec umělé inteligence s názvem AlphaProof Code k matematickému prokázání několika hlavních kryptografických záruk protokolu Signal. Čtyřtýdenní projekt typu proof-of-concept neodhalil žádné nové zranitelnosti v částech protokolu, které zkoumal, informoval server WIRED 10. listopadu.wired.com

Výsledek má význam přesahující samotnou aplikaci Signal. Protokol také zabezpečuje zprávy ve službách Google Messages a WhatsApp společnosti Meta Platforms, Inc. ↗ 0.22%, takže analýza přidává další nezávislou kontrolu šifrování, které chrání velkou část světové komunikace, uvádí WIRED. Zároveň ukazuje, že agenti umělé inteligence mohou zkrátit formální verifikaci, což je dlouho vyhledávaný, ale pomalý způsob využití matematiky k prokázání, že software funguje podle záměru.wired.com

Co analýza zjistila

Výzkumníci testovali AlphaProof Code na starších verzích Signalu, které obsahovaly známé zranitelnosti, jež byly dávno opraveny. Nástroj tyto chyby správně našel a ukázal, že tyto verze nebylo možné formálně verifikovat, uvedl WIRED. DeepMind zveřejňuje specifikaci a důkaz, který vytvořil, aby je mohly využít další verifikační úsilí.wired.com

Rozsah byl omezený. Práce neověřila celou mobilní aplikaci Signal a výzkumníci ji popsali jako jeden milník v delším procesu. „Jsme z tohoto výsledku velmi nadšeni, ale je před námi ještě dlouhá cesta, než budeme schopni toto škálovat na veškerý software na světě, a chceme to udělat,“ řekl pro WIRED výzkumný vědec DeepMind Swarat Chaudhuri.wired.com

Tým uvedl, že předchozí práce na formální verifikaci ze strany Signalu jim poskytla náskok. „Zatímco předchozí formální verifikace se zaměřovala na menší části kódu, přístup Google DeepMind umožňuje významné rozšíření,“ uvedl v prohlášení technický ředitel Signalu Ehren Kret a dodal, že verifikace dává společnosti „ještě větší jistotu“ v době, kdy rostou bezpečnostní hrozby řízené umělou inteligencí.wired.com

Přeplněné pole

Práce DeepMind přichází v době, kdy se o podobné cíle snaží i další skupiny. V dubnu 2026 spustily Signal, Beneficial AI Foundation a Lean FRO projekt Signal Shot, veřejnou iniciativu zaměřenou na verifikaci protokolu Signal a jeho implementace v jazyce Rust pomocí asistenta důkazů Lean. Cílem projektu je přeložit skutečný kód Signalu do jazyka Lean a dokázat, že odpovídá verifikovanému modelu protokolu, uvádí nadace. Výsledek DeepMind je od tohoto projektu oddělený, poznamenal Startup Fortune.beneficialaifoundation.org+2

Otevřené otázky ohledně nákladů

Zda lze automatizovanou verifikaci pomocí AI škálovat za přijatelnou cenu, je stále nejasné. DeepMind provedl analýzu Signalu zdarma jako výzkumný projekt. Google odmítl sdělit, kolik to stálo nebo zda plánuje komerční verifikační produkt, informoval WIRED.wired.com

Chaudhuri uvedl, že klíčovým pokrokem byl proces, při kterém agenti AI přispívají a opravují svou vlastní práci, zatímco lidé ji v klíčových bodech kontrolují. „Nechceme svět, kde AI generuje cíle a AI generuje důkazy a v podstatě dělá testy, které si sama napsala,“ řekl. „Existuje střední cesta.“wired.com