Google DeepMind bünyesindeki araştırmacılar, Signal‘ın temel kodlarının belirli bölümlerini biçimsel olarak doğrulamak için YZ kullandı. Bu durum, şifreli mesajlaşma uygulamasının kodlarının en azından bir kısmının vaat ettiği işi hatasız şekilde yerine getirdiğini matematiksel olarak kanıtladıkları anlamına geliyor. YZ sistemlerinin son zamanlarda yazılımlarda çok sayıda güvenlik açığı keşfettiği ve milyonlarca insanın iletişiminin Signal’ın şifreleme altyapısıyla korunduğu düşünüldüğünde, söz konusu gelişme güven veriyor. WhatsApp ve Google Messages da aynı şifrelemeyi kullanıyor.
DeepMind, araştırmacıların ifadesiyle “insan uzmanlığını YZ ajanlarıyla birleştiren, eşi görülmemiş bir derinlikte biçimsel doğrulama sunan yeni bir ajan çerçevesi” olan AlphaProof Code sistemini kullandı. Araştırmacılar, biçimsel doğrulamanın “güvenlik güvencesinin en yüksek standardı” olduğunu ancak YZ sistemleri gibi geniş ölçekli bir otomasyon olmadan bu sürecin zor ve zaman alıcı kaldığını ekledi.
DeepMind Signal’ı Nasıl Doğruladı?
OpenAI gibi yapay zeka şirketleri, son dönemde matematik alanında peş peşe önemli gelişmelere imza atıyor. Bazı durumlarda YZ kullanarak neredeyse yüz yıllık matematik problemlerini çözüyorlar. YZ modelleri, çok büyük ölçekte hesaplama yapabilmeleri sayesinde matematikçilerin elle yürüttüğü çalışmaların önemli bir bölümünü hızlandırabiliyor.
DeepMind araştırmacıları, AlphaProof Code’u kullanarak ve Signal Foundation’ın önceki doğrulama çalışmalarından yararlanarak doğrulama sürecini iki bölüme ayırdı. İlk bölümde insanlar, YZ ajanlarıyla birlikte nelerin kanıtlanması gerektiğini belirledi. Ardından şirketin en yeni modeli Gemini Carbon ile çalışan birden fazla ajan, doğrulama işlemini gerçekleştirdi.
Ajanlar ayrıca oluşturulan kanıtları denetledi. Araştırmacıların ifadesiyle, “Bir insanın yeniden incelemesi gereken alanları belirledi. Bu alanlar kod tabanının yalnızca %1’ini oluşturuyordu ve büyük bir zaman tasarrufu sağladı.”
Araştırmacılar, AlphaProof Code’un doğru kod ile hatalı kodu ayırt etme becerisini de test etti. Bunun için sisteme Signal’de daha önce tespit edilip düzeltilmiş iki hata gösterdiler. Sistem, bu iki hata için doğru kanıtlar üretti.
Araştırmacılar sonuçları şöyle değerlendirdi:
“Çalışmamız, yaygın olarak kullanılan bir kriptografik protokolü bu derinlikte biçimsel olarak doğrulamak adına YZ’nin ilk kez kullanılışını temsil ediyor. Aynı zamanda böylesine yaygın dağıtılmış bir protokol uygulamasının, YZ ile veya YZ olmadan, herhangi bir yöntemle ilk kez biçimsel olarak doğrulanması anlamına geliyor.”
Normalde araştırmacıların yazılımları doğrulamak için manuel olarak bir kanıt geliştirmesi gerekiyor ve bu süreç çok daha uzun sürüyor. Yoğun emek gerektiren bu engel, şimdiye kadar biçimsel doğrulamayı ulaşılması güç bir vaat haline getiriyordu. DeepMind ekibinin yürüttüğü doğrulama, uzmanların normalde yıllarını alabilecek bir çalışmayı bir ayda tamamladı.
DeepMind, Signal kodlarının tamamını doğrulamadı ama bu testin, YZ’nin tüm siber güvenlik alanını kökten dönüştürdüğü bir dönemde güvenlik altyapısını güçlendirmeye yönelik bir adım olduğunu belirtti.
Araştırmacılar, “Temel Signal protokolünün otomatik teorem kanıtlama yoluyla titizlikle doğrulanması, kodumuzun gizlilik vaatlerini yerine getirdiğine yönelik güvenimizi daha da artırıyor.” ifadelerini kullandı.
Sırada Ne Var?
Bu atılım, YZ’nin siber güvenlik için hem büyük bir risk hem de aynı derecede güçlü bir çözüm olduğunu yeniden gösteriyor. 2026 yılı, özellikle birçoğunda ajanların yer aldığı YZ kaynaklı güvenlik vakalarıyla dikkat çekiyor. Aynı zamanda Anthropic, Google ve OpenAI gibi şirketler; Anthropic’in Claude Mythos modeli de dahil olmak üzere özellikle siber güvenliğe odaklanan modeller geliştiriyor.
DeepMind bulgularını tüketiciye yönelik bir ürün olarak çıkarma planı paylaşmadı fakat araştırmacılar, başkalarının biçimsel doğrulama çabalarına katkı sağlamak için kodlarını açık kaynak haline getiriyor. DeepMind, bu çalışmanın daha geniş etkisini şu sözlerle açıkladı:
“Signal’in temel şifreleme teknolojisinin doğrulanması, tıbbi cihazların aygıt yazılımlarından elektrik şebekesi yazılımlarına kadar diğer kritik sistemlerin güvenliğini sağlamak için de temel oluşturuyor.”
Kaynak: https://www.zdnet.com/tech/google-deepmind-researchers-prove-signal-whatsapp-encryption-works/
