Anthropic, mevcut projelerin güvenilirliğini ve güvenliğini resmi olarak doğrulamak için yapay zeka modelleri kullanılarak yapılan deneylerin sonuçlarını sundu. Deney sırasında, OSS Fuzz altyapısında test edilen 123 açık kaynaklı kütüphane için bellek hatalarının bulunmadığına dair matematiksel kanıtlar üretmek amacıyla yapay zeka modelleri kullanıldı.
Doğrulama, RISC-V mimarisi için derlenmiş assembly kodu seviyesinde gerçekleştirildi. Oluşturulan kanıtların toplam hacmi, Rocq Prover doğrulama sistemi için yaklaşık 180 milyon satır koda (600 RISC-V komutu içeren ikili dosya başına yaklaşık 18 satır) ulaştı. Kanıtlar, mevcut fuzzing testlerinin otomatik olarak biçimsel spesifikasyonlara dönüştürülmesiyle oluşturuldu ve ardından Claude AI modeli, programın 64 MB'a kadar olan herhangi bir giriş verisi için hatasız olduğunu kanıtladı.
Kanıt oluşturma sürecinde, yapay zeka modeli, daha önce bulanık testlerle tespit edilemeyen yüzlerce hatayı belirleyip düzeltmeler hazırlayabildi. Bunlar arasında, belirli girdi verilerinin işlenmesi sırasında ortaya çıkan arabellek taşması güvenlik açıkları (örneğin, libexpat'taki CVE-2026-56132) ve mantıksal hatalar yer alıyordu. Ayrıca, yapay zeka modeli, çekirdeğin zlib algoritmasının uygulamasının uygunluğunu kanıtlamak için de kullanıldı. Linux RFC 1950 spesifikasyonları.
Python'ın bir alt kümesi için Rust dilinde bir yorumlayıcı da oluşturuldu ve Verus araç seti kullanılarak CPython semantiğine uygunluğun resmi bir kanıtı hazırlandı. Davranışı CPython ile karşılaştırmak için 1.7 milyondan fazla rastgele oluşturulmuş Python programı çalıştırıldı. Vakaların %99.95'inde, bu programların yeni uygulamada ve CPython'da çalıştırılmasının sonuçları eşleşti ve bulunan herhangi bir tutarsızlık bilinen uç durumlar oldu.
Biçimsel doğrulama, spesifikasyona uygunluğu garanti eder, ancak çoklu iş parçacığı sorunları, dinamik bağlantı ve gerçek donanımda anormal davranışlardan kaynaklanan riskler biçimselleştirilmediği için güvenlik sorunlarını tamamen ortadan kaldırmaz. Önerilen yaklaşımın en önemli avantajı, mevcut kodu biçimsel olarak doğrulanabilir dillerde yeniden yazma ihtiyacını ortadan kaldırarak doğrudan ikili dosyalarla çalışmasıdır.
Kaynak: opennet.ru
