AlphaProof Code and Signal: ellenőrzött gépi kódú biztonsági igazolások és megbízható feltételezések

Amit ez a videó tartalmaz

• Az AI-ügynökök jelölt igazolásokat készítenek; a Lean kernelje ellenőrzi, hogy azok alátámasztják-e az emberi jóváhagyással rendelkező formális állítást.
• Az ellenőrzött cél egy adott lefordított libsignal CLI "heveder", megbízható szemantikával és kriptográfiai szerződésekkel.
• A lefordított bináris bizonyítása eltávolítja a Rust fordítót a megbízható alapból az adott bináris megadott tulajdonságai tekintetében.
• A kutatók két, korábban kijavított hiba elkülönített újra bevezetéséről számolnak be, amelyek sértik a szimbolikus biztonsági tételüket.
• Az összehasonlító ellenőrzi a tételt és minden függő definíciót egy védett, jóváhagyott specifikációval szemben; a módosítások külön felülvizsgálati folyamaton mennek keresztül.

Lefordított átirat

Az eredeti angol narrációból fordítva. A rendelkezésre álló hangot és feliratokat a YouTube vezérli.

Ki ellenőrzi egy AI biztonsági igazolását?

0:00 Egy AI biztonsági audit még mindig úgy hangzik, mint egy chatbotban való bizalom. A Google új Signal eredménye matematikai igazolásokkal érkezik egy külön kernel ellenőrzésekkel. Ebben a videóban mit bizonyított a Google? És hogyan akadályozzák meg, hogy egy ügynök mozgassa a célpontokat? Itt van a hasznos válasz. A modellek jelölt igazolásokat írnak, és a Lean ellenőrzi az igazolásokat egy emberi jóváhagyással rendelkező állítás ellenében, amely kiválasztott fordított kódról szól. Az állítás és a feltételezések továbbra is emberek tulajdonában vannak.

0:21 Ellenőrizheti az eredményt anélkül, hogy hinne a modell győzelmi beszédének. Egy külön ellenőrzés észreveszi a kérdés csendes megváltoztatását. Le fogjuk követni a definíciókig. Kedden, november tizedike van, és ez a The Daily Diff. Az AlphaProof Code a Google keretrendszere szoftverspecifikációk írására emberi útmutatással és ellenőrzött igazolások generálására AI-ügynökökkel. Ez a tanulmány a libsignalt célozza, a Rust könyvtárat, amely a Signal üzenetküldési protokollját valósítja meg egy adott parancssori programban.

0:45 A Google ma jelentette be a munkát. A cikkük szerint öt kutató négy hétig dolgozott. Az ügynökök írták az igazolásokat, míg az emberek legtöbb erőfeszítésüket a specifikációkra fordították. A követelményeknek sikerült még drágább találkozókká válniuk. A specifikáció kimondja, hogy mit kell tennie a programnak,

Hogyan válik egy állítás igazolási céllá?

0:59 mit irányít egy támadó, és mely feltételezésekre van szükség az érveléshez. A felülvizsgálók azt kérdezik, hogy megragadja-e a biztonságot, amelyre az emberek vágynak. Egy gyönyörűen ellenőrzött válasz egy gyenge kérdésre érintetlenül hagyja azt a kérdést. A csapat a Signal kézfogásával és üzenetkulcsos racsnijával kapcsolatos korábbi kutatásokra épít. Formális elemzések már tanulmányozták ezeket a terveket. A Google állítása a biztonsági érvelésüket egy módosítatlan gyártási könyvtár lefordított implementációjához köti, ahol a tervezésnek túl kell élnie a valódi kóddal való érintkezést. A Signal technológiai igazgatója, Ehren Kret,

1:27 a korábbi ellenőrzések kisebb hatókörének kibővítését írja le. Az implementációs részletek közé tartoznak a sorrenden kívüli üzenetek és az archivált munkamenetek a késleltetett üzenetekhez. A valódi szoftver megőrzi azokat a nyugtákat, amelyeket az elegáns diagramja eldobott. A kutatók a módosítatlan Rust könyvtárat a szabványos

Miért kell a lefordított binárist igazolni?

1:41 fordítóval Arm sixty-four Linux futtathatóvá fordítják. Tételeik ezt a binárist formális utasításmodellel írják le, áthidalva a forráskód és az optimalizált gépi kód közötti szakadékot. Egy fordítási hiba, amely megsért egy megadott tulajdonságot, hamissá tenné a tételt. A fordító ezért elhagyja a megbízható alapot ehhez a binárishoz. Továbbra is megbízik az utasításmodellben és a Lean ellenőrzőjében. A bizalmi határ elmozdult, és van címe. Körülbelül hat és fél millió sor ellenőrzött igazolás alapja körülbelül huszonhat

2:06 ezer megbízható specifikációs és utasításszemantikai sor. Ezek műtermék-számok. Intelligencia-pontszámokként kezelni őket olyan, mintha a fejlesztőket a node_modules mappájuk mérete alapján rangsorolnánk.

Mely biztonsági tulajdonságok élték túl az implementációs rést?

2:16 Az érvelések az üzenetek titkosságát és hitelességét fedik le, előrehaladási titkossággal és kompromisszum utáni biztonsággal a megadott modellek szerint. Ez utóbbi kettő a lopott kulcsok okozta károk korlátait és a friss cserék utáni helyreállítást írja le. Minden garancia feltételeket támaszt a támadóra és a munkamenetre. A kriptográfiai primitívek megbízható szerződések mögött állnak. Az igazolás feltételezi, hogy ezek a rutinok a specifikáció szerint viselkednek, és kriptográfiai biztonsági feltételezésekre támaszkodik. Az egyik igazolás idealizálja a kriptográfiát; a másik a támadók siker valószínűségéről érvel.

2:42 Mindkettő korlátozásokat tartalmaz az általa lefedett forgatókönyvekre vonatkozóan. Kérdezze meg, melyik buildről, melyik tulajdonságról és mely feltételezésekről van szó. Ez az eredmény a kutatók parancssori "hevederére" vonatkozik. A csoportos üzenetküldés jövőbeli munka, és a számítási modell kizárja a többeszközös állapotot. Minden Signal telepítés hibamentesnek nevezése túlmegy a tételen. A kutatók két, korábban kijavított Signal hibát vezettek be újra

Visszautasíthatja a specifikáció a hibás kódot?

3:02 izolált másolatokba és lefordították azokat. Az ellenőrzött igazolások kimutatták, hogy ezek a binárisok sértették a szimbolikus biztonsági tételt. Ez azt tesztelte, hogy a specifikáció elutasíthatja-e a valós, hibás implementációkat. A zöld pipának szüksége van egy piros tesztre. A Google közzéteszi a specifikációkat és az igazolásokat ellenőrzési utasításokkal. A tároló szerint egy tiszta build órákat és jelentős memóriát igényel. A bejelentés elolvasása jelentősen könnyebb a laptopon. A hardvermodell és a megbízható szerződések még mindig felülvizsgálatra szorulnak.

3:26 Nem építettem újjá az óriási műterméket ehhez az epizódhoz. A közzétett eredményt és annak határait jelentjük be. A kívülállóknak van módjuk megvizsgálni, ami számomra fontosabb, mint egy újabb AI győzelmi kör. Most jön a csapda.

Válaszolhat-e egy helyes igazolás rossz kérdésre?

3:36 A Lean elfogadhat egy helyes igazolást egy olyan állításról, amely szinte semmit sem kér. Lehetetlen feltételezések üresjáratúvá tehetik a tételt. A címtétel alatt elrejtett definíció megváltoztatása gyengítheti a célt. A tanulmány ellenőrzéseket tervezett ez ellen. A kapuőr egy tárolt, jóváhagyott specifikációt tart fenn, amelyet az igazolási ügynökök nem írhatnak. Javításokat javasolhatnak egy külön módosítási folyamaton keresztül. A biztonsági gyengítést potenciális hibaként kezelik. Az igazoló sikerének deklarációjának nincs itt tekintélye.

4:00 Az emberek bírálják el a megbízható feltételezések változásait, közvetlenül vagy politikájukon keresztül, és felülvizsgálják a módosításokat minden kampány után. A szakértői ítélet marad a horogon. Az ügynök kérhet más feladatot. Nem adhat magának átmenő osztályzatot.

Mi fogja meg a mozgó célpontokat?

4:13 Itt van az ígért ellenőrzés. A Lean összehasonlítója összehasonlítja a tételt és minden definíciót, amelytől függ, azzal a védett, jóváhagyott másolattal. Ellenőrzi az engedélyezett axiómákat is, és új kernelben játssza le az igazolást. Egy segítő definíció csendes gyengítése ezért megváltoztatja az összehasonlított dolgot. Egy elfogadott igazolásnak meg kell alapoznia a jóváhagyott célt. Ez továbbra is az embereket teszi felelőssé az erős cél és az őszinte feltételezések kiválasztásáért. Saját AI munkafolyamatához tartsa az elfogadási kritériumokat a

4:37 dolgozó szerkesztési jogosultságain kívül, és külön vizsgálja felül a javasolt változtatásokat. A Google eredménye ezt a szétválasztást kézzelfoghatóvá teszi. Az igazolásíró végzi a munkát; az ellenőrzési határ dönti el, hogy számít-e. Ha inkább elolvasná ezt, mint hallaná tőlem, a diff minden reggel megérkezik a postaládájába, ingyenesen a daily diff dot dev címen, link lent. Tehát a mai ítélet SHIP IT.

Élesíteném ezt az igazolási munkafolyamatot?

4:54 Én élesíteném ezt az ellenőrzött igazolási munkafolyamatot, mert a jóváhagyott állítás elkülönül attól az ügynöktől, amely a választ adja. Minden eredményhez csatolnám a hatóköröket és a feltételezéseket. Iratkozz fel, nyomd meg a harangot, és írd meg kommentben, ha te másként pecsételted volna. És ez a mai diff. Én Niko vagyok az Axrisi-tól. Merge felelősségteljesen.

Források

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