AlphaProof Code ja Signaal: kontrollitud masinkoodi turvatõestused ja usaldusväärsed eeldused

Mida see video hõlmab

• AI agendid toodavad kandidaattõestusi; Leani kernel kontrollib, kas need kinnitavad inimeste poolt heakskiidetud ametlikku väidet.
• Kontrollitud sihtmärk on konkreetne kompileeritud libsignali CLI rakendus, millel on usaldusväärne semantika ja krüptograafilised lepingud.
• Kompileeritud binaarfaili tõestamine eemaldab Rusti kompilaatori selle binaarfaili deklareeritud omaduste usaldusväärsest baasist.
• Teadlased teatavad kahest isoleeritud varem parandatud vea taastekkest, mis rikuvad nende sümboolset turvalisuse teoreemi.
• Võrdlusvahend kontrollib teoreemi ja iga sõltuvat definitsiooni kaitstud heakskiidetud spetsifikatsiooni suhtes; muudatused läbivad eraldi ülevaadatud protsessi.

Tõlgitud transkriptsioon

Tõlgitud ingliskeelsest originaaljutustusest. Saadaolevat heli ja subtiitreid kontrollib YouTube.

Kes kontrollib AI turvatõestust?

0:00 AI turvaaudit kõlab endiselt nagu vestlusrobotile usaldamine. Google'i uus Signali tulemus sisaldab matemaatilisi tõestusi, mida eraldi kernel kontrollib. Mida Google selles videos tõestas? Ja kuidas nad takistavad agendi väravate liigutamist? Siin on kasulik vastus. Mudelid kirjutavad kandidaattõestusi ja Lean kontrollib tõestusi vastu inimeste poolt heakskiidetud väitele valitud kompileeritud koodi kohta. Inimestele kuuluvad endiselt väited ja eeldused.

0:21 Saate tulemust kontrollida, uskumata mudeli võidukõnesse. Eraldi kontroll tuvastab küsimuse vaikse muutumise. Jälgime seda definitsioonideni. On teisipäev, 10. november ja see on The Daily Diff. AlphaProof Code on Google'i raamistik tarkvara spetsifikatsioonide kirjutamiseks inimjuhendamisega ja kontrollitud tõestuste genereerimiseks AI agentidega. See uuring keskendub libsignalile, Rusti teegile, mis rakendab Signali sõnumside protokolli, konkreetse käsureaprogrammi sees.

0:45 Google teatas tööst täna. Selle artiklis öeldakse, et viis teadlast töötasid neli nädalat. Agendid kirjutasid tõestused, samas kui inimesed kulutasid suurema osa oma jõupingutustest spetsifikatsioonidele. Nõuded on leidnud viisi, kuidas muutuda veelgi kallimateks kohtumisteks. Spetsifikatsioon ütleb, mida programm peab tegema,

Kuidas saab väitest tõestussihik?

0:59 mida ründaja kontrollib ja milliseid eeldusi argument vajab. Arvustajad küsivad, kas see hõlmab turvalisust, millest inimesed hoolivad. Kaunilt kontrollitud vastus nõrgale küsimusele jätab selle küsimuse puutumata. Meeskond tugineb varasematele uuringutele Signali käepigistuse ja selle sõnumivõtme ratšeti kohta. Ametlikud analüüsid on neid disaine juba uurinud. Google'i väide ühendab nende turvalisuse argumendid muutmata tootmise teegi kompileeritud implementatsiooniga, kus disain peab üle elama kokkupuute tegeliku koodiga. Signali tehnoloogiajuht Ehren Kret,

1:27 kirjeldab laienemist varasemate verifitseerimiste väiksematest ulatusest kaugemale. Implementeerimisdetailid hõlmavad järjest väljaspool sõnumeid ja arhiveeritud seansse hilinenud sõnumite jaoks. Tarkvara säilitab tegelikud kviitungid, mille teie elegantne diagramm minema viskas. Teadlased kompileerivad muutmata Rusti teegi standardse

Miks tõestada kompileeritud binaarfaili?

1:41 kompilaatoriga Arm 64-bitise Linuxi käivitatavaks failiks. Nende teoreemid kirjeldavad seda binaarfaili ametliku käskude mudeli abil, ulatudes allika ja optimeeritud masinkoodi vahelisest lüngast üle. Kompilaatori viga, mis rikub deklareeritud omadust, muudaks selle teoreemi valeks. Kompilaator lahkub seega selle binaarfaili usaldusväärsest baasist. Te usaldate endiselt käskude mudelit ja Leani kontrollijat. Usalduspiir liikus ja sellel on aadress. Umbes kuus ja pool miljonit rida kontrollitud tõestust tuginevad ligikaudu kahekümne kuuele

2:06 tuhandele usaldusväärsele spetsifikatsioonile ja käskude semantika ridadele. Need on artefaktide arvud. Nende intelligentsuse skoorideks pidamine on nagu arendajate järjestamine nende node_modules kausta suuruse järgi.

Millised turvaomadused elasid ellu implementeerimislünga?

