Signal şifreleme kodu, DeepMind yapay zekasıyla dört haftada doğrulandı

Resmi doğrulama nedir?

Yazılımın amaçlandığı gibi davrandığını testlerle değil matematikle göstermek demek. Eldeki en güçlü güvenlik garantisi sayılıyor ama geleneksel olarak yavaş ve zahmetli. Kriptografik protokol doğrulamalarının çoğu tasarım aşamasında kalıyor. DeepMind ise gerçek uygulamayı, yani hataların çoğu zaman saklandığı yeri kontrol ettiğini söylüyor. Şirkete göre bu kadar yaygın kullanılan bir protokolün uygulaması, yapay zekayla ya da yapay zekasız, ilk kez resmi olarak doğrulandı.

Sistem nasıl çalışıyor?

Sistemin adı AlphaProof Code ve birkaç yapay zeka modelini insan uzmanlarla birleştiriyor. DeepMind araştırmacıları ve modeller Signal'in güvenlik hedeflerini resmi şartnamelere çevirdi, uzmanlar da her birini inceledi. Gemini Carbon destekli ajanlar, bilgisayarın ispatları otomatik denetlemesini sağlayan Lean dilinde altı milyondan fazla satır ispat yazdı. Ardından ajanlar kendi işlerini denetledi ve kod tabanının yaklaşık yüzde 1'ini insanın ikinci kez bakması gereken bölüm olarak işaretledi. İspatlar, bir cihaz geçici olarak ele geçirilse bile mesajların öncesinde ve sonrasında korunması gibi özellikleri kapsıyor.

Analiz yeni bir güvenlik açığı bulmadı. Sistemin iyi kodla kötü kodu ayırt edip edemediğini görmek için ekip, Signal kodunun yalıtılmış bir sürümüne daha önce düzeltilmiş iki gerçek hatayı geri koydu. DeepMind'a göre sistem iki durumda da bu sürümün güvensiz olduğuna dair makineyle doğrulanmış bir ispat üretti.

Proje Signal'in tüm mobil uygulamasını doğrulamadı. Wired'a göre DeepMind, Signal Foundation'ın önceki resmi doğrulama çalışmasından da avantaj sağladı. Signal'in teknoloji direktörü Ehren Kret, önceki çalışmanın "kodun daha küçük kısımlarına odaklandığını", DeepMind'ın yaklaşımının ise "anlamlı bir genişlemeye imkân verdiğini" söyledi.

Araştırmacılar, yapay zekanın hem hedefleri hem ispatları yazdığı bir düzen istemiyor. DeepMind araştırmacısı Swarat Chaudhuri, yapay zekanın hedefleri de ispatları da ürettiği, yani kendi yazdığı sınavlara girdiği bir dünya istemediklerini söyledi. Bu yüzden şartnameleri ve işaretlenen bölümleri insanlar inceledi.

Bunun ölçeklenip ölçeklenmeyeceği ve maliyeti belirsiz. DeepMind analizi araştırma projesi olarak ücretsiz yaptı, maliyeti ve ticari bir ürün planını açıklamadı. Şirket doğrulama çıktılarını açık kaynak olarak paylaşıyor ve yaklaşımın ileride tıbbi cihaz yazılımlarına ve elektrik şebekesi yazılımlarına uzanabileceğini söylüyor.