Anthropic, Claude modelinin 123 açık kaynaklı yazılım kütüphanesindeki güvenlik özelliklerini biçimsel yöntemlerle doğruladığını ve bu süreçte yüzlerce hata ortaya çıkardığını açıkladı. Bazı güvenlik açıkları, trilyonlarca otomatik test çalıştırılmasına rağmen yıllarca tespit edilememişti.
Yazılım doğrulama şirketi Theorem ortaklığıyla yürütülen proje, matematiksel kanıtları doğrudan derlenmiş makine koduna uyguluyor. Araştırmacılar, bu yaklaşımın kapsamlı yazılım doğrulamasını çok daha geniş bir proje yelpazesi için uygulanabilir kılabileceğini belirtiyor.
Çalışma, giderek büyüyen bir güvenlik sorununu hedef alıyor. Otomatik araçlar artık olgun yazılımlardaki açıkları dahi bulabiliyor; bu durum geliştiricileri istismar edilebilir kusurları önleyecek daha güçlü yöntemler aramaya yöneltiyor. Biçimsel doğrulama, kodun belirli koşullar altında tanımlanmış kurallara uyduğunu ispatlayarak bu alanda potansiyel bir çözüm sunuyor.
Claude Gizli Hataları Ortaya Çıkarıyor
Geleneksel yazılım testleri, hataları ortaya çıkarmak için programları seçilmiş girdilerle çalıştırıyor. Fuzzing araçları ise çok sayıda alışılmadık girdi üretiyor ancak olası tüm kombinasyonları test edemiyor.
Anthropic, Claude’u mevcut fuzzing testlerini matematiksel belirtimlere dönüştürmek için kullandı. Model daha sonra 123 kütüphanedeki 239 program giriş noktasının, belirlenen koşullar altında çökmeyeceğini gösteren matematiksel ispatlar üretti.
Araştırmacılar, işlemcinin yürüttüğü komutları temsil eden RISC-V makine dili (assembly) kodu üzerinde çalıştı. Claude yaklaşık 180 milyon satır kanıt kodu oluştururken, tipik bir kanıt tek başına yaklaşık 600.000 satıra ulaştı.
Rocq adlı bağımsız bir araç, üretilen kanıtların şartnamelere uygunluğunu denetledi. Bu bağımsız doğrulama adımı, geliştiricilerin oluşturulan kanıt kodlarını satır satır manuel inceleme zorunluluğunu ortadan kaldırıyor. Anthropic ayrıca Claude’un doğrulama sırasında keşfedilen hataları yamamasına olanak tanıdı; model daha sonra güncellenen kod için yeni kanıtlar üretti.
Kusurlar Yıllarca Süren Testleri Atlattı
Bu süreç, geleneksel fuzzing testlerinin bulmakta zorlanabileceği güvenlik açıklarını ortaya çıkardı. Kütüphanelerden birinde, sıkıştırılmış verinin açılması sırasında bellek sınırları dışına yazmaya yol açabilecek bir sayaç alt taşması bulunuyordu.
Kusurun ortaya çıkması için nadir bir veri düzenine sahip yaklaşık 20 MB boyutunda bir girdi gerekiyordu. Bir başka hata ise arızayı sergilemek adına 64 MB’lık bir girdi ile 2 GB’tan fazla belleğe ihtiyaç duyan bir görsel kod çözücüde (image decoder) yer alıyordu.
Claude ayrıca, aynı dosyaya işaret eden iki dosya tanıtıcısının kullanıldığı belirli bir işlem sırasına bağlı olarak ortaya çıkan, bellek sınırları dışından okuma hatası keşfetti. Başka bir durumda ise libexpat XML ayrıştırıcısındaki bilinen bir güvenlik açığını yeniden keşfetti.
Her sorun çökmeye yol açmadı. Model ayrıca bir uygulamanın yükleyebileceği dosyaları kısıtlamak için tasarlanan bir özelliği atlatmasına izin verebilecek bir mantık hatasını da ortaya çıkardı.
Elde edilen bulgular, biçimsel doğrulamanın rutin testlerin gözden kaçırdığı kusurları yakalamada yardımcı olabileceğini gösteriyor. Bu yöntem, standart testlerin izin verilen tüm girdiler genelinde ispatlayamadığı güvenlik niteliklerini kesinleştirmeyi de sağlıyor.
Kanıtların Önemli Sınırları Var
Anthropic, biçimsel olarak doğrulanan yazılımların kendiliğinden hatasız sayılamayacağı konusunda uyardı. Sunulan güvenceler yalnızca her kanıtta tanımlanan belirli nitelikler, girdiler ve varsayımlar dahilinde geçerlilik taşıyor.
Mevcut çalışma, modellenmiş bir Linux ortamında çalışan tek iş parçacıklı, statik olarak bağlanmış RISC-V programlarını kapsıyor. Kullanımdaki sistemlerin çoğu ise başka işlemci mimarilerinden ya da farklı yazılım yapılandırmalarından yararlanıyor.
Şartnameler de kapsamına almadığı özellikleri güvence altına alamıyor. Bu nedenle araştırmacıların, kurdukları matematiksel modellerin gerçek işlemcileri ve işletim sistemlerini doğru yansıttığından emin olmaları gerekiyor.
Tüm bu kısıtlamalara rağmen proje, yazılım geliştirmede biçimsel doğrulamanın çok daha geniş bir rol üstleneceğine işaret ediyor. Anthropic, daha gelişmiş modellerin ve yeniden kullanılabilir kanıtların kritik yazılım bileşenlerini denetleme maliyetini düşürmesini bekliyor.
Geliştiriciler yaygın paylaşılan kütüphaneleri bir kez doğrulayıp bu güvenceleri yeniden kullanabilirse, bu yaklaşım onlara bağımlı çalışan sayısız uygulamada güvenliği kökten güçlendirebilir.
Kaynak: https://interestingengineering.com/ai-robotics/claude-formal-verification-software-security
