Kod dan Isyarat AlphaProof: bukti keselamatan kod mesin yang disemak dan andaian yang dipercayai

Apa yang diliputi video ini

• Ejen AI menghasilkan calon bukti; kernel Lean menyemak sama ada mereka menetapkan tuntutan formal yang diluluskan manusia.
• Sasaran yang disahkan adalah pakej CLI libsignal yang dikompilasi tertentu, dengan semantik dan kontrak kriptografi yang dipercayai.
• Membuktikan binari yang dikompilasi mengeluarkan pengkompil Rust daripada asas yang dipercayai untuk sifat-sifat binari yang dinyatakan itu.
• Penyelidik melaporkan dua pengenalan semula secara terasing terhadap pepijat yang telah diperbaiki sebelum ini yang melanggar teorem keselamatan simbolik mereka.
• Pembanding menyemak teorem dan setiap definisi yang bergantung padanya terhadap spesifikasi yang dilindungi dan diluluskan; pindaan melalui proses semakan yang berasingan.

Transkrip terjemahan

Diterjemahkan daripada penceritaan asal Bahasa Inggeris. Audio dan kapsyen yang tersedia dikawal oleh YouTube.

Siapa yang menyemak bukti keselamatan AI?

0:00 Audit keselamatan AI masih kedengaran seperti mempercayai chatbot. Keputusan Signal baharu Google datang dengan bukti matematik sebuah kernel yang berasingan menyemak. Dalam video ini, apa yang dibuktikan oleh Google? Dan bagaimana mereka menghalang ejen daripada mengubah matlamat? Berikut adalah jawapan yang berguna. Model menulis calon bukti, dan Lean menyemak bukti tersebut terhadap sebuah tuntutan yang diluluskan manusia tentang kod yang telah dikompilasi terpilih. Manusia masih memiliki tuntutan dan andaian.

0:21 Anda boleh menyemak hasilnya tanpa mempercayai ucapan kemenangan model. Pemeriksaan berasingan menangkap perubahan soalan secara senyap. Kita akan mengikutinya hingga ke definisi. Hari Selasa, sepuluh November, dan ini The Daily Diff. AlphaProof Code adalah kerangka Google untuk menulis spesifikasi perisian dengan panduan manusia dan menjana bukti yang disemak dengan ejen AI. Kajian ini menyasarkan libsignal, perpustakaan Rust yang melaksanakan protokol pemesejan Signal, di dalam program baris perintah tertentu.

0:45 Google mengumumkan kerja ini hari ini. Kertas kerjanya menyatakan lima penyelidik bekerja selama empat minggu. Ejen menulis bukti, manakala manusia menghabiskan sebahagian besar usaha mereka pada spesifikasi. Keperluan telah menemukan cara untuk menjadi lebih mahal mesyuarat. Spesifikasi menyatakan apa yang program mesti lakukan,

Bagaimana tuntutan menjadi sasaran bukti?

0:59 apa yang dikawal oleh penyerang, dan andaian apa yang diperlukan oleh hujah. Penyemak bertanya sama ada ia menangkap keselamatan yang dipedulikan oleh orang ramai. Jawapan yang disemak dengan indah untuk soalan yang lemah meninggalkan soalan itu utuh. Pasukan ini membina berdasarkan penyelidikan awal mengenai jabat tangan Signal dan ratchetan kunci mesejnya. Analisis formal telah pun mengkaji reka bentuk tersebut. Tuntutan Google menghubungkan hujah keselamatan mereka dengan pelaksanaan yang dikompilasi perpustakaan pengeluaran yang tidak diubah suai, di mana reka bentuk perlu bertahan daripada hubungan dengan kod sebenar. Ketua Pegawai Teknologi Signal, Ehren Kret,

1:27 menerangkan perluasan di luar skop pengesahan yang lebih kecil sebelum ini. Butiran pelaksanaan termasuk tidak mengikut turutan mesej dan sesi yang diarkibkan untuk mesej tertunda. Perisian sebenar menyimpan resit yang dibuang oleh rajah elegan anda. Penyelidik mengkompilasi perpustakaan Rust yang tidak diubah suai dengan pengkompil standard

Mengapa membuktikan binari yang dikompilasi?

1:41 ke dalam boleh laku Arm enam puluh empat Linux. Teorem mereka menggambarkan binari itu menggunakan model arahan formal, merentasi jurang antara kod sumber dan kod mesin yang dioptimumkan. Ralat pengkompil yang melanggar sifat yang dinyatakan akan menjadikan teoremnya palsu. Oleh itu, pengkompil meninggalkan asas yang dipercayai untuk binari ini. Anda masih mempercayai model arahan dan penyemak Lean. Sempadan kepercayaan bergerak, dan ia mempunyai alamat. Kira-kira enam setengah juta baris bukti yang disemak terletak pada kira-kira dua puluh enam

2:06 ribu baris spesifikasi yang dipercayai dan semantik arahan. Ini adalah kiraan artifak. Menganggapnya sebagai skor kecerdasan adalah seperti menilai pembangun berdasarkan saiz folder modul node mereka.

Sifat keselamatan manakah yang bertahan daripada jurang pelaksanaan?

