AlphaProof Code and Signal: sinuring mga patunay sa seguridad ng machine-code at pinagkakatiwalaang mga pagpapalagay

Ang sakop ng video na ito

• Ang mga AI agent ay gumagawa ng mga kandidatong patunay; sinusuri ng kernel ng Lean kung itinatag nila ang aprubadong pormal na claim ng tao.
• Ang na-verify na target ay isang partikular na naipon na libsignal CLI harness, na may pinagkakatiwalaang semantika at cryptographic na kontrata.
• Ang pagpapatunay sa naipon na binary ay nag-aalis sa Rust compiler mula sa pinagkakatiwalaang base para sa mga nakasaad na katangian ng binary na iyon.
• Iniulat ng mga mananaliksik ang dalawang nakahiwalay na muling pagpapakilala ng mga dati nang naayos na bug na lumalabag sa kanilang simbolikong teorama ng seguridad.
• Sinusuri ng comparator ang teorama at bawat nakadepende na kahulugan laban sa isang protektadong aprubadong pagtutukoy; ang mga pagbabago ay dumadaan sa isang hiwalay na proseso na sinuri.

Isinaling transcript

Isinalin mula sa orihinal na salaysay sa English. Ang available na audio at mga caption ay kinokontrol ng YouTube.

Sino ang sumusuri sa isang AI security proof?

0:00 Ang isang AI security audit ay parang pagtitiwala pa rin sa isang chatbot. Ang bagong resulta ng Signal ng Google ay may mga mathematical proofs na isang hiwalay na kernel sinusuri. Sa video na ito, ano ang pinatunayan ng Google? At paano nila pinipigilan ang isang agent na baguhin ang layunin? Narito ang kapaki-pakinabang na sagot. Ang mga modelo ay sumusulat ng mga kandidatong patunay, at sinusuri ng Lean ang mga patunay laban sa isang claim na aprubado ng tao tungkol sa mga napiling compiled code. Ang mga tao pa rin ang nagmamay-ari ng claim at mga pagpapalagay.

0:21 Maaari mong suriin ang resulta nang hindi naniniwala sa victory speech ng modelo. Isang hiwalay na tseke ang nakakahuli sa tahimik na pagbabago ng tanong. Susundan natin ito hanggang sa mga kahulugan. Martes, Nobyembre sampu, at ito ang The Daily Diff. Ang AlphaProof Code ay ang framework ng Google para sa pagsulat ng mga software specification na may gabay ng tao at pagbuo ng mga checked proof gamit ang mga AI agent. Ang pag-aaral na ito ay nagta-target ng libsignal, ang Rust library na nagpapatupad ng messaging protocol ng Signal, sa loob ng isang partikular na command-line program.

0:45 Inanunsyo ng Google ang gawaing ito ngayon. Sinasabi sa papel nito na limang mananaliksik ang nagtrabaho nang mahigit apat na linggo. Ang mga ahente ang sumulat ng mga patunay, habang ang mga tao ay gumugol ng karamihan ng kanilang pagsisikap sa mga pagtutukoy. Nakahanap ng paraan ang mga kinakailangan upang maging mas mahal na mga pulong. Sinasabi ng pagtutukoy kung ano ang dapat gawin ng programa,

Paano nagiging proof target ang isang claim?

0:59 kung ano ang kontrolado ng isang umaatake, at kung anong mga pagpapalagay ang kailangan ng argumento. Tinatanong ng mga tagasuri kung nakuha nito ang seguridad na pinapahalagahan ng mga tao. Ang isang napakagandang nasuri na sagot sa isang mahinang tanong ay nag-iiwan ng tanong na iyon nang buo. Ang team ay bumubuo sa mas maagang pananaliksik sa handshake ng Signal at sa message-key ratchet nito. Pormal nang sinuri ang mga disenyo na iyon. Kinokonekta ng claim ng Google ang kanilang mga argumento sa seguridad sa isang hindi binagong production na pagpapatupad ng library na na-compile, kung saan ang disenyo ay dapat makaligtas sa pakikipag-ugnayan sa aktwal na code. Inilarawan ni Ehren Kret, chief technology officer ng Signal,

