Koda in signal AlphaProof: preverjeni varnostni dokazi strojne kode in zaupanja vredne predpostavke

Kaj zajema ta videoposnetek

• Agenti umetne inteligence izdelujejo kandidate za dokaze; Leanovo jedro preveri, ali ti dokazujejo formalno trditev, ki so jo odobrili ljudje.
• Preverjena tarča je specifično prevedeno orodje v ukazni vrstici libsignal z zaupanja vredno semantiko in kriptografskimi pogodbami.
• Dokazovanje prevedene binarne kode odstrani Rust prevajalnik iz zaupanja vredne osnove za navedene lastnosti te binarne kode.
• Raziskovalci poročajo o dveh izoliranih ponovnih vpeljavah predhodno odpravljenih napak, ki kršijo njihov simbolni varnostni izrek.
• Primerjalnik preveri izrek in vsako odvisno definicijo glede na zaščiteno, odobreno specifikacijo; spremembe gredo skozi ločen pregledan postopek.

Preveden prepis

Prevedeno iz izvirnega angleškega pripovedovanja. Razpoložljivi zvok in podnapisi so nadzorovani s strani YouTuba.

Kdo preveri varnostni dokaz umetne inteligence?

0:00 Varnostna revizija z umetno inteligenco še vedno zveni kot zaupanje klepetalnemu robotu. Googlov novi rezultat za Signal prihaja z matematičnimi dokazi, ki jih ločeno jedro preveri. V tem videu, kaj je Google dokazal? In kako preprečijo agentu, da bi premikal cilje? Tukaj je koristen odgovor. Modeli pišejo kandidate za dokaze, Lean pa preveri dokaze glede na človeško odobreno trditev o izbrani prevedeni kodi. Ljudje še vedno so lastniki trditve in predpostavk.

0:21 Rezultat lahko preverite, ne da bi verjeli zmagoslavnemu govoru modela. Ločena preverka ujame tiho spreminjanje vprašanja. Sledili ji bomo do definicij. Torek, 10. november, in to je The Daily Diff. AlphaProof Code je Googlov okvir za pisanje specifikacij programske opreme z človeškim vodenjem in generiranje preverjenih dokazov z agenti umetne inteligence. Ta študija cilja na libsignal, knjižnico Rust, ki implementira Signalov protokol za sporočanje, znotraj določenega programa ukazne vrstice.

0:45 Google je danes objavil delo. V njihovem prispevku piše, da je pet raziskovalcev delalo več kot štiri tedne. Agenti so napisali dokaze, medtem ko so ljudje večino truda vložili v specifikacije. Zahteve so našle način, da postanejo še dražja srečanja. Specifikacija določa, kaj mora program storiti,

Kako trditev postane tarča dokazovanja?

0:59 kaj nadzoruje napadalec in katere predpostavke argument potrebuje. Recenzenti sprašujejo, ali zajema varnost, ki je ljudem pomembna. Lepo preverjen odgovor na šibko vprašanje pusti to vprašanje nedotaknjeno. Ekipa gradi na prejšnjih raziskavah o rokovanju Signala in njegovi ključni ratchet za sporočila. Formalne analize so že preučevale te zasnove. Googlova trditev povezuje njihove varnostne argumente z nespremenjeno produkcijsko implementacijo knjižnice, kjer mora zasnova preživeti stik z dejansko kodo. Signalov tehnični direktor, Ehren Kret,

1:27 opisuje razširitev onkraj manjših obsegov prejšnjega preverjanja. Podrobnosti implementacije vključujejo neurejena sporočila in arhivirane seje za zamiknjena sporočila. Prava programska oprema hrani potrdila, ki jih je vaš eleganten diagram zavrgel. Raziskovalci prevedejo nespremenjeno knjižnico Rust s standardnim

Zakaj dokazati prevedeno binarno kodo?

1:41 prevajalnikom v izvedljivo datoteko Arm 64 Linux. Njihovi izreki opisujejo to binarno kodo z uporabo formalnega modela navodil, premoščajoč vrzel med izvorno in optimizirano strojno kodo. Napaka prevajalnika, ki krši določeno lastnost, bi naredila njen izrek napačen. Prevajalnik zato zapusti zaupanja vredno bazo za to binarno kodo. Še vedno zaupate modelu navodil in Leanovemu preverjevalniku. Meja zaupanja se je premaknila in ima naslov. Približno šest milijonov in pol vrstic preverjenega dokaza temelji na približno šestindvajset

2:06 tisoč zaupanja vrednih specifikacijskih in semantičnih vrstic navodil. To so števila artefaktov. Obravnavanje le-teh kot inteligentnih rezultatov je kot razvrščanje razvijalcev po velikosti njihove mape modulov node.

