Google DeepMind, Ajan Tabanlı Yapay Zeka ile Signal Protokolünü Biçimsel Olarak Doğruladı

Google DeepMind araştırmacıları, Signal protokolünün temel kriptografik güvencelerinden bir kısmını matematiksel olarak kanıtlamak, yani biçimsel olarak doğrulamak için ajan tabanlı yapay zekayı dört haftalık bir kavram kanıtında kullandı. Çalışma, Signal uygulaması, Google Messages ve WhatsApp gibi platformlardaki iletişimi koruyan kriptografi için ek bir bağımsız doğrulama niteliği taşıyor ve yeni bir yapay zeka çerçevesi olan AlphaProof Code ile DeepMind'ın biçimsel doğrulama yeteneklerini gösteriyor.

Analizin bulguları

DeepMind analizi, incelediği Signal protokolü bölümlerinde yeni bir zafiyet bulmadı. Araştırmacılar, bilinen ve uzun süre önce düzeltilmiş zafiyetler içeren eski Signal sürümlerinde AlphaProof Code kullandığında, araç bunları doğru tanımladı ve protokolün biçimsel olarak doğrulanamayacağını gösterdi. Analiz, Signal mobil uygulamasının tamamını biçimsel olarak doğrulamadı ve DeepMind araştırmacıları bulgularını daha büyük bir sürecin tek bir kilometre taşı olarak nitelendiriyor. Araştırmacılar, Signal protokolü analizi için geliştirdikleri spesifikasyonu ve kanıtı, başka biçimsel doğrulama çalışmalarına yardımcı olmak için yayımlıyor.

Biçimsel doğrulama neden önemli

Biçimsel doğrulama, yazılımın amaçlandığı gibi çalıştığını, yani kritik açıklar içermediğini kontrol etmek için matematiği kullanır; bu nedenle savunucuları onu uzun süredir yazılım güvenliğinde bir tür kutsal kâse olarak adlandırıyor. Yapay zeka öncesi dönemde, kanıtlamak istedikleri yazılımın özelliklerini tanımlamak, bu özetleri formüllere dönüştürmek ve ardından kanıtı geliştirmek insanlar için son derece zaman alıcıydı. Ajan tabanlı yapay zeka, DeepMind'ın Signal değerlendirmesi gibi analizlere olanak tanıyarak bu son görevin süresini önemli ölçüde kısaltabilir. DeepMind'ın kritik ilerlemeleri arasında, ajanların hemen her aşamada katkı sunmasına ve kendini düzeltmesine izin verirken kilit noktalarda insan girdisi ve incelemesi arayan bir insan-yapay zeka iş birliği süreci var. "Biz, yapay zekanın hedefleri ürettiği, kanıtları ürettiği ve temelde kendi yazdığı testlere girdiği böyle bir vibe dünyası istemiyoruz," diyor DeepMind araştırma bilimcisi Swarat Chaudhuri WIRED'a. "Bir orta yol var."

Ölçek ve maliyet konusundaki açık sorular

Yapay zeka destekli biçimsel doğrulamanın yaygın kullanım için ne kadar pratik olacağı ve büyük miktarda kodu güvence altına almada ne kadar etkili olabileceği hâlâ belirsiz. DeepMind, Signal analizini bir araştırma projesi olarak ücretsiz yürüttü; Google ise analizin maliyetini paylaşmayı ve ticari bir biçimsel doğrulama ürünü ya da hizmeti yayımlama planları olup olmadığı konusunda yorum yapmayı reddetti. Signal'ın baş teknoloji sorumlusu Ehren Kret, bir açıklamada önceki biçimsel doğrulamanın kodun daha küçük bölümlerine odaklandığını, Google DeepMind'ın yaklaşımının ise önemli bir genişleme sağladığını söylüyor. "Yapay zeka destekli güvenlik tehditleri arttıkça, Signal protokolü uygulamasını titizlikle doğrulamak, kodumuzun gizlilik güvencelerine yönelik güvenimizi daha da artırıyor," diyor Kret. Google Cloud'un baş bilimcisi ve DeepMind'ın araştırma başkan yardımcısı Pushmeet Kohli, uygulamaların doğruluğu artık doğrulanabiliyorsa, güvencelere dayanan ve hatalardan endişe duyan şirketlerin bu özellikleri kanıtlayabildiklerini söyleyebileceklerini belirtiyor. Chaudhuri, DeepMind'ın sonuçtan heyecan duyduğunu ancak bunu dünyanın tüm yazılımına ölçeklendirmeden önce uzun bir yol olduğunu söylüyor.

Kaynaklar: Wired