1:27 ang isang pagpapalawak na lampas sa mas maliliit na saklaw ng naunang beripikasyon. Kasama sa mga detalye ng pagpapatupad ang out-of-order na mga mensahe at naka-archive na mga sesyon para sa mga naantalang mensahe. Ang tunay na software ay nagtatago ng mga resibo na itinapon ng iyong eleganteng diagram. Kinompile ng mga mananaliksik ang hindi binagong Rust library gamit ang standard

Bakit dapat patunayan ang compiled binary?

1:41 na compiler sa isang Arm sixty-four Linux executable. Inilalarawan ng kanilang mga teorama ang binary na iyon gamit ang isang pormal na modelo ng instruksyon, na umaabot sa pagitan ng source at optimized machine code. Ang isang error sa compiler na sumisira sa isang nakasaad na property ay gagawing mali ang teorama nito. Samakatuwid, iniiwan ng compiler ang pinagkakatiwalaang base para sa binary na ito. Pinagkakatiwalaan mo pa rin ang instruction model at ang checker ng Lean. Ang hangganan ng tiwala ay gumalaw, at mayroon itong address. Mga anim at kalahating milyong linya ng nasuri na patunay ang nakasalalay sa humigit-kumulang dalawampu't anim na

2:06 libong pinagkakatiwalaang pagtutukoy at mga linya ng semantika ng instruksyon. Ito ay mga bilang ng artifact. Ang pagtrato sa kanila bilang mga marka ng katalinuhan ay parang pagraranggo ng mga developer ayon sa laki ng kanilang node modules folder.

Aling mga katangian ng seguridad ang nakaligtas sa puwang ng implementasyon?

2:16 Sinasaklaw ng mga argumento ang pagiging kumpidensyal ng mensahe at pagpapatunay, na may forward secrecy at post-compromise security sa ilalim ng mga nakasaad na modelo. Ang huling dalawang ito ay naglalarawan ng mga limitasyon sa pinsala ng ninakaw na susi at pagbawi pagkatapos ng mga sariwang palitan. Ang bawat garantiya ay may mga kondisyon sa umaatake at sesyon. Ang mga cryptographic primitive ay nasa likod ng pinagkakatiwalaang kontrata. Ipinapalagay ng patunay na ang mga routine na iyon ay kumilos ayon sa tinukoy at umaasa sa mga cryptographic na pagpapalagay ng seguridad. Ang isang patunay ay idealizes cryptography; ang isa ay nagbibigay-katwiran tungkol sa mga probabilidad ng tagumpay ng umaatake.

2:42 Parehong may mga paghihigpit sa mga sitwasyon na kanilang sinasaklaw. Tanungin kung aling build, aling property, at aling mga pagpapalagay. Ang resultang ito ay tungkol sa command-line harness ng mga mananaliksik. Ang pagmemensahe ng grupo ay gawain sa hinaharap, at ang computational model ay nagbubukod ng multi-device state. Ang pagtawag sa bawat pag-install ng Signal na walang bug ay naliligaw sa labas ng teorama. Muling ipinakilala ng mga mananaliksik ang dalawang dati nang naayos na bug ng Signal sa

Maaari bang tanggihan ng pagtutukoy ang sirang code?

3:02 nakahiwalay na kopya at kinompile ang mga ito. Ang mga nasuri na patunay ay nagpakita na ang mga binary na iyon ay lumabag sa simbolikong teorama ng seguridad. Sinubukan nito kung ang pagtutukoy ay maaaring tumanggi sa mga totoong sirang implementasyon. Ang iyong berdeng checkmark ay nangangailangan ng pulang pagsubok. Inilalathala ng Google ang mga pagtutukoy at patunay na may mga tagubilin sa pagsusuri. Sinasabi ng repository na ang isang malinis na build ay tumatagal ng mga oras at malaking memorya. Ang pagbasa ng anunsyo ay mas madali sa laptop. Ang hardware model at pinagkakatiwalaang kontrata ay nangangailangan pa rin ng pagsusuri.

3:26 Hindi ko pa muling binuo ang napakalaking artifact para sa episode na ito. Iniulat namin ang nailathala na resulta at ang mga hangganan nito. May paraan ang mga tagalabas upang suriin ito, na mas mahalaga sa akin kaysa sa isa pang AI na victory lap. Ngayon ang bitag.

Maaari bang sagutin ng tamang patunay ang maling tanong?

3:36 Maaaring tanggapin ng Lean ang tamang patunay ng isang pahayag na halos walang hinihingi. Maaaring gawing walang saysay ng imposibleng pagpapalagay ang isang teorama. Ang pagbabago ng isang kahulugan na nakabaon sa ilalim ng pangunahing teorama ay maaaring magpahina sa layunin. Dinisenyo ng papel ang mga pagsusuri laban dito. Ang gatekeeper ay nagtatago ng isang pinigil na aprubadong pagtutukoy na hindi maaaring isulat ng mga ahente ng patunay. Maaari silang magmungkahi ng mga pagwawasto sa pamamagitan ng isang hiwalay na proseso ng pagbabago. Ang paghina ng seguridad ay iniiskal bilang isang potensyal na bug. Walang awtoridad ang deklarasyon ng tagapagpatunay ng tagumpay dito.

4:00 Ang mga tao ang nagpapasya sa mga pagbabago sa pinagkakatiwalaang pagpapalagay, direkta o sa pamamagitan ng kanilang patakaran, at sinusuri ang mga pagbabago pagkatapos ng bawat kampanya. Mananatili ang responsibilidad ng dalubhasang paghuhusga. Maaaring humiling ang ahente ng ibang assignment. Hindi nito maaaring bigyan ang sarili ng passing grade.

Ano ang nakakahuli sa nagbabagong layunin?

4:13 Narito ang ipinangakong tseke. Kinokompara ng comparator ng Lean ang teorama at bawat depinisyon na nakadepende dito sa na protektado at aprubadong kopya. Sinusuri din nito ang mga pinapayagan na axiom at nire-replay ang patunay sa isang bagong kernel. Ang tahimik na pagpapahina ng isang kahulugan ng katulong ay samakatuwid ay nagbabago ng bagay na ikinumpara. Ang isang tinanggap na patunay ay dapat magtatag ng aprubadong target. Nag-iiwan pa rin iyon sa mga tao na responsable sa pagpili ng isang matibay na target at tapat na mga pagpapalagay. Para sa iyong sariling AI workflow, panatilihin ang mga pamantayan ng pagtanggap sa labas ng

4:37 mga pahintulot sa pag-edit ng manggagawa at suriin ang mga iminungkahing pagbabago nang hiwalay. Pinapatunayan ng resulta ng Google ang paghihiwalay na iyon. Ang sumusulat ng patunay ang gumagawa ng trabaho; ang checking boundary ang nagpapasya kung ito ay mahalaga. Kung mas gusto mong basahin ito kaysa pakinggan akong sabihin, ang diff ay dumarating sa iyong inbox bawat umaga, libre sa the daily diff dot dev, link sa ibaba. Kaya ang hatol ngayon ay SHIP IT.

Ipapadala ko ba ang proof workflow na ito?

4:54 Ipapadala ko ang workflow na ito na may nasuri na patunay dahil ang naaprubahang claim ay nananatiling hiwalay sa ahente na gumagawa ng sagot. Pananatilihin ko ang saklaw at mga pagpapalagay na nakakabit sa bawat resulta. Mag-subscribe, pindutin ang bell, at sabihin sa akin sa mga komento kung naiiba mo itong tinatakan. At iyon ang diff para ngayon. Ako si Niko mula sa Axrisi. Mag-merge nang may pananagutan.

Mga Pinagmulan

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