Истражувачите од одделот DeepMind на компанијата Google постигнаа значаен успех во областа на софтверската безбедност. Со помош на агенти на вештачка интелигенција, тие математички ги докажаа клучните безбедносни својства на изворниот код на протоколот Signal. Оваа технологија ги штити разговорите на корисниците во апликации како Signal, WhatsApp и Google Messages.
Формалната верификација, односно математичкиот доказ дека кодот работи беспрекорно и без ранливости, е највисокиот стандард за безбедносна гаранција. Таа, сепак, вообичаено е исклучително сложена и бара долготрајна работа. Ова е првпат вештачка интелигенција да се користи за формална верификација на широко користен криптографски протокол на ова ниво, а воедно и првпат самата имплементација на ваков протокол да биде формално верификувана со каков било метод.
Пробивот е постигнат со AlphaProof Code, нов систем во кој повеќе модели на вештачка интелигенција ја делат работата слично како истражувачки тим. Човечките експерти соработуваат со вештачката интелигенција за да утврдат што треба да се докаже, а потоа ја прегледуваат секоја математичка спецификација на безбедносните цели на протоколот Signal.
Потоа агентите, кои работат со моделот Gemini Carbon, ги изработиле математичките докази и создале повеќе од шест милиони линии код во програмата Lean. Тоа е специјализиран компјутерски јазик со кој математички се потврдува точноста на кодот. Агентите потоа ги провериле доказите и издвоиле само еден отсто од кодот за дополнителна човечка проверка, а остатокот автоматски го проверила програмата Lean.
Криптографските протоколи се темел на речиси целата дигитална комуникација, па еден единствен пропуст може одеднаш да изложи милиони корисници на опасност. Повеќето досегашни проверки застанувале на ниво на дизајнот на протоколот. Агентите на DeepMind отишле чекор подалеку и докажале дека и самиот код што се извршува на уредите ги исполнува клучните безбедносни својства.
Ова е особено важно бидејќи вистинските ранливости најчесто се кријат токму во јазот меѓу дизајнот и практичната изведба. Доказот опфаќа и заштита на пораките пред и по моментот кога уредот привремено бил компромитиран. Целата постапка траела само четири недели, наспроти долгогодишната работа што порано им била потребна на стручните тимови.
За да потврдат дека системот може јасно да го разликува исправниот од неисправниот код, истражувачите во изолирана верзија на кодот повторно внеле два вистински безбедносни пропусти, кои претходно биле отстранети. Во двата случаја системот изработил доказ, кој може да го провери компјутер, дека верзијата со грешка не е безбедна.
Решавањето на овој долгогодишен предизвик покажува дека вештачката интелигенција може да им понуди врвна безбедносна гаранција на компаниите, владите и критичната инфраструктура во одбраната од сајбер-заканите. Од DeepMind порачуваат дека проверката на протоколот Signal ги поставува темелите и за заштита на други витални системи, како софтверот во медицинските уреди и системите за управување со електричната мрежа.
