AlphaProof Code ve Signal: makine tarafından kontrol edilen kod güvenlik kanıtları ve güvenilen varsayımlar

Bu video neleri kapsar

• Yapay zeka ajanları aday kanıtlar üretir; Lean'in çekirdeği, insan tarafından onaylanmış resmi iddiayı destekleyip desteklemediklerini kontrol eder.
• Doğrulanmış hedef, güvenilir semantik ve kriptografik sözleşmelerle derlenmiş belirli bir libsignal CLI donanımıdır.
• Derlenmiş ikiliyi kanıtlamak, Rust derleyicisini o ikilinin belirtilen özellikleri için güvenilen temelden çıkarır.
• Araştırmacılar, sembolik güvenlik teoremlerini ihlal eden, daha önce düzeltilmiş hataların iki izole yeniden tanıtımını rapor eder.
• Karşılaştırıcı, teoremi ve her bağımlı tanımı korunan onaylanmış bir spesifikasyona karşı kontrol eder; değişiklikler ayrı bir incelenen süreçten geçer.

Çevrilmiş deşifre

Orijinal İngilizce anlatımdan çevrilmiştir. Mevcut ses ve altyazılar YouTube tarafından kontrol edilir.

Yapay zeka güvenlik kanıtını kim kontrol eder?

0:00 Bir yapay zeka güvenlik denetimi hala bir sohbet robotuna güvenmek gibi geliyor. Google'ın yeni Signal sonucu, ayrı bir çekirdek tarafından matematiksel kanıtlarla birlikte geliyor kontrol eder. Bu videoda Google neyi kanıtladı? Ve bir ajanın hedefleri değiştirmesini nasıl engellerler? İşte faydalı cevap. Modeller aday kanıtlar yazar ve Lean, kanıtları bir insan tarafından onaylanmış, seçili derlenmiş kod hakkındaki iddiaya karşı kontrol eder. İnsanlar hala iddia ve varsayımların sahibidir.

0:21 Modelin zafer konuşmasına inanmadan sonucu kontrol edebilirsiniz. Ayrı bir kontrol, sessizce değişen soruyu yakalar. Tanımlara kadar takip edeceğiz. Salı, on Kasım ve bu The Daily Diff. AlphaProof Code, Google'ın yazılım spesifikasyonlarını insan rehberliğiyle yazmak ve yapay zeka ajanlarıyla kontrol edilmiş kanıtlar üretmek için çerçevesidir. Bu çalışma, Signal'in mesajlaşma protokolünü uygulayan Rust kütüphanesi libsignal'ı, belirli bir komut satırı programı içinde hedefler. içinde hedefler.

0:45 Google çalışmayı bugün duyurdu. Makalesi, beş araştırmacının dört hafta boyunca çalıştığını söylüyor. Ajanlar kanıtları yazarken, insanlar çabalarının çoğunu spesifikasyonlara harcadı. Gereksinimler daha da pahalı toplantılar haline gelmenin bir yolunu buldu. toplantılar. Spesifikasyon, programın ne yapması gerektiğini,

Bir iddia nasıl bir kanıt hedefi haline gelir?

0:59 bir saldırganın neyi kontrol ettiğini ve argümanın hangi varsayımlara ihtiyaç duyduğunu söyler. İncelemeciler, güvenliği insanların önemsediği şekilde yakalayıp yakalamadığını sorar. Zayıf bir soruya harika bir şekilde kontrol edilmiş bir cevap, o soruyu olduğu gibi bırakır. Ekip, Signal'in el sıkışması ve mesaj anahtarı cırcırına ilişkin önceki araştırmalara dayanmaktadır. cırcırı. Resmi analizler zaten bu tasarımları incelemişti. Google'ın iddiası, güvenlik argümanlarını değiştirilmemiş bir üretim kütüphanesinin derlenmiş uygulamasına bağlar, burada tasarım gerçek kodla temasla hayatta kalmak zorundadır. gerçek kodla temasla hayatta kalmak zorundadır. Signal'in baş teknoloji sorumlusu Ehren Kret,

