Nový nástroj Google DeepMind formálně ověřil vybrané bezpečnostní záruky šifrovacího protokolu Signal. Cílem výzkumníků je podle Wired zajít dál a ověřit software celého světa, ale to je zatím vzdálený cíl.
Wired popisuje, že výzkumníci DeepMind použili AI nástroj AlphaProof Code k formální verifikaci vybraných kryptografických záruk široce používaného šifrovacího protokolu Signal. Formální verifikace matematicky dokazuje, že systém splňuje zadané vlastnosti, a je tedy silnější než běžné testování.
Šlo o čtyřtýdenní výzkumný projekt s omezeným rozsahem: v prozkoumaných částech protokolu nebyly nalezeny nové zranitelnosti a celá mobilní aplikace Signal ověřena nebyla. Na starších verzích se známými, dávno opravenými chybami nástroj tyto chyby odhalil a ukázal, že je nelze ověřit.
Výzkumníci mají ambicióznější plán: stejný postup chtějí uplatnit na veškerý software světa. Podle výzkumníka DeepMind Swarata Chaudhuriho je však škálování na veškerý software ještě daleko. Zdroj neuvádí časový rámec.
Proč by vás to mělo zajímat
Formálně ověřené záruky protokolu Signal znamenají vyšší jistotu u zpráv, které denně posíláte, ale ověřena byla jen část protokolu, nikoli celé aplikace. Sledujte, zda se podobné ověřování rozšíří i na další komponenty, které ve firmě používáte.
