AlphaProof Code ja Signal: tarkistetut konekoodin tietoturvatodistukset ja luotetut oletukset

Mitä tämä video käsittelee

• Tekoälyagentit tuottavat ehdokastodisteita; Leanin ydin tarkistaa, täyttävätkö ne ihmisen hyväksymän muodollisen väitteen.
• Varmennettu kohde on tietty käännetty libsignal CLI -komentorivityökalu, jolla on luotettu semantiikka ja kryptografiset sopimukset.
• Käännetyn binäärin todistaminen poistaa Rust-kääntäjän luotetusta peruspaketista kyseisen binäärin ilmoitettujen ominaisuuksien osalta.
• Tutkijat raportoivat kahdesta erillisestä, aiemmin korjattujen virheiden uudelleen tuomisesta, jotka rikkovat heidän symbolista tietoturvalausettaan.
• Vertailija tarkistaa lauseen ja jokaisen riippuvan määritelmän suojattua, hyväksyttyä spesifikaatiota vasten; muutokset käyvät läpi erillisen tarkistetun prosessin.

Käännetty transkriptio

Käännetty alkuperäisestä englanninkielisestä selostuksesta. Käytettävissä olevan äänen ja tekstitysten hallinta tapahtuu YouTuben kautta.

Kuka tarkistaa tekoälyn tietoturvatodisteen?

0:00 Tekoälyn tietoturva-auditoinnit kuulostavat edelleen siltä, kuin luottaisi chattibottiin. Googlen uusi Signal-tulos sisältää matemaattisia todisteita, jotka erillinen kernel tarkistaa. Tässä videossa, mitä Google todisti? Ja miten he estävät agenttia siirtämästä maalitolppia? Tässä on hyödyllinen vastaus. Mallit kirjoittavat ehdokastodisteita, ja Lean tarkistaa todisteet ihmisen hyväksymää väitettä vastaan, joka koskee valittua käännettyä koodia. Ihmiset omistavat edelleen väitteen ja oletukset.

0:21 Voit tarkistaa tuloksen uskomatta mallin voitonpuheeseen. Erillinen tarkistus havaitsee kysymyksen hiljaisen muuttamisen. Seurataan sitä määritelmiin asti. On tiistai, marraskuun kymmenes, ja tämä on The Daily Diff. AlphaProof Code on Googlen kehys ohjelmistospesifikaatioiden kirjoittamiseen ihmisen ohjauksessa ja tarkistettujen todisteiden luomiseen tekoälyagenttien avulla. Tämä tutkimus kohdistuu libsignaliin, Rust-kirjastoon, joka toteuttaa Signalin viestintäprotokollan tietyn komentoriviohjelman sisällä.

0:45 Google julkisti työn tänään. Sen paperi sanoo, että viisi tutkijaa työskenteli yli neljä viikkoa. Agentit kirjoittivat todisteet, kun taas ihmiset käyttivät suurimman osan työajastaan spesifikaatioihin. Vaatimukset ovat löytäneet tavan tulla entistä kalliimmiksi kokouksiksi. Spesifikaatio kertoo, mitä ohjelman on tehtävä,

Miten väitteestä tulee todistuskohde?

0:59 mitä hyökkääjä hallitsee ja mitä oletuksia argumentti tarvitsee. Arvostelijat kysyvät, kattaako se tietoturvan, josta ihmiset välittävät. Kauniisti tarkistettu vastaus heikkoon kysymykseen jättää kysymyksen ennalleen. Tiimi rakentaa aiemman tutkimuksen pohjalta Signalin kättelystä ja sen viestiavaimen räikkämekanismista. Muodolliset analyysit ovat jo tutkineet näitä malleja. Googlen väite yhdistää heidän tietoturva-argumenttinsa muokkaamattoman tuotanto- kirjaston käännettyyn toteutukseen, jossa suunnittelun on kestettävä kosketus todellisen koodin kanssa. Signalin teknologiajohtaja, Ehren Kret,

1:27 kuvailee laajennusta aiemman varmennuksen pienemmistä soveltamisaloista. Toteutuksen yksityiskohdat sisältävät viestien saapumisen väärässä järjestyksessä ja arkistoidut istunnot viivästyneille viesteille. Todellinen ohjelmisto säilyttää kuitit, jotka elegantti kaaviosi heitti pois. Tutkijat kääntävät muokkaamattoman Rust-kirjaston standardi-

Miksi todistaa käännetty binääri?

1:41 kääntäjällä Arm 64 Linux -suorituskelpoiseksi tiedostoksi. Heidän lauseensa kuvaavat binääriä muodollisella ohjemallilla, ulottuen lähdekoodin ja optimoidun konekoodin välisen kuilun yli. Kääntäjän virhe, joka rikkoo ilmoitetun ominaisuuden, tekisi sen lauseesta epätosi. Kääntäjä jättää siksi tämän binäärin luotettavan perustan ulkopuolelle. Luotat edelleen ohjemalliin ja Leanin tarkistajaan. Luottamusraja siirtyi, ja sillä on osoite. Noin kuusi ja puoli miljoonaa riviä tarkistettua todistetta perustuu noin kahdenteenkymmenenteenkuudenteen

2:06 tuhanteen luotettuun spesifikaatio- ja ohje-semantiikkariviin. Nämä ovat artefaktimääriä. Niiden käsittelyä älykkyyspisteinä on kuin kehittäjien rankingia heidän node_modules-kansion koon perusteella.

Mitkä tietoturvaominaisuudet selvisivät toteutuskuilusta?