1:27 daha önceki doğrulamaların daha küçük kapsamlarının ötesinde bir genişlemeyi tanımlıyor. Uygulama detayları arasında sırasız mesajlar ve gecikmeli mesajlar için arşivlenmiş oturumlar bulunur. gecikmeli mesajlar. Gerçek yazılım, zarif diyagramınızın attığı makbuzları saklar. attığı makbuzları saklar. Araştırmacılar, değiştirilmemiş Rust kütüphanesini standart

Derlenmiş ikiliyi neden kanıtlamalıyız?

1:41 derleyici ile Arm altmış dört Linux yürütülebilir dosyasına derler. Teoremleri, bu ikiliyi resmi bir talimat modeli kullanarak tanımlar, kaynak ve optimize edilmiş makine kodu arasındaki boşluğu aşarak. Belirtilen bir özelliği bozan bir derleyici hatası, teoremini yanlış yapardı. Bu nedenle derleyici, bu ikili için güvenilen temeli terk eder. Yine de talimat modeline ve Lean'in denetleyicisine güvenirsiniz. Güven sınırı değişti ve bir adresi var. Yaklaşık altı buçuk milyon satır kontrol edilmiş kanıt, yaklaşık yirmi altı bin güvenilen spesifikasyon ve talimat-semantik satırına dayanır.

2:06 bin güvenilen spesifikasyon ve talimat-semantik satırına dayanır. Bunlar yapıt sayılarıdır. Bunları zeka puanı olarak değerlendirmek, geliştiricileri node_modules klasörlerinin boyutuna göre sıralamak gibidir. klasörlerinin boyutuna göre sıralamak gibidir.

Uygulama boşluğunu hangi güvenlik özellikleri atlattı?

2:16 Argümanlar, belirtilen modeller altında ileri gizlilik ve uzlaşma sonrası güvenlik ile mesaj gizliliğini ve kimlik doğrulamasını kapsar. ile mesaj gizliliğini ve kimlik doğrulamasını kapsar. Bu son ikisi, çalınan anahtar hasarı ve yeni değişimlerden sonra kurtarma üzerindeki limitleri tanımlar. değişimlerden sonra kurtarma üzerindeki limitleri tanımlar. Her garantinin saldırgan ve oturum üzerinde koşulları vardır. Kriptografik ilkel öğeler güvenilen sözleşmelerin arkasındadır. Kanıt, bu rutinlerin belirtildiği gibi davrandığını varsayar ve kriptografik güvenlik varsayımlarına dayanır. güvenlik varsayımlarına dayanır. Biri kriptografiyi idealleştirir; diğeri saldırganın başarı olasılıkları hakkında akıl yürütür. olasılıkları hakkında akıl yürütür.

2:42 Her ikisinin de kapsadıkları senaryolarda kısıtlamaları vardır. Hangi derleme, hangi özellik ve hangi varsayımlar diye sorun. Bu sonuç, araştırmacıların komut satırı donanımını ilgilendiriyor. Grup mesajlaşma gelecekteki bir çalışmadır ve hesaplamalı model çoklu cihaz durumunu hariç tutar. çoklu cihaz durumunu hariç tutar. Her Signal kurulumunu hatasız olarak adlandırmak teoremin dışına çıkar. teoremin dışına çıkar. Araştırmacılar, daha önce düzeltilmiş iki Signal hatasını izole kopyalara yeniden tanıttı ve derledi.

Spesifikasyon bozuk kodu reddedebilir mi?

3:02 izole kopyalara yeniden tanıttı ve derledi. Kontrol edilen kanıtlar, bu ikililerin sembolik güvenlik teoremini ihlal ettiğini gösterdi. Bu, spesifikasyonun gerçek bozuk uygulamaları reddedip reddedemeyeceğini test etti. Yeşil onay işaretinizin kırmızı bir teste ihtiyacı var. Google, spesifikasyonları ve kanıtları kontrol talimatlarıyla yayınlar. Depo, temiz bir derlemenin saatler ve önemli miktarda bellek gerektirdiğini söylüyor. Duyuruyu okumak dizüstü bilgisayarda oldukça kolaydır. Donanım modeli ve güvenilen sözleşmeler hala inceleme gerektiriyor.