2:16 Argumendid hõlmavad sõnumite konfidentsiaalsust ja autentimist, ettepoole suunatud saladuse ja kompromissijärgse turvalisusega määratud mudelite alusel. Need kaks viimast kirjeldavad varastatud võtme kahjustuste piiranguid ja taastumist pärast uusi vahetusi. Igal garantiil on tingimused ründajale ja seansile. Krüptograafilised primitiivid asuvad usaldusväärsete lepingute taga. Tõestus eeldab, et need rutiinid käituvad vastavalt spetsifikatsioonile ja tugineb krüptograafilistele turvalisuse eeldustele. Üks tõestus idealiseerib krüptograafiat; teine arutleb ründaja edu tõenäosuste üle.

2:42 Mõlemal on piirangud stsenaariumidele, mida nad hõlmavad. Küsi, milline versioon, milline omadus ja millised eeldused. See tulemus puudutab teadlaste käsurea rakendust. Grupisõnumid on tulevikutöö ja arvutusmudel välistab mitme seadme oleku. Iga Signali installatsiooni veavabaks nimetamine kaldub teoreemist kõrvale. Teadlased taasisesestasid kaks varem parandatud Signali viga

Kas spetsifikatsioon suudab tagasi lükata katkise koodi?

3:02 isoleeritud koopiatele ja kompileerisid need. Kontrollitud tõestused näitasid, et need binaarfailid rikkusid sümboolset turvalisuse teoreemi. See testis, kas spetsifikatsioon suudab tagasi lükata tõelisi katkisi implementatsioone. Teie roheline linnuke vajab punast testi. Google avaldab spetsifikatsioonid ja tõestused koos kontrollimise juhistega. Hoidla ütleb, et puhas kompileerimine võtab tunde ja märkimisväärselt mälu. Teate lugemine on sülearvutil tunduvalt lihtsam. Riistvaramudel ja usaldusväärsed lepingud vajavad endiselt ülevaatamist.

3:26 Ma ei ole selle episoodi jaoks tohutut artefakti uuesti ehitanud. Me kajastame avaldatud tulemust ja selle piire. Välisriikidel on võimalus seda kontrollida, mis on minu jaoks olulisem kui järjekordne AI võidusõit. Nüüd lõks.

Kas korrektne tõestus saab vastata valele küsimusele?

3:36 Lean võib aktsepteerida korrektset tõestust väitele, mis ei nõua peaaegu midagi. Võimatud eeldused võivad teoreemi tühjaks muuta. Peateoreemi all oleva definitsiooni muutmine võib eesmärki nõrgestada. Artikkel kavandab kontrollid selle vastu. Väravahoidja hoiab varjatud heakskiidetud spetsifikatsiooni, mida tõestusagendid ei saa kirjutada. Nad saavad esitada parandusi eraldi muudatusprotsessi kaudu. Turvalisuse nõrgenemine esitatakse potentsiaalse veana. Tõestaja edu deklaratsioonil ei ole siin autoriteeti.

4:00 Inimesed otsustavad usaldusväärsete eelduste muudatusi, otse või oma poliitika kaudu, ja vaatavad muudatused üle pärast iga kampaaniat. Ekspertotsus jääb vastutama. Agent saab taotleda teistsugust ülesannet. See ei saa endale läbimise hinnet anda.

Mis püüab kinni liikuvaid väravaid?

4:13 Siin on lubatud kontroll. Leani võrdlusvahend võrdleb teoreemi ja iga definitsiooni, millest see sõltub, selle kaitstud heakskiidetud koopiaga. See kontrollib ka lubatud aksioome ja kordab tõestust uues kernelis. Abistaja definitsiooni vaikne nõrgestamine muudab seega võrreldavat asja. Aktsepteeritud tõestus peab kinnitama heakskiidetud sihtmärki. See jätab inimestele endiselt vastutuse tugeva sihtmärgi ja ausate eelduste valimise eest. Oma AI töövoo jaoks hoidke vastuvõtukriteeriumid väljaspool

4:37 töötaja redigeerimisõigusi ja vaadake pakutud muudatused eraldi üle. Google'i tulemus muudab selle eraldamise konkreetseks. Tõestuse kirjutaja teeb tööd; kontrollipiir otsustab, kas see arvestatakse. Kui soovite seda pigem lugeda kui mind kuulda rääkimas, siis erinevused jõuavad teie postkasti igal hommikul, tasuta saidil thedailydiff.dev, link allpool. Seega tänane otsus on SHIP IT.

Kas ma võtaksin selle tõestuse töövoo kasutusele?

4:54 Ma võtaksin selle kontrollitud tõestuse töövoo kasutusele, sest heakskiidetud väide jääb eraldi vastuse tootvast agendist. Ma hoiaksime iga tulemusega seotud ulatuse ja eeldused. Tellige, vajutage kella ja öelge mulle kommentaarides, kas oleksite sellele tempeli erinevalt löönud. Ja see ongi tänane erinevus. Olen Niko Axrisist. Ühendage vastutustundlikult.

Allikad

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