Google DeepMind MI aģenti matemātiski pierāda Signal šifrēšanas koda drošības īpašības

Google DeepMind pētnieki otrdien, 10. novembrī, paziņoja, ka ar MI aģentu palīdzību ir matemātiski pierādījuši vairākas būtiskas Signal protokola drošības īpašības. Pārbaudīts ne tikai protokola apraksts, bet arī reālais kods, uz kura balstās šifrētā saziņa tādās lietotnēs kā Signal un Google Messages.

Darbā izmantots jauns rīks AlphaProof Code – vairāku MI aģentu sistēma programmatūras formālai verifikācijai. Ar formālo verifikāciju matemātiski pierāda, ka programma dara tieši to, kas tai noteikts. To uzskata par augstāko drošības pārbaudes līmeni, taču tradicionāli tā prasa ļoti daudz darba.

Process sadalīts posmos. Vispirms pētnieki kopā ar MI modeļiem pārvērta Signal drošības mērķus formālās specifikācijās pierādījumu valodā Lean, un katru no tām pārskatīja cilvēki. Pēc tam aģenti, kurus darbina Google modelis Gemini Carbon, izveidoja pašus pierādījumus – kopumā aptuveni 6,5 miljonus rindu Lean koda. Pierādījums tiek pieņemts tikai tad, ja to apstiprina Lean automātiskā pārbaude.

Pārbaudīta oficiālās Signal bibliotēkas libsignal kompilētā mašīnkoda daļa, kas nodrošina sesijas izveidi ar pēckvantu atslēgu apmaiņu PQXDH un ziņu šifrēšanu ar mehānismu Triple Ratchet. Pierādījumi aptver tādas īpašības kā sarunas dalībnieku autentifikācija, agrāko ziņu aizsardzība arī tad, ja atslēgas vēlāk nonāk svešās rokās, un drošības atjaunošanās pēc tam, kad ierīce bijusi īslaicīgi kompromitēta.

Darbu četrās nedēļās paveica piecu cilvēku komanda, lai gan līdzīga apjoma verifikācija agrāk prasījusi gadus. Lai pārliecinātos, ka sistēma spēj atšķirt drošu kodu no kļūdaina, pētnieki izolētā Signal koda versijā atkal ieviesa divas reālas, jau sen izlabotas kļūdas. Abos gadījumos sistēma ar pārbaudītu pierādījumu parādīja, ka šāda versija nav droša.

Rezultātam ir arī ierobežojumi. Pierādījumi pieņem, ka pašas kriptogrāfijas pamatfunkcijas ir drošas, un attiecas uz konkrētām koda daļām un īpašībām, nevis uz visu lietotni vai jebkuru iespējamo uzbrukumu.

Pagaidām tas ir pētniecības projekts, nevis komerciāls produkts. DeepMind publiskojis izstrādātās specifikācijas un pierādījumus, lai tos varētu izmantot arī citi formālās verifikācijas pētnieki.