3:26 Bu bölüm için devasa yapıtı yeniden inşa etmedim. Yayınlanmış sonucu ve sınırlarını rapor ediyoruz. Dışarıdakilerin bunu incelemesi için bir yol var, bu benim için başka bir yapay zeka zafer turundan daha önemli. zafer turundan daha önemli. Şimdi tuzak.

Doğru bir kanıt yanlış soruyu cevaplayabilir mi?

3:36 Lean, neredeyse hiçbir şey istemeyen bir ifadenin doğru bir kanıtını kabul edebilir. İmkansız varsayımlar bir teoremi boş hale getirebilir. Başlık teoreminin altında gömülü bir tanımı değiştirmek, hedefi zayıflatabilir. hedefi zayıflatabilir. Makale buna karşı kontroller tasarlar. Kapı bekçisi, kanıt ajanlarının yazamayacağı, tutulan onaylanmış bir spesifikasyon tutar. yazamayacağı. Ayrı bir düzeltme süreciyle düzeltmeler önerebilirler. Güvenlik zayıflaması potansiyel bir hata olarak yükseltilir. Kanıtlayıcının başarı beyanının burada yetkisi yoktur.

4:00 İnsanlar güvenilen varsayımlardaki değişiklikleri karara bağlar, doğrudan veya politikaları aracılığıyla ve her kampanyadan sonra değişiklikleri inceler. Uzman yargısı sorumlu kalır. Ajan farklı bir görevlendirme talep edebilir. Kendine geçer not veremez.

Hareket eden hedefleri ne yakalar?

4:13 İşte vaat edilen kontrol. Lean'in karşılaştırıcısı, teoremi ve bağımlı olduğu her tanımı, korunan onaylanmış kopyayla karşılaştırır. ile o korunan onaylanmış kopyayla karşılaştırır. Ayrıca izin verilen aksiyomları kontrol eder ve kanıtı yeni bir çekirdekte tekrar oynatır. Yardımcı bir tanımı sessizce zayıflatmak, karşılaştırılan şeyi değiştirir. karşılaştırılan şeyi değiştirir. Kabul edilmiş bir kanıtın onaylanmış hedefi sağlaması gerekir. Bu, güçlü bir hedef seçme ve dürüst varsayımlar belirleme sorumluluğunu hala insanlara bırakır. varsayımlar. Kendi yapay zeka iş akışınız için, kabul kriterlerini çalışanın düzenleme izinlerinin dışında tutun ve önerilen değişiklikleri ayrı ayrı inceleyin.

4:37 düzenleme izinlerinin dışında tutun ve önerilen değişiklikleri ayrı ayrı inceleyin. Google'ın sonucu bu ayrımı somutlaştırır. Kanıt yazarı işi yapar; kontrol sınırı bunun sayılıp sayılmadığına karar verir. Bunu benden duymak yerine okumak isterseniz, diff her sabah ücretsiz olarak e-posta kutunuza düşer, her sabah, daily diff dot dev'den ücretsiz, bağlantı aşağıda. Bu nedenle bugünün kararı SHIP IT.

Bu kanıt iş akışını gönderir miydim?

4:54 Bu kontrol edilmiş kanıt iş akışını gönderirdim çünkü onaylanmış iddia, cevabı üreten ajandan ayrı kalır. cevabı üreten ajandan ayrı kalır. Her sonuca kapsamı ve varsayımları ekli tutardım. Abone olun, zili çalın ve farklı bir şekilde damgalayıp damgalamayacağınızı yorumlarda bana bildirin. farklı bir şekilde. Ve bugünün diff'i bu kadar. Ben Axrisi'den Niko. Sorumlu bir şekilde birleştirin.

Kaynaklar

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