Katere varnostne lastnosti so preživele vrzel v implementaciji?

2:16 Argumenti zajemajo zaupnost in avtentikacijo sporočil, z napredno tajnostjo in varnostjo po kompromisu v navedenih modelih. Zadnja dva opisujeta omejitve škode zaradi ukradenih ključev in okrevanja po novih izmenjavah. Vsaka garancija ima pogoje glede napadalca in seje. Kriptografske primitive so za zaupanja vrednimi pogodbami. Dokaz predpostavlja, da te rutine delujejo, kot je določeno, in se zanaša na kriptografske varnostne predpostavke. En dokaz idealizira kriptografijo; drugi razmišlja o verjetnosti uspeha napadalca.

2:42 Oba imata omejitve glede scenarijev, ki jih pokrivata. Vprašajte, katera zgradba, katera lastnost in katere predpostavke. Ta rezultat se nanaša na orodje ukazne vrstice raziskovalcev. Skupinsko sporočanje je prihodnje delo, računski model pa izključuje stanje več naprav. Imenovanje vsake namestitve Signala brez napak je zunaj izreka. Raziskovalci so ponovno uvedli dve predhodno odpravljeni napaki Signala v

Ali lahko specifikacija zavrne pokvarjeno kodo?

3:02 izolirane kopije in jih prevedli. Preverjeni dokazi so pokazali, da so te binarne datoteke kršile simbolni varnostni izrek. To je preverjalo, ali lahko specifikacija zavrne resnične pokvarjene implementacije. Vaš zeleni kljukec potrebuje rdeči test. Google objavlja specifikacije in dokaze z navodili za preverjanje. Skladišče pravi, da čista zgradba traja ure in precej pomnilnika. Branje objave je precej lažje na prenosniku. Model strojne opreme in zaupanja vredne pogodbe še vedno potrebujejo pregled.

3:26 Za to epizodo nisem ponovno zgradil ogromnega artefakta. Poročamo o objavljenem rezultatu in njegovih mejah. Zunanji imajo pot do vpogleda, kar mi je pomembneje kot še en krog zmage AI. Zdaj past.

Ali lahko pravilen dokaz odgovori na napačno vprašanje?

3:36 Lean lahko sprejme pravilen dokaz trditve, ki ne zahteva skoraj ničesar. Nemogoče predpostavke lahko naredijo izrek praznega. Sprememba definicije, zakopane pod naslovnim izrekom, lahko oslabi cilj. Prispevek določa preglede proti temu. Vratar hrani shranjeno odobreno specifikacijo, v katero agenti za dokazovanje ne morejo pisati. Predlagajo lahko popravke prek ločenega postopka sprememb. Oslabitev varnosti se obravnava kot potencialna napaka. Izjavlja o uspehu preverjalca nima tukaj nobene avtoritete.

4:00 Ljudje presojajo spremembe zaupanja vrednih predpostavk, neposredno ali prek svoje politike, in pregledujejo spremembe po vsaki kampanji. Strokovna presoja ostaja odgovorna. Agent lahko zahteva drugačno nalogo. Ne more si dati prehodne ocene.

Kaj ujame premikajoče se cilje?

4:13 Tukaj je obljubljena preverka. Leanov primerjalnik primerja izrek in vsako definicijo, od katere je odvisen, z zaščiteno odobreno kopijo. Preverja tudi dovoljene aksiome in ponovno predvaja dokaz v svežem jedru. Tiho oslabitev pomožne definicije torej spremeni stvar, ki se primerja. Sprejet dokaz mora potrditi odobreno tarčo. To še vedno pušča ljudi odgovorne za izbiro močne tarče in poštenih predpostavk. Za lasten delovni tok AI, hranite merila sprejemljivosti zunaj

4:37 dovoljenj za urejanje delavca in ločeno preglejte predlagane spremembe. Googlov rezultat to ločitev konkretizira. Pisec dokazov opravi delo; meja preverjanja odloča, ali se to upošteva. Če bi raje prebrali to, kot pa slišali, kako to govorim, se diff prikaže v vašem nabiralniku vsako jutro, brezplačno na daily diff dot dev, povezava spodaj. Torej, današnja sodba je SHIP IT.

Ali bi poslal ta delovni tok dokazovanja?

4:54 Poslal bi ta potrjen delovni tok dokazovanja, ker odobrena trditev ostaja ločena od agenta, ki proizvaja odgovor. Obdržal bi obseg in predpostavke, priložene vsakemu rezultatu. Naročite se, kliknite zvonec in mi v komentarjih povejte, če bi to žigosali drugače. In to je diff za danes. Sem Niko iz Axrisija. Združujte odgovorno.

Viri

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