Google DeepMind matematicky ověřil část kryptografických záruk protokolu Signal
Výzkumníci z Google DeepMind s pomocí AI formálně ověřili vybrané bezpečnostní vlastnosti protokolu Signal. Čtyřtýdenní projekt nepokryl celou aplikaci, ukazuje ale, jak mohou AI agenti urychlit matematickou kontrolu softwaru.
Matematická kontrola protokolu
Výzkumníci z Google DeepMind použili agentickou umělou inteligenci k formálnímu ověření několika důležitých kryptografických záruk protokolu Signal. V praxi to znamená, že pomocí matematických důkazů ověřovali, zda zkoumané části fungují podle stanovených bezpečnostních vlastností. K práci využili nový framework AlphaProof Code.
Projekt trval čtyři týdny a měl podobu ověřovací studie. Protokol Signal chrání komunikaci nejen v aplikaci Signal, ale také ve Zprávách Google a WhatsAppu. Výsledek proto podle autorů představuje další nezávislou kontrolu technologie, na kterou spoléhá velké množství uživatelů.
Nešlo o kontrolu celé aplikace
Analýza se zaměřila na vybrané části protokolu, nikoli na celý software Signal. Formálně ověřena tedy nebyla například kompletní mobilní aplikace. Výzkumníci v prověřovaných částech nenašli nové zranitelnosti a zdůrazňují, že jejich práce je pouze jedním krokem k rozsáhlejšímu ověřování.
Schopnost systému prověřovat i starší verze ukázali na vydáních, která obsahovala známé a již opravené chyby. AlphaProof Code je podle týmu správně rozpoznal a ukázal, že daný protokol nelze formálně ověřit. Výzkumníci zveřejňují specifikaci i důkaz vytvořený pro tuto analýzu, aby mohly posloužit dalším projektům v oblasti formálního ověřování.
AI urychluje práci, ale potřebuje lidi
Formální ověřování je považováno za důležitý způsob, jak matematicky prověřit, zda software splňuje požadované vlastnosti a nemá kritické chyby. Jeho rozšíření však dlouho brzdila časová náročnost: lidé museli popsat, co chtějí ověřit, převést požadavky do formální podoby a následně vytvořit důkaz. Agentická AI může některé z těchto kroků výrazně zrychlit.
Výzkumníci zároveň popisují proces jako spolupráci člověka a AI. Agenti mohou přispívat v různých fázích a opravovat vlastní výstupy, lidé ale zůstávají zapojeni do důležitých rozhodnutí a kontroly. Tým odmítá představu, že by AI sama stanovovala cíle i vytvářela důkazy bez lidského dohledu.
Otázkou zůstává rozsah a cena
Signal už dříve prováděl formální ověřování menších částí svého kódu. Podle technického ředitele společnosti Ehrena Kreta přístup DeepMind umožňuje tuto práci významně rozšířit. Výsledky tak mohou posílit důvěru v implementaci protokolu, neznamenají však záruku, že je bez chyb veškerý software, který jej využívá.
Širší nasazení AI při formálním ověřování zatím zůstává otevřenou otázkou. Není jasné, zda lze takto prověřovat rozsáhlé programy a dodavatelské řetězce softwaru za přijatelnou cenu. DeepMind provedl analýzu Signalu jako výzkumný projekt bez poplatku, Google ale cenu práce nesdělil. Firma také neuvedla, zda plánuje komerční produkt nebo službu pro formální ověřování.