Istraživači iz Googleovog odjela DeepMind ostvarili su značajan uspjeh u području softverske sigurnosti usmjeravanjem agenata umjetne inteligencije prema matematičkom dokazivanju ključnih sigurnosnih svojstava izvornog koda Signalovog protokola, tehnologije koja štiti razgovore korisnika u aplikacijama kao što su Signal, WhatsApp i Google Messages.

Formalna verifikacija, odnosno matematičko dokazivanje da kod funkcionira besprijekorno i bez ranjivosti, predstavlja najviši standard sigurnosnog jamstva, no tradicionalno je izuzetno složena i zahtijeva dugotrajan rad. Ovo je prvi put da je umjetna inteligencija upotrijebljena za formalnu verifikaciju masovno korištenog kriptografskog protokola na ovoj razini, kao i prvi put da je sama implementacija takvog protokola uopće formalno verificirana bilo kojom metodom.

Napredni agentski okvir

Proboj je ostvaren pomoću AlphaProof Codea, novog agentskog okvira s više modela koji dijeli proces formalne verifikacije na način sličan istraživačkom timu. U tom procesu ljudski stručnjaci surađuju s umjetnom inteligencijom kako bi odredili što je potrebno dokazati, pri čemu su stručnjaci pregledali svaku matematičku specifikaciju sigurnosnih ciljeva Signala.

Zatim su agenti pogonjeni modelom Gemini Carbon izradili matematičke dokaze, generirajući više od šest milijuna linija koda u programu Lean, specijaliziranom računalnom jeziku za matematičku potvrdu točnosti koda. Agenti su potom revidirali dokaze i izdvojili svega jedan posto koda koji je zahtijevao dodatnu ljudsku provjeru, što je donijelo uštedu vremena dok je ostatak automatski provjerio Lean.

Ispitivanje sigurnosnih propusta

Kriptografski protokoli čine temelj gotovo cjelokupne digitalne komunikacije, pa pojedinačni propust može odjednom izložiti milijune korisnika. Većina dosadašnjih verifikacija zaustavljala se na razini samog dizajna, dok su agenti Google DeepMinda otišli korak dalje i dokazali da kompajlirani kod zadovoljava ključna sigurnosna svojstva sve do točnog koda koji se izvodi na uređajima. To uključuje i zaštitu poruka prije i nakon što je uređaj privremeno kompromitiran. Budući da se stvarne ranjivosti najčešće kriju upravo u jazu između dizajna i implementacije, cijeli je postupak verifikacije trajao svega četiri tjedna, za razliku od višegodišnjeg rada koji je ranije bio potreban stručnim timovima.

Kako bi potvrdili da AlphaProof Code može jasno razlikovati ispravan kod od onoga s pogreškama, istraživači su u izoliranu verziju Signalova koda ponovno uveli dva stvarna, ranije otklonjena sigurnosna propusta. U oba slučaja sustav je izradio strojno provjerljiv dokaz da je verzija s pogreškom nesigurna.

Rješavanje ovog dugogodišnjeg izazova pokazuje kako umjetna inteligencija može pružiti vrhunsku razinu sigurnosnog jamstva tvrtkama, vladama i kritičnoj infrastrukturi u obrani od kibernetičkih prijetnji vođenih AI agentima. Verifikacija osnovne kriptografije Signala ujedno postavlja temelje za osiguravanje ostalih vitalnih sustava, poput softvera u medicinskim uređajima i upravljačkih sustava energetske mreže, zaključuju iz DeepMinda.