2:16 Argumentit kattavat viestien luottamuksellisuuden ja aitouden, eteenpäin salassapidon ja kompromissin jälkeisen turvallisuuden ilmoitettujen mallien mukaisesti. Nämä kaksi viimeistä kuvaavat varastettujen avainten aiheuttamien vahinkojen rajoja ja toipumista uusien vaihtojen jälkeen. Jokaisella takuulla on ehdot hyökkääjälle ja istunnolle. Kryptografiset primitiivit ovat luotettujen sopimusten takana. Todiste olettaa, että nämä rutiinit toimivat määritellysti ja tukeutuu kryptografisiin tietoturvaoletuksiin. Yksi todiste idealisoi kryptografiaa; toinen perustelee hyökkääjän onnistumistodennäköisyyksiä.

2:42 Molemmilla on rajoituksia kattamiensa skenaarioiden suhteen. Kysy, mikä versio, mikä ominaisuus ja mitkä oletukset. Tämä tulos koskee tutkijoiden komentorivityökalua. Ryhmäviestintä on tulevaa työtä, ja laskennallinen malli sulkee pois monilaitetilan. Jokaisen Signal-asennuksen kutsuminen virheettömäksi harhautuu lauseen ulkopuolelle. Tutkijat toivat uudelleen kaksi aiemmin korjattua Signal-bugia

Voiko spesifikaatio hylätä rikkinäisen koodin?

3:02 eristettyihin kopioihin ja käänsivät ne. Tarkastetut todisteet osoittivat, että nämä binäärit rikkoivat symbolista tietoturvalausetta. Tämä testasi, voiko spesifikaatio hylätä todellisia rikkinäisiä toteutuksia. Vihreä valintamerkkisi tarvitsee punaisen testin. Google julkaisee spesifikaatiot ja todisteet tarkistusohjeiden kera. Repositoryn mukaan puhdas käännös kestää tunteja ja vaatii huomattavasti muistia. Ilmoituksen lukeminen on huomattavasti helpompaa kannettavalla tietokoneella. Laitteistomalli ja luotetut sopimukset vaativat edelleen tarkistusta.

3:26 En ole rakentanut tätä valtavaa artefaktia uudelleen tätä jaksoa varten. Raportoimme julkaistun tuloksen ja sen rajat. Ulkopuolisilla on mahdollisuus tarkistaa se, mikä on minulle tärkeämpää kuin uusi tekoälyn voitonkierros. Nyt ansa.

Voiko oikea todiste vastata väärään kysymykseen?

3:36 Lean voi hyväksyä oikean todisteen lauseesta, joka pyytää lähes mitään. Mahdottomat oletukset voivat tehdä lauseesta turhan. Pääotsikkolauseen alla olevan määritelmän muuttaminen voi heikentää tavoitetta. Paperi suunnittelee tarkistuksia tätä vastaan. Portinvartija pitää hallussaan hyväksyttyä spesifikaatiota, johon todisteagentit eivät voi kirjoittaa. Ne voivat ehdottaa korjauksia erillisen muutoksenhakuprosessin kautta. Tietoturvan heikentyminen eskaloituu potentiaaliseksi virheeksi. Todistajan menestysjulistuksella ei ole tässä valtuuksia.

4:00 Ihmiset käsittelevät luotettujen oletusten muutoksia, suoraan tai politiikkansa kautta, ja tarkistavat muutokset jokaisen kampanjan jälkeen. Asiantuntijan harkintavalta pysyy vastuussa. Agentti voi pyytää eri tehtävää. Se ei voi antaa itselleen hyväksyttyä arvosanaa.

Mikä havaitsee liikkuvat maalitolpat?

4:13 Tässä on luvattu tarkistus. Leanin vertailija vertaa lausetta ja kaikkia sen riippuvaisia määritelmiä suojattuun hyväksyttyyn kopioon. Se tarkistaa myös sallitut aksioomat ja toistaa todisteen uudessa ytimessä. Apumääritelmän hiljainen heikentäminen muuttaa siis verrattavaa asiaa. Hyväksytyn todisteen on todistettava hyväksytty kohde. Tämä jättää edelleen ihmiset vastuuseen vahvan kohteen ja rehellisten oletusten valinnasta. Omassa tekoälytyönkulussasi pidä hyväksymiskriteerit työntekijän muokkausoikeuksien ulkopuolella ja tarkista ehdotetut muutokset erikseen.

4:37 työntekijän muokkausoikeuksien ulkopuolella ja tarkista ehdotetut muutokset erikseen. Googlen tulos tekee tästä erottelusta konkreettisen. Todisteen kirjoittaja tekee työn; tarkistusraja päättää, lasketaanko se. Jos haluat mieluummin lukea tämän kuin kuulla minun sanovan sen, The Daily Diff saapuu sähköpostiisi joka aamu, ilmaiseksi osoitteessa dailydiff.dev, linkki alla. Joten tämänpäivän tuomio on SHIP IT.

Lähettäisinkö tämän todistustyönkulun?

4:54 Lähettäisin tämän tarkistetun todistuksen työnkulun, koska hyväksytty väite pysyy erillään vastauksen tuottavasta agentista. Pidän soveltamisalan ja oletukset jokaisen tuloksen liitteenä. Tilaa, paina kelloa ja kerro minulle kommenteissa, jos olisit leimannut sen eri tavalla. Ja se on The Daily Diff tänään. Olen Niko Axrisistä. Yhdistä vastuullisesti.

Lähteet

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub