DeepMind provjerio sigurnosna svojstva Signalova koda

Google DeepMind predstavio je AlphaProof Code, sustav AI agenata koji je matematički provjerio odabrana sigurnosna svojstva konkretne implementacije Signalova protokola. Agenti su proizveli približno 6,5 milijuna redaka dokaza u jeziku Lean, oslonjenih na približno 26.000 redaka pouzdanih specifikacija i formalne semantike procesora AArch64.

Provjera obuhvaća uspostavu veze protokolom PQXDH i razmjenu poruka mehanizmom Triple Ratchet. Istraživači su dokazivali svojstva kao što su povjerljivost poruka, autentikacija te zaštita ranijih i budućih poruka nakon određenih vrsta kompromitacije. Novost je što su tvrdnje povezane s prevedenim strojnim kodom promatrane implementacije, a ne samo s apstraktnim modelom protokola.

Formalna verifikacija razlikuje se od uobičajenog testiranja: nastoji matematički dokazati da program zadovoljava precizno opisane uvjete. Pritom valjanost dokaza ovisi o tome jesu li specifikacije potpune i jesu li pretpostavke modela primjenjive. To nije opće jamstvo da sustav nema nikakvu ranjivost.

AlphaProof Code kombinira agente koji uz ljudsku pomoć oblikuju specifikacije s agentima koji izrađuju dokaze. Rezultat vrijedi tek kada ga prihvati provjeravatelj u jezgri sustava Lean. Ljudski stručnjaci i dalje određuju što treba dokazati, provjeravaju pretpostavke i odgovaraju za tumačenje rezultata.

Opseg od 6,5 milijuna redaka nije sam po sebi mjera kvalitete modela, ali ilustrira razmjer posla koji bi ručno bio iznimno skup. DeepMind uspoređuje pristup s projektima poput operacijskog sustava seL4 i prevoditelja CompCert, čiji su formalni dokazi tražili godine stručnog rada. AI ovdje automatizira velik dio izvođenja, ne i sigurnosnu odgovornost.

Istraživači su javno objavili specifikacije i dokaze kako bi drugi stručnjaci mogli pregledati opseg istraživanja. To je važno jer naslovna tvrdnja da je cijeli Signal „dokazan sigurnim” ne bi bila točna. Rad se odnosi na određenu verziju biblioteke libsignal i skup sigurnosnih svojstava, ali ne obuhvaća sve dijelove aplikacije, operacijski sustav, način čuvanja ključeva na uređaju ili društveni inženjering.

Razvoj bi mogao smanjiti trošak primjene formalnih metoda. Formalne metode dosad su uglavnom bile dostupne projektima s velikim proračunom i malim, stabilnim kodom. Ako agentski dokazivači smanje vrijeme izrade i održavanja dokaza, mogli bi se proširiti na kriptografske biblioteke, čipove, kritične upravljačke sustave i osjetljive cloud komponente.

Praktična vrijednost ovisit će o održavanju dokaza nakon svake promjene koda. Nova verzija biblioteke može poništiti dio rezultata i zahtijevati ponovno dokazivanje. Sljedeći mjerljiv korak bit će primjena istog okvira na druge implementacije i objava vremena, računalnog troška te ljudskog rada potrebnog za ažuriranje 6,5 milijuna redaka provjere.

Formalni dokaz može biti osobito vrijedan za široko korišten kriptografski kod, ali se mora održavati nakon promjena implementacije. Nova verzija biblioteke može zahtijevati ponovnu provjeru dijela ili svih dokaza. U ovom istraživanju ključna je i kvaliteta približno 26.000 redaka pouzdane osnove: dokaz ostaje ograničen svojstvima koja su istraživači odlučili formalizirati. Objavljeni repozitorij omogućuje drugim timovima da pokušaju reproducirati postupak i procijeniti trošak njegova održavanja.