- Katılım
- 22 Aralık 2023
- Mesajlar
- 2.796
- Çözümler
- 1
- Beğeniler
- 1.308
Google DeepMind araştırmacıları, AlphaProof Code adlı yapay zekâ destekli sistemle Signal'ın açık kaynaklı libsignal kütüphanesini inceledi. Çalışmanın amacı, yazılımın belirli kriptografik güvenlik özelliklerini gerçekten sağlayıp sağlamadığını matematiksel olarak kanıtlamaktı.
Yaklaşık dört hafta süren çalışma sonucunda sistem, 6,5 milyon satır civarında makine tarafından kontrol edilebilir ispat kodu üretti. Bu süreçte Signal'ın geçmiş mesajları korumaya yönelik Forward Secrecy, cihaz ele geçirildikten sonra güvenliğin yeniden kazanılmasını sağlayan Post-Compromise Security ve kimlik doğrulama gibi özellikleri incelendi.
Araştırmacılar ayrıca geçmişte düzeltilmiş iki yazılım hatasını yeniden sisteme ekleyerek yapay zekânın bu güvenlik ihlallerini tespit edip edemediğini test etti. Sistem, hatalı sürümlerin belirlenen güvenlik özelliklerini sağlayamadığını ortaya koydu.
Burada önemli bir ayrıntı var: Çalışma, Signal'ın tamamının veya bütün olası saldırılara karşı güvenli olduğunun kanıtlandığı anlamına gelmiyor. Yalnızca incelenen kodun belirli matematiksel güvenlik özelliklerini sağladığı doğrulandı.
deepmind.google
Yaklaşık dört hafta süren çalışma sonucunda sistem, 6,5 milyon satır civarında makine tarafından kontrol edilebilir ispat kodu üretti. Bu süreçte Signal'ın geçmiş mesajları korumaya yönelik Forward Secrecy, cihaz ele geçirildikten sonra güvenliğin yeniden kazanılmasını sağlayan Post-Compromise Security ve kimlik doğrulama gibi özellikleri incelendi.
Araştırmacılar ayrıca geçmişte düzeltilmiş iki yazılım hatasını yeniden sisteme ekleyerek yapay zekânın bu güvenlik ihlallerini tespit edip edemediğini test etti. Sistem, hatalı sürümlerin belirlenen güvenlik özelliklerini sağlayamadığını ortaya koydu.
Burada önemli bir ayrıntı var: Çalışma, Signal'ın tamamının veya bütün olası saldırılara karşı güvenli olduğunun kanıtlandığı anlamına gelmiyor. Yalnızca incelenen kodun belirli matematiksel güvenlik özelliklerini sağladığı doğrulandı.
Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
AlphaProof Code agents wrote over three million lines of machine-checked proof in Lean to verify the core cryptographic protections in Signal down to machine instructions.
