Claude, 123 yazılım kütüphanesi için denetlenebilir güvenlik kanıtları hazırladı
Anthropic ve Theorem, Claude ile 123 açık kaynak kütüphanede belirli güvenlik özellikleri için biçimsel kanıtlar hazırladı. Ayrı bir doğrulayıcı, bu kanıtları derlenmiş programların matematiksel modellerine göre denetliyor. Çalışmada yazılım hataları da düzeltildi. Sağlanan güvence, programın çalışma koşullarına, girdi sınırlarına ve yazılım davranışını tanımlayan modellerin doğruluğuna bağlı; bütün kullanım biçimlerini kapsayan genel bir güvenlik belgesi anlamına gelmiyor.
Yapay Zekâ··Öğle
Claude belirli kütüphane özelliklerini kanıtlıyor
Anthropic, Claude modelleriyle 123 açık kaynak yazılım kütüphanesinde belirli güvenlik özellikleri için biçimsel kanıtlar hazırladığini açıkladı. Çalışma, program davranışına ilişkin matematiksel güvenceleri ele alıyor. Şirket, projenin birkaç hafta sürdüğünü belirtiyor.[1], [2]
Doğrulama çalışmasında Anthropic ile çalışan Theorem’in de katıldığı proje, yazılım sınama sistemi OSS-Fuzz içindeki 239 giriş noktasını kapsıyor. Belirli çalışma koşullarında çökme ve tanımlanmış bellek güvenliği hataları ele alınıyor. Bazı programlarda kanıtın tamamlanabilmesi için önce hataların giderilmesi gerekti. Anthropic, çalışma boyunca yüzlerce hatanın bulunup düzeltildiğini söylüyor.[1]
Üretilen kanıtları ayrı bir doğrulayıcı denetliyor
Projede kullanılan kanıt doğrulama yazılımı Rocq, üretilen kanıtları RISC-V makine kodu ve Linux süreç davranışının biçimsel modellerine göre denetliyor. İnceleme, tek iş parçacıklı ve statik bağlanmış programları, ayrıca musl yazılım kütüphanesini esas alıyor. Sabit bellek bütçesi ile 64 MB altındaki girdiler de koşullar arasında. Bu varsayımlar, açıklanan güvencenin geçerli olduğu programları ve çalışma ortamını daraltıyor.[1]
Kapsamı tanımlanan program modeli belirliyor
Güvence bütün giriş noktalarını, bütün bellek hatalarını veya kütüphaneyi çağıran yazılımın yanlış kullanımını kapsamıyor. Doğrulayıcıdaki, belirtimlerdeki veya makine modelindeki hatalar sonucu etkileyebiliyor. Anthropic, bazı kanıtları ve biçimsel modelleri, henüz kanıtlanmamış giriş noktalarının belirtimleriyle birlikte yayımladığını belirtiyor. Projede yamaların program davranışını nasıl değiştirdiği de değerlendiriliyor; bir hatayı düzeltmek, doğrulanan programı da değiştirebiliyor.[1]
