6,5 milyon satır kanıt kodu: Yapay zekâ Signal'in bire bir sohbet kodunu doğruladı

Google DeepMind, Signal'in şifreleme protokolündeki bire bir sohbet kodunun temel güvenlik özelliklerini matematiksel olarak doğruladı. Dört hafta süren çalışma grup sohbetlerini ve Signal uygulamasının tamamını kapsamadı.

Google DeepMind, ayın 10'unda resmi blogunda ve teknik makale ile kanıt materyallerinde AlphaProof Code araştırmasının sonuçlarını yayımladı. AlphaProof Code, insanlar tarafından belirlenen güvenlik koşullarına göre yapay zekâ ajanlarının gerçek kod için kanıt oluşturduğu bir biçimsel doğrulama çerçevesi.

Biçimsel doğrulama, bazı girdilerle hata arayan testlerden farklı işliyor. Kodun uyması gereken koşullar matematiksel olarak ifade ediliyor ve kodun bu koşulları karşılayıp karşılamadığı kanıtlanıyor.

Araştırmacılar hangi güvenlik özelliklerinin kanıtlanacağını belirleyerek spesifikasyonları yazdı ve gözden geçirdi. Yapay zekâ ajanlarının oluşturduğu kanıtlar ancak Lean denetleyicisinden geçerse kabul edildi; sonuca yalnızca ajanların değerlendirmesiyle varılmadı.

İncelenen hedef, libsignal 0.105.4 ve SPQR 1.6.0 ile oluşturulan, bire bir sohbet için bir yürütülebilir dosyaydı. Araştırmacılar değiştirilmemiş kütüphaneleri bir komut satırı aracına sarıp aracı AArch64 makine koduna derleyerek analiz etti.

Doğrulanan özellikler, sohbet başlarken şifreleme anahtarları üzerinde anlaşmayı sağlayan PQXDH ile her mesajda anahtarları yenileyen Triple Ratchet oldu. Signal protokol ailesi Signal uygulamasının yanı sıra Google Mesajlar, WhatsApp ve Meta Messenger'da da kullanılıyor.

Makale, geçmiş mesajların daha sonra anahtarlar açığa çıksa bile okunamamasını sağlayan ileri yönlü gizliliği, anahtarların açığa çıkmasından sonra korumanın yeniden sağlanmasını ve karşı tarafın doğrulanmasıyla ilk bağlantının gizliliğini kanıt kapsamındaki özellikler arasında saydı. Mesajların gizliliği ve gerçekliğinin doğrulanması da incelendi.

Araştırmacılar sonuçları hem sembolik hem de hesaplamalı modelde sundu. Sembolik model, kriptografik işlemleri ideal kabul ediyor. Hesaplamalı model ise hesaplama gücü sınırlı bir saldırganı varsayarak güvenlik özelliklerini inceliyor.

İki modelin sağladığı güvenceler aynı değil. Sembolik model, kuantum saldırganının Diffie-Hellman anahtar değişimini kırdığı durumda bile ilk bağlantının gizliliğini ele aldı. Hesaplamalı model kuantum saldırganlarını kapsamadı; SPQR'nin kuantum saldırılarına karşı koruma sağlayan kurtarma özelliği de kanıt kapsamı dışında kaldı.

Çalışma, protokol tasarım belgeleriyle sınırlı kalmayıp derlenmiş bir yürütülebilir dosyanın davranışını spesifikasyonla karşılaştırdı. Ancak kanıtlanan hedef Signal uygulaması değil, araştırmacıların oluşturduğu komut satırı aracına ait yürütülebilir dosyaydı.

Sonuçlar bazı varsayımlara dayanıyor. Kriptografik işlemlerin ve bazı kütüphane özelliklerinin sözleşmede belirtilen koşullara uygun çalıştığı kabul edildi. Lean denetleyicisi ile AArch64 anlam modeli de güven temelinin parçasıydı.

Doğrulama iki kullanıcı arasındaki sohbetlerle sınırlı kaldı. Grup mesajlaşması, birden fazla cihazın durumu ve Signal uygulamasının kendisi kapsama alınmadı; araştırmacılar makalede bu sınırlamayı açıkça belirtti.

Araştırmacılar yöntemin kusurları tespit edip edemediğini görmek için daha önce bulunup düzeltilmiş iki hatayı izole edilmiş koda yeniden ekledi. Her iki durumda da güvenlik önermesinin geçerli olmadığını makineyle doğruladılar. Yeni bir güvenlik açığı bulmadılar.

Beş kişilik araştırma ekibi dört hafta boyunca paralel çalışarak yaklaşık 6,5 milyon satır Lean kanıt kodu üretti. Makaleye göre kanıt için gereken güvenilir spesifikasyonlar ile AArch64 anlam modeli yaklaşık 26 bin satırdan oluşuyordu.

Signal CTO'su Ehren Kret, “Geleneksel biçimsel doğrulama kodun küçük bölümlerine odaklanıyordu; Google DeepMind'ın yaklaşımı kapsamı önemli ölçüde genişletiyor” dedi. Kret'in değerlendirmesi, protokol uygulamasının daha geniş kapsamda incelenmesine dayanıyor.

WIRED, araştırmanın yapay zekâ destekli biçimsel doğrulamanın uygulamadaki ölçeklenebilirlik ve maliyet sorunlarını çözüp çözmediğinin net olmadığını belirtti. Google analiz maliyetini veya ticari doğrulama ürünü ya da hizmeti sunma planını açıklamadı.

Makale, sonraki doğrulama çalışmaları için grup mesajlaşmasını, gönderici gizliliği özelliklerini ve sunucu tarafındaki protokolleri gündeme getirdi. Google DeepMind spesifikasyonları ve kanıt materyallerini yayımladı.