Google DeepMind, AlphaProof Code ile Signal'in post-quantum handshake ve Triple Ratchet katmanlarını biçimsel olarak doğruladı; ajanlar 6,5 milyon satır Lean ispatı yazdı

Google DeepMind araştırmacıları, Signal'in mesajlaşma güvenliğinin temel parçalarını biçimsel olarak doğruladıklarını (formal verification) açıkladı. The Register'ın aktardığına göre çalışma, Signal'in post-quantum PQXDH handshake'ini ve Triple Ratchet'ini kapsıyor. Ekip, AI'ın protokol düzeyindeki güvenlik güvencelerini yaygın kullanılan bir kriptografik uygulamaya bağlayan bir ispatın hazırlanmasına ilk kez yardım ettiğini öne sürüyor.

Çalışmada AlphaProof Code adlı çok ajanlı bir çerçeve kullanıldı. İspat, libsignal'in forward secrecy, kimlik doğrulama, post-compromise security ve handshake gizliliği özelliklerini doğruluyor. DeepMind'ın duyurusu AlphaProof Code blog yazısında yer alıyor.

Nasıl çalıştı?

Önce Signal'in güvenlik hedefleri, insanların gözden geçirdiği matematiksel bir şartnameye (specification) dönüştürüldü. Ardından Gemini Carbon ajanları, libsignal uygulamasının bu şartnameye uyduğunu gösteren Lean kodunu yazdı. Ajanlar toplam 6,5 milyon satır Lean kodu üretti. Sonra bir denetim turuyla insan incelemesi gereken bölümler işaretlendi. İspatın doğruluğunu Lean çekirdeği kontrol ediyor.

Sonucun bir sınırı var: İspat kriptografinin kusursuz olduğunu varsayıyor, baytların hesaplamalı gizliliğini garanti etmiyor. Yani algoritmalar değil, uygulamanın tasarıma uygunluğu ispatlanmış oluyor. İş, beş kişilik bir ekiple dört hafta sürdü. Karşılaştırma için: seL4 mikroçekirdeğinin doğrulanması 20 kişi-yıl, doğrulanmış CompCert C derleyicisinin geliştirilmesi altı yıl sürmüştü.

Neden önemli?

Biçimsel doğrulama şimdiye kadar çok pahalıydı. Bu yüzden yalnızca küçük, kritik bileşenlerde kullanılabiliyordu. DeepMind araştırmacısı Swarat Chaudhuri, saldırı amaçlı AI yeteneklerinin arttığını ve dünyadaki pek çok güvensiz sistemin istismar edileceğini söylüyor. Ona göre hedef, bu teknolojiyi genel koda uygulamak. Chaudhuri asıl zorluğun artık ispatta değil, neyin ispatlanacağını tanımlamakta olduğunu vurguluyor. Bu süreç de hâlâ insan gözetimine dayanıyor.

Kimin işine yarar / ne yapabilirsiniz?

1. Kriptografi ve protokol geliştiricileri: Kendi kütüphanelerinizin güvenlik hedeflerini yazılı ve test edilebilir özellikler olarak tanımlamaya bugünden başlayın. AI destekli doğrulamanın ilk koşulu iyi yazılmış bir şartname.
2. Güvenlik ekipleri: "Biçimsel olarak doğrulandı" ifadesini görünce ispatın varsayımlarını okuyun. Bu çalışmada kriptografinin kusursuz olduğu varsayılıyor.
3. Signal kullanıcıları: Yapmanız gereken bir şey yok. Bu çalışma bir açık bildirimi değil, mevcut tasarıma dair bir doğruluk güvencesi.