Yazılım güvenliğinde kullanılan testler, her olası hatayı ortaya çıkarmaya yetmeyebiliyor. Anthropic’in Theorem ile yürüttüğü yeni çalışma, yapay zekânın matematiksel doğrulama yöntemleriyle bu boşlukların kapatılmasına nasıl katkı sağlayabileceğini gösteriyor.
Araştırmacılar, Claude’u kullanarak yazılımların belirli güvenlik koşullarını sağlayıp sağlamadığını matematiksel olarak kanıtlamaya odaklandı. Bu yaklaşım, yalnızca yazılımı farklı girdilerle denemek yerine, tanımlanan koşullar altında nasıl davrandığını doğrulamayı amaçlıyor.
Claude, Yazılımın Güvenliğini Nasıl İnceledi?
Geleneksel yazılım testlerinde programlar farklı girdilerle çalıştırılıyor ve ortaya çıkan hatalar inceleniyor. Fuzzing adı verilen yöntem ise çok sayıda beklenmedik girdi üreterek yazılımların sınırlarını zorluyor. Ancak bu yöntemlerle bütün olasılıkları denemek mümkün değil.
Anthropic’in çalışmasında Claude, mevcut fuzzing testlerini matematiksel olarak ifade edilen gereksinimlere dönüştürmek için kullanıldı. Model, 123 yazılım kütüphanesindeki 239 program giriş noktası için, belirlenen koşullar altında çökmeme özelliğini kanıtlayan çıktılar üretti.
Çalışmanın önemli bir özelliği, doğrulamanın doğrudan RISC-V işlemci mimarisine ait makine kodu üzerinde gerçekleştirilmesiydi.
180 Milyon Satırlık Kanıt Üretildi
Claude, yaklaşık 180 milyon satır matematiksel kanıt kodu oluşturdu. Tipik bir kanıtın uzunluğu yaklaşık 600 bin satıra ulaştı.
Üretilen kanıtlar, Rocq adlı bağımsız bir doğrulama aracıyla kontrol edildi. Böylece sonuçların yalnızca Claude’un değerlendirmesine dayanmasının önüne geçilmesi amaçlandı. Araştırmacılar ayrıca modelin tespit ettiği bazı kusurları düzeltmesine ve güncellenen kod için yeni kanıtlar üretmesine olanak tanıdı.
Yıllarca Gizli Kalan Hatalar Nasıl Bulundu?
Araştırmada ortaya çıkan kusurların bazıları, yalnızca oldukça özel koşullar altında kendini gösteriyordu.
Örneğin bir kütüphanede, sıkıştırılmış verilerin açılması sırasında bellek sınırlarının dışına yazılmasına neden olabilecek bir sayaç alt taşması tespit edildi. Bu hatanın ortaya çıkması için belirli bir veri düzenine sahip yaklaşık 20 MB büyüklüğünde bir girdi gerekiyordu.
Bir başka kusur, 64 MB boyutundaki bir girdiyi işlerken 2 GB’tan fazla bellek gerektiren bir görsel kod çözücüde bulundu. Claude ayrıca aynı dosyaya işaret eden iki dosya tanıtıcısının belirli bir sırayla kullanılmasına bağlı bir bellek okuma hatasını da ortaya çıkardı.
Bulgular bunlarla sınırlı kalmadı. Model, libexpat XML ayrıştırıcısında daha önce bilinen bir güvenlik açığını yeniden tespit etti. Ayrıca bir uygulamanın yükleyebileceği dosyaları sınırlayan güvenlik mekanizmasını aşmaya imkân verebilecek bir mantık hatası da belirlendi.
Bu örnekler, bazı yazılım kusurlarının neden uzun süre gizli kalabildiğini ortaya koyuyor. Hataların tetiklenmesi için alışılmadık veri yapıları, yüksek bellek tüketimi veya belirli işlem sıraları gerekebiliyor.
Matematiksel Kanıtlar Her Hatayı Ortadan Kaldırıyor mu?
Biçimsel doğrulama, yazılımın belirli özelliklerini matematiksel olarak kanıtlamayı sağlıyor. Ancak bu, bir programın tüm koşullarda hatasız olduğu anlamına gelmiyor.
Anthropic’in çalışması, modellenmiş bir Linux ortamında çalışan tek iş parçacıklı ve statik olarak bağlanmış RISC-V programlarıyla sınırlı. Gerçek sistemlerde farklı işlemci mimarileri, işletim sistemleri ve yazılım yapılandırmaları kullanılabiliyor.
Üstelik doğrulama, yalnızca matematiksel şartnamelerde tanımlanan özellikleri kapsıyor. Şartnamede yer almayan bir güvenlik sorunu, bu yöntemle kendiliğinden güvence altına alınmış olmuyor.
Buna rağmen araştırma, yapay zekânın yazılım güvenliğinde yalnızca hata tespit eden bir araç olmanın ötesine geçebileceğini gösteriyor. Claude’un ürettiği kanıtlar bağımsız bir araçla doğrulanabiliyor ve bazı kusurların düzeltilmesinin ardından yeniden kullanılabiliyor.
Bu yaklaşım daha geniş ölçekte uygulanabilirse, milyonlarca uygulamanın dayandığı ortak yazılım kütüphanelerindeki güvenlik açıklarını azaltmak ve doğrulama süreçlerini daha erişilebilir hâle getirmek için önemli bir fırsat sunabilir.