Signal şifrelemesi, yapay zekânın 6,5 milyon satırlık ispatını geçti

Signal’ın şifreleme kodu artık yaygın kullanılan yazılımların neredeyse hiçbirinin sahip olmadığını iddia edebileceği bir şeye sahip: vaat ettiğini yaptığını gösteren matematiksel bir kanıt. Bir yapay zekâ ajanları ekibi, Signal protokolünü çalıştıran kütüphane libsignal üzerinde çalışarak bire bir sohbetlerin gizli kaldığını, karşı tarafın kimliğini doğruladığını ve bir anahtar çalındıktan sonra saldırganı yeniden dışarıda bıraktığını kanıtladı. Yeni bir güvenlik açığı bulmadılar.

Bu gelişme, Signal kullanıcılarının çok ötesinde önem taşıyor. Protokol, uçtan uca şifreli mesajlaşmanın dünya çapındaki standardı; farklı sürümleri WhatsApp, Messenger ve Google Messages’taki sohbetleri koruyor. Gerçekten kullanıma sunulmuş kodu bu derinlikte incelemek bugüne kadar o kadar yavaştı ki bunu neredeyse kimse denemiyordu: Alanın en büyük başarılarından biri olan, doğrulanmış bir işletim sistemi çekirdeği için yirmi kişi-yıl harcanmıştı. Bu çalışma ise dört haftada tamamlandı.

Google DeepMind tarafından geliştirilen aracın adı AlphaProof Code. Önce insan uzmanlar ve yapay zekâ modelleri, Signal’in güvenlik hedeflerini matematiksel kanıtlar için geliştirilmiş bir programlama dili olan Lean’de biçimsel ifadelere dönüştürdü; her birini de bir kişi gözden geçirdi. Ardından Gemini Carbon ile çalışan 40 ila 80 ajandan oluşan ekipler kanıtları yazdı. Tek bir makinede, her seferinde 24 ila 72 saat boyunca çalıştılar. Ortaya yaklaşık 6,5 milyon satır Lean kodu çıktı.

Bu milyonlarca satıra güvenmek gerekmiyor. Lean’in çekirdeği her adımı denetleyip geçerli olmayan kanıtları eliyor; dolayısıyla kanıtı hangi modelin yazdığı ya da süreç boyunca kaç kez hata yaptığı önem taşımıyor. İnsanların güvenmesi gereken kısım çok daha küçük: yaklaşık 26.000 satırlık belirtimler ve bir ARM işlemcisinin kodu nasıl çalıştırdığını gösteren bir model.

Kanıtlar, Signal’deki bir konuşmayı koruyan bileşenleri kapsıyor: sohbeti başlatan PQXDH el sıkışma sürecini ve her mesajda anahtarı değiştiren Triple Ratchet’i. Buna, gelecekteki kuantum bilgisayarların saldırılarına direnmesi amaçlanan kuantum sonrası katman da dahil. Pratikte bu, bir telefonun o anki anahtarları çalınsa bile eski mesajların açılamayacağı ve iki taraf yeni anahtarları değiştirdikten sonra hırsızın erişimini yeniden kaybedeceği anlamına geliyor.

Araştırmacılar, sistemin doğru kodla hatalı kodu ayırt edebildiğini göstermek için libsignal’deki, daha önce tespit edilip düzeltilmiş iki eski hatayı yeniden ekledi. Bunlardan biri, kütüphanenin atması gereken gizli bir anahtarın kopyasını saklamasına yol açıyordu. AlphaProof Code, her iki durumda da hatalı derlemenin güvensiz olduğunu gösteren, makine tarafından denetlenmiş bir kanıt üretti.

Sistemin sınırları da var. Kanıt yalnızca bire bir oturumları kapsıyor; DeepMind, grup mesajlaşmasını gelecekte yapılacak çalışmalar arasında sayıyor. Sonuç, iPhone, Android ya da masaüstü için geliştirilmiş Signal uygulamalarının tamamına değil, küçük bir test programı içinde ARM Linux için standart Rust derleyicisiyle derlenen libsignal 0.105.4 sürümüne uygulanıyor. Düşük seviyeli kriptografik yapı taşlarının güvenli olduğu varsayılıyor, ancak bu güvenlik kanıtlanmış değil. İnsanların onayladığı belirtimlerdeki bir hata, güvencenin zayıflamasına yol açabilir. WhatsApp ve diğer uygulamalar da protokolün kendi sürümlerini kullandığından, bu sonuç onlara kendiliğinden uygulanmıyor. Google ayrıca Wired’a analizin ne kadara mal olduğunu ya da bunu bir hizmet olarak satmayı planlayıp planlamadığını açıklamayı reddetti.

Signal sonucu memnuniyetle karşıladı. Signal’in teknoloji direktörü Ehren Kret, yaptığı açıklamada, “Yapay zekâ kaynaklı güvenlik tehditleri artarken Signal protokolü uygulamasının titizlikle doğrulanması, kodumuzun gizlilik güvencelerine duyduğumuz güveni daha da artırıyor,” dedi. DeepMind araştırma bilimcisi Swarat Chaudhuri ise daha temkinli konuştu; Wired’a, bu yöntemin “dünyadaki tüm yazılımlara” ölçeklenebilmesi için “önümüzde daha uzun bir yol olduğunu” söyledi.

Signal kullananların herhangi bir şey yüklemesine ya da bir ayarı değiştirmesine gerek yok. Kanıt, uygulamada zaten bulunan kodla ilgili.

DeepMind, çalışmayı teknik bir makaleyle birlikte 10 Kasım’da yayımladı ve belirtimlerle kanıtları GitHub’da açık kaynak olarak paylaştı. Şirket, Signal projesini nisan ayında belirlenen biçimsel doğrulama alanındaki büyük hedefe giden yolda bir dönüm noktası olarak tanımlıyor; bundan sonra incelemek istediği sistemlere tıbbi cihaz yazılımlarını ve elektrik şebekesi yazılımlarını örnek gösteriyor.

Chaudhuri, makinelerin bu işin ne kadarını üstlenmesi gerektiği konusunda da bir sınır çizdi. Wired’a, “Yapay zekânın hedefleri, yine yapay zekânın da kanıtları ürettiği böyle bir dünya istemiyoruz,” dedi. Neyin güvenli sayılacağına hâlâ insanlar karar veriyor; yapay zekâ ise yalnızca bunun kanıtını ortaya koyuyor.

Etiketler: siber güvenlik, Google DeepMind, AlphaProof Code, biçimsel doğrulama, libsignal, Signal