Anthropic, mövcud layihələrin etibarlılığını və təhlükəsizliyini rəsmi olaraq yoxlamaq üçün süni intellekt modellərindən istifadə edərək aparılan təcrübələrin nəticələrini təqdim etdi. Təcrübə zamanı OSS Fuzz infrastrukturunda sınaqdan keçirilmiş 123 açıq mənbəli kitabxana üçün yaddaş səhvlərinin olmamasının riyazi sübutlarını yaratmaq üçün süni intellekt modellərindən istifadə edildi.
Doğrulama RISC-V arxitekturası üçün kompilyasiya edilmiş assembler kodu səviyyəsində aparılmışdır. Yaradılmış sübutların ümumi həcmi Rocq Prover doğrulama sistemi üçün təxminən 180 milyon sətir kod təşkil etmişdir (600 RISC-V təlimatı ilə ikili fayl üçün təxminən 18 sətir). Sübutlar mövcud fuzzing testlərini rəsmi spesifikasiyalara avtomatik çevirməklə yaradılmışdır və bundan sonra Claude AI modeli proqramın 64 MB-a qədər hər hansı giriş məlumatı üçün qüsursuz olduğunu sübut etmişdir.
Sübut qurma prosesi zamanı süni intellekt modeli əvvəllər fuzz testi ilə aşkarlanmayan yüzlərlə səhvi müəyyən edə və düzəlişlər hazırlaya bildi. Digər şeylər arasında bunlara müəyyən giriş məlumatlarını (məsələn, libexpat-da CVE-2026-56132) emal edərkən bufer daşma zəiflikləri, eləcə də məntiqi səhvlər daxil idi. Bundan əlavə, süni intellekt modeli nüvənin zlib alqoritminin tətbiqinin uyğunluğunu sübut etmək üçün istifadə edilmişdir. Linux RFC 1950 spesifikasiyaları.
Python dilinin bir alt dəsti üçün tərcüməçi də Rust-da yaradıldı və bunun üçün Verus alət dəsti istifadə edərək CPython semantikasına uyğunluğun rəsmi sübutu hazırlandı. Davranışı CPython ilə müqayisə etmək üçün təsadüfi olaraq yaradılan 1.7 milyondan çox Python proqramı icra edildi. Halların 99.95%-də bu proqramların yeni tətbiqetmədə və CPython-da icrasının nəticələri üst-üstə düşdü və aşkar edilən hər hansı uyğunsuzluq məlum kənar hallar idi.
Formal yoxlama spesifikasiyaya uyğunluğu təmin edir, lakin çoxaxınlılıq problemləri, dinamik bağlantı və real aparat təminatında anomal davranışın yaratdığı risklər qeyri-rəsmi olaraq qaldığı üçün təhlükəsizlik problemlərini tamamilə aradan qaldırmır. Təklif olunan yanaşmanın əsas üstünlüyü ondan ibarətdir ki, o, birbaşa ikili fayllarla işləyir və mövcud kodu rəsmi olaraq təsdiqlənə bilən dillərdə yenidən yazmaq ehtiyacını aradan qaldırır.
Mənbə: opennet.ru
