Google DeepMind araştırmacıları, yapay zeka ajanları (agentic AI) kullanarak, yaygın olarak kullanılan Signal protokolünün kritik şifreleme güvencelerini matematiksel olarak kanıtladı. Bu gelişme, hem kriptografi hem de yapay zeka alanında önemli bir dönüm noktası olarak kabul ediliyor.
Dört hafta gibi kısa bir sürede tamamlanan bu konsept kanıtlama projesi, iki önemli açıdan dikkat çekiyor. İlk olarak, Signal uygulaması, Google Mesajlar ve WhatsApp gibi platformlarda dünya çapında büyük miktarda iletişimi koruyan kriptografinin bağımsız bir şekilde doğrulanmasını sağlıyor. İkinci olarak ise, Google DeepMind'ın AlphaProof Code adlı yeni bir yapay zeka çerçevesi kullanarak formal doğrulama yeteneklerini gözler önüne seriyor.
Daha geniş bir perspektiften bakıldığında, yapay zeka destekli formal doğrulama günümüzde popülerleşiyor. Ancak, geniş çaplı kullanım için ne kadar pratik olacağı ve büyük miktarda kodu ne ölçüde güvence altına alabileceği henüz belirsizliğini koruyor. Formal doğrulama savunucuları, bu yöntemi yazılım güvenliğinin kutsal kâsesi olarak görüyor, zira matematiksel olarak yazılımın amaçlandığı gibi çalıştığını, yani kritik güvenlik açıklarının olmadığını kontrol ediyor.
Yapay zeka çağından önce, insanların yazılımın özelliklerini tanımlamak, bu özetleri formüllere dönüştürmek ve ardından kanıtları geliştirmek için inanılmaz derecede zaman harcaması gerekiyordu. Yapay zeka ajanları, özellikle son adımdaki zamanı önemli ölçüde azaltarak DeepMind'ın Signal değerlendirmesi gibi analizlere olanak tanıyor. Ancak, bu analiz bile sınırlı bir kapsamdaydı; örneğin, tüm Signal mobil uygulamasını kapsamadı. DeepMind araştırmacıları da bulgularının daha büyük bir sürecin sadece bir kilometre taşı olduğunu vurguluyor.
DeepMind araştırma bilimcisi Swarat Chaudhuri, bu sonuçtan dolayı çok heyecanlı olduklarını ancak dünyanın tüm yazılımlarına bu yöntemi ölçeklendirmeden önce gidilecek uzun bir yol olduğunu belirtti. DeepMind analizi, incelenen Signal protokolü bölümlerinde herhangi bir yeni güvenlik açığı bulmadı. Ancak araştırmacılar, AlphaProof Code'u bilinen ve uzun süredir düzeltilmiş güvenlik açıklarını içeren eski Signal sürümlerinde kullandıklarında, bu açıkları doğru bir şekilde tespit etti ve protokolün resmi olarak doğrulanamayacağını gösterdi. Araştırmacılar, diğer formal doğrulama çalışmalarına yardımcı olmak amacıyla Signal protokolü analizi için geliştirdikleri spesifikasyonu ve kanıtı yayınlıyorlar.
Projenin hızı dikkat çekici olsa da, DeepMind araştırmacıları, Signal Vakfı'nın daha önceki formal doğrulama çalışmalarından bir dereceye kadar fayda sağladıklarını belirtiyor. Signal'ın teknoloji şefi Ehren Kret, yaptığı açıklamada, önceki formal doğrulamaları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öyledi. Kret, yapay zeka kaynaklı güvenlik tehditleri arttıkça, Signal protokolü uygulamasının titizlikle doğrulanmasının, kodun gizlilik güvencelerine olan güvenlerini daha da artırdığını ekledi.
Yüksek riskli ortamlarda kullanılan kritik hizmetler için, her kod tabanını ve tüm yazılım tedarik zincirlerini tam olarak doğrulayabilmek bir rüya. Google Cloud ve DeepMind araştırma başkan yardımcısı Pushmeet Kohli, bu uygulamaların doğruluğunu artık doğrulayabildiklerinde, bankalar ve hatalardan endişe duyan, özelliklerin doğruluğunu kanıtlayabileceğini söyleyebilecek diğer şirketler için rahat bir nefes alınabileceğini belirtti.
Ancak teknoloji sektöründe açık soru şu ki, yapay zeka otomasyonlu formal doğrulama gerçekten ölçeklenebilir mi ve bunun maliyeti makul düzeyde olabilir mi? DeepMind, Signal analizini bir araştırma projesi olarak ücretsiz gerçekleştirdi ve Google analizin maliyetini paylaşmadı. Şirket ayrıca ticari bir formal doğrulama ürünü veya hizmeti çıkarma planları olup olmadığı konusunda yorum yapmaktan kaçındı.
Araştırmacılar, kritik ilerlemelerinden bazılarının, ajanların sürecin neredeyse her aşamasında katkıda bulunmasına ve kendi kendini düzeltmesine olanak tanıyan, ancak yine de önemli noktalarda insan girdisi ve incelemesi arayan bir "insan-yapay zeka işbirliği süreci" geliştirmeleri olduğunu söylüyor. Chaudhuri, yapay zekanın hedefleri ve kanıtları ürettiği bir ortam istemediklerini, bunun yerine bir "orta yol" bulunduğunu vurguluyor.
Kaynakça: arstechnica.com
