Gervigreind Google DeepMind sannar dulkóðunaröryggi Signal

Vísindamenn hjá Google DeepMind, Alphabet Inc. ↘ 0.21%, notuðu nýtt gervigreindarkerfi sem kallast AlphaProof Code til að sanna stærðfræðilega nokkrar af helstu dulkóðunartryggingum Signal samskiptareglunnar. Fjögurra vikna tilraunaverkefnið fann engar nýjar veikleika í þeim hlutum samskiptareglunnar sem skoðaðir voru, að því er WIRED greindi frá þann 10. nóvember.wired.com

Niðurstaðan skiptir máli fyrir fleiri en bara Signal forritið. Samskiptareglan tryggir einnig skilaboð í Google Messages og WhatsApp hjá Meta Platforms, Inc. ↗ 0.22%, svo greiningin bætir við enn einni óháðu athuguninni á dulkóðun sem verndar stóran hluta samskipta heimsins, samkvæmt WIRED. Hún sýnir einnig að gervigreind getur stytt formlega sannprófun, sem er lengi eftirsótt en hæg leið til að nota stærðfræði til að sýna fram á að hugbúnaður hegði sér eins og til er ætlast.wired.com

Hvað greiningin leiddi í ljós

Vísindamennirnir prófuðu AlphaProof Code á eldri útgáfum af Signal sem innihéldu þekkta veikleika, sem allir voru lagaðir fyrir löngu. Tólið fann þessa galla réttilega og sýndi fram á að ekki var hægt að sannprófa þær útgáfur formlega, að því er WIRED greindi frá. DeepMind er að birta forskriftina og sönnunina sem þeir smíðuðu svo önnur sannprófunarverkefni geti nýtt sér þær.wired.com

Sviðið var takmarkað. Vinnan sannprófaði ekki allt farsímaforrit Signal og vísindamennirnir lýstu þessu sem einum áfanga í lengra ferli. "Við erum mjög spennt fyrir þessari niðurstöðu, en það er langt í land áður en við getum stækkað þetta yfir í allan hugbúnað heimsins, og við viljum gera það," sagði Swarat Chaudhuri, rannsóknarvísindamaður hjá DeepMind, við WIRED.wired.com

Liðið sagði að fyrri formleg sannprófunarvinna hjá Signal hefði gefið þeim forskot. "Þótt fyrri formleg sannprófun hafi beinst að smærri hlutum kóðans, gerir nálgun Google DeepMind kleift að stækka verulega," sagði Ehren Kret, tæknistjóri Signal, í yfirlýsingu og bætti við að sannprófunin veiti fyrirtækinu "enn meira öryggi" eftir því sem öryggisógnir tengdar gervigreind aukast.wired.com

Fjölmennt svið

Vinna DeepMind kemur á sama tíma og aðrir hópar stefna að svipuðum markmiðum. Í apríl 2026 hófu Signal, Beneficial AI Foundation og Lean FRO verkefnið Signal Shot, sem er opinbert átak til að sannprófa Signal samskiptaregluna og Rust útfærslu hennar með Lean sönnunaraðstoðarmanninum. Verkefnið miðar að því að þýða raunverulegan kóða Signal yfir í Lean og sanna að hann passi við sannprófað líkan af samskiptareglunni, samkvæmt stofnuninni. Niðurstaða DeepMind er aðskilin frá því verkefni, benti Startup Fortune á.beneficialaifoundation.org+2

Opnar spurningar um kostnað

Enn er óljóst hvort gervigreindarsjálfvirk sannprófun geti skilað árangri með viðráðanlegum kostnaði. DeepMind vann Signal-greininguna ókeypis sem rannsóknarverkefni. Google neitaði að gefa upp hvað það kostaði eða hvort þeir hyggist bjóða upp á viðskiptalega sannprófunarvöru, að því er WIRED greindi frá.wired.com

Chaudhuri sagði að lykilframfarir hafi verið ferli þar sem gervigreind leggur sitt af mörkum og lagfærir eigin vinnu á meðan menn fara yfir hana á mikilvægum stigum. "Við viljum ekki þennan heim þar sem gervigreind býr til markmiðin og gervigreind býr til sannanirnar og tekur í raun próf sem eru sjálfskrifuð," sagði hann. "Það er millivegur."wired.com