Googleova umjetna inteligencija za četiri sedmice provjerila koliko je Signal siguran

Kada aplikacija za poruke tvrdi da je „šifrovana s kraja na kraj“, korisnik to uglavnom mora uzeti zdravo za gotovo. Stručnjaci mogu pregledati kod, ali pregled nije dokaz. Google DeepMind je u utorak objavio da je za kod Signal protokola napravio nešto strože: formalni, mašinski provjeren matematički dokaz da ključne zaštite rade kako je obećano.

Signal protokol nije važan samo korisnicima aplikacije Signal. Na njemu se od 2016. zasniva i šifrovanje WhatsAppa, koji je tada, prema objavi Signala, imao više od milijardu korisnika. Važno je, ipak, razlikovati: DeepMind je provjeravao Signalov kod, ne WhatsAppovu verziju protokola.

Šta je tačno dokazano

U objavi koju potpisuju Pushmeet Kohli i Swarat Chaudhuri iz DeepMinda navodi se da su dokazana ključna sigurnosna svojstva stvarnog koda na kojem Signal protokol radi, i to sve do koda koji se stvarno izvršava na uređajima. Jedan od primjera je da poruke ostaju zaštićene i prije i poslije trenutka kada je uređaj privremeno kompromitovan.

DeepMind tvrdi da je ovo prvi put da je umjetna inteligencija iskorištena za ovako duboku formalnu provjeru kriptografskog protokola koji se masovno koristi, ali i prvi put da je implementacija takvog protokola uopće formalno provjerena, s AI ili bez nje.

Ljudi biraju šta se dokazuje, agenti rade ostalo

AlphaProof Code je sistem u kojem ljudi odlučuju šta treba dokazati, a grupa AI agenata piše dokaze. Agente pokreće Gemini Carbon, najjači Googleov model, koji je kompanija ove sedmice pustila i developerima i pretplatnicima najskupljeg plana Google AI Ultra. Dokazi su napisani u Leanu, programskom jeziku u kojem računar sam provjerava da li je svaki korak dokaza ispravan.

Prema DeepMindu, agenti su samo oko jedan posto koda izdvojili da ga pregledaju ljudi. Cijeli posao trajao je četiri sedmice, dok ovakvi zadaci, navodi DeepMind, stručnim timovima tradicionalno traju godinama.

Test s poznatim greškama

DeepMind u objavi ne navodi da je u Signalovom kodu pronašao nove greške. Da bi provjerili radi li sistem, istraživači su u izdvojenu kopiju koda vratili dvije stvarne greške koje su ranije već bile ispravljene. U oba slučaja sistem je proizveo mašinski provjeren dokaz da je takva verzija nesigurna.

„Kako rastu sigurnosne prijetnje koje pokreće AI, rigorozna provjera implementacije Signal protokola daje nam još veće povjerenje“, rekao je tehnički direktor Signala Ehren Kret. DeepMind navodi da materijale iz provjere objavljuje kao otvoreni kod, kako bi ih mogli koristiti i drugi.

Šta to znači za vas

Za korisnika se u aplikaciji ništa ne mijenja i ne treba ništa podešavati. Dokaz se odnosi na šifrovanje poruka na putu između uređaja. Ne štiti od prevaranta koji vas nagovori da mu pošaljete kod za prijavu, niti od nekoga ko ima vaš otključan telefon u ruci.