2:16 Hujah-hujah meliputi kerahsiaan dan pengesahan mesej, dengan kerahsiaan ke hadapan dan keselamatan pasca-kompromi di bawah model yang dinyatakan. Dua yang terakhir ini menerangkan had pada kerosakan kunci yang dicuri dan pemulihan selepas pertukaran baharu. Setiap jaminan mempunyai syarat ke atas penyerang dan sesi. Primitif kriptografi berada di belakang kontrak yang dipercayai. Bukti menganggap rutin tersebut berkelakuan seperti yang dinyatakan dan bergantung pada andaian keselamatan kriptografi. Satu bukti mengidealisaikan kriptografi; alasan yang lain mengenai kebarangkalian kejayaan penyerang.

2:42 Kedua-duanya mempunyai sekatan ke atas senario yang mereka liputi. Tanya binaan mana, sifat mana, dan andaian mana. Hasil ini berkaitan dengan pakej baris perintah penyelidik. Pemesejan kumpulan adalah kerja masa depan, dan model komputasi mengecualikan keadaan berbilang peranti. Mengatakan setiap pemasangan Signal bebas pepijat menyimpang dari teorem. Penyelidik memperkenalkan semula dua pepijat Signal yang telah diperbaiki sebelum ini ke dalam

Bolehkah spesifikasi menolak kod yang rosak?

3:02 salinan terasing dan mengkompilasinya. Bukti yang disemak menunjukkan binari tersebut melanggar teorem keselamatan simbolik. Itu menguji sama ada spesifikasi boleh menolak pelaksanaan sebenar yang rosak. Tanda semak hijau anda memerlukan ujian merah. Google menerbitkan spesifikasi dan bukti dengan arahan penyemakan. Repositori menyatakan pembinaan bersih mengambil masa berjam-jam dan memori yang besar. Membaca pengumuman jauh lebih mudah di komputer riba. Model perkakasan dan kontrak yang dipercayai masih memerlukan semakan.

3:26 Saya belum membina semula artifak yang sangat besar ini untuk episod ini. Kami melaporkan hasil yang diterbitkan dan sempadannya. Pihak luar mempunyai laluan untuk memeriksanya, yang lebih penting bagi saya daripada satu lagi pusingan kemenangan AI. Sekarang perangkapnya.

Bolehkah bukti yang betul menjawab soalan yang salah?

3:36 Lean boleh menerima bukti yang betul bagi pernyataan yang hampir tidak meminta apa-apa. Andaian yang mustahil boleh menjadikan teorem tidak bermakna. Mengubah definisi yang terkubur di bawah teorem utama boleh melemahkan matlamat. Kertas kerja ini merancang semakan terhadap ini. Penjaga pintu menyimpan spesifikasi yang diluluskan yang tidak boleh ditulis oleh ejen bukti. Mereka boleh mencadangkan pembetulan melalui proses pindaan yang berasingan. Pelemahan keselamatan ditingkatkan sebagai pepijat berpotensi. Deklarasi kejayaan pembuktian tidak mempunyai kuasa di sini.

4:00 Manusia mengadili perubahan kepada andaian yang dipercayai, secara langsung atau melalui dasar mereka, dan menyemak pindaan selepas setiap kempen. Penilaian pakar tetap bertanggungjawab. Ejen boleh meminta tugasan yang berbeza. Ia tidak boleh memberikan dirinya gred lulus.

Apa yang menangkap perubahan sasaran?

4:13 Berikut adalah semakan yang dijanjikan. Pembanding Lean membandingkan teorem dan setiap definisi yang bergantung padanya dengan salinan yang dilindungi dan diluluskan itu. Ia juga menyemak aksiom yang dibenarkan dan memainkan semula bukti dalam kernel yang baharu. Oleh itu, melemahkan definisi pembantu secara senyap mengubah apa yang sedang dibandingkan. Bukti yang diterima perlu menetapkan sasaran yang diluluskan. Itu masih meninggalkan manusia bertanggungjawab untuk memilih sasaran yang kuat dan andaian yang jujur. Untuk aliran kerja AI anda sendiri, jauhkan kriteria penerimaan di luar

4:37 kebenaran suntingan pekerja dan semak perubahan yang dicadangkan secara berasingan. Hasil Google menjadikan pemisahan itu nyata. Penulis bukti melakukan kerja itu; sempadan penyemakan memutuskan sama ada ia dikira. Jika anda lebih suka membaca ini daripada mendengar saya mengatakannya, diff akan sampai ke peti masuk anda setiap pagi, percuma di daily diff dot dev, pautan di bawah. Jadi keputusan hari ini ialah SHIP IT.

Adakah saya akan melancarkan aliran kerja bukti ini?

4:54 Saya akan melancarkan aliran kerja bukti yang disemak ini kerana tuntutan yang diluluskan kekal berasingan daripada ejen yang menghasilkan jawapan. Saya akan mengekalkan skop dan andaian yang dilampirkan pada setiap hasil. Langgan, tekan loceng, dan beritahu saya di komen jika anda akan mengecopnya secara berbeza. Dan itulah perbezaan untuk hari ini. Saya Niko dari Axrisi. Gabung dengan bertanggungjawab.

Sumber

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