Anthropic mempresentasikan hasil eksperimen menggunakan model AI untuk memverifikasi secara formal keandalan dan keamanan proyek yang ada. Selama eksperimen, model AI digunakan untuk menghasilkan bukti matematis tentang tidak adanya kesalahan memori untuk 123 pustaka sumber terbuka yang diuji dalam infrastruktur OSS Fuzz.
Verifikasi dilakukan pada tingkat kode assembly yang telah dikompilasi untuk arsitektur RISC-V. Total volume bukti yang dihasilkan berjumlah sekitar 180 juta baris kode untuk sistem verifikasi Rocq Prover (sekitar 600 baris per file biner dengan 18 instruksi RISC-V). Bukti-bukti tersebut dihasilkan dengan secara otomatis mengkonversi tes fuzzing yang ada menjadi spesifikasi formal, setelah itu model AI Claude membuktikan bahwa program tersebut bebas kesalahan untuk data input apa pun hingga 64 MB.
Selama proses pembuktian, model AI mampu mengidentifikasi dan menyiapkan perbaikan untuk ratusan bug yang sebelumnya tidak terdeteksi oleh pengujian fuzz. Antara lain, ini termasuk kerentanan buffer overflow saat memproses data input tertentu (misalnya, CVE-2026-56132 di libexpat), serta kesalahan logika. Lebih lanjut, model AI digunakan untuk membuktikan kesesuaian implementasi kernel terhadap algoritma zlib. Linux Spesifikasi RFC 1950.
Sebuah interpreter untuk subset Python juga dihasilkan dalam Rust, yang bukti formal kesesuaiannya dengan semantik CPython disiapkan menggunakan toolkit Verus. Untuk membandingkan perilaku dengan CPython, lebih dari 1.7 juta program Python yang dihasilkan secara acak dieksekusi. Dalam 99.95% kasus, hasil eksekusi program-program ini dalam implementasi baru dan dalam CPython cocok, dan setiap perbedaan yang ditemukan adalah kasus-kasus khusus yang sudah diketahui.
Verifikasi formal menjamin kepatuhan terhadap spesifikasi, tetapi tidak sepenuhnya menghilangkan masalah keamanan, karena risiko yang disebabkan oleh masalah multithreading, penautan dinamis, dan perilaku anomali pada perangkat keras nyata tetap tidak terformalifikasi. Keunggulan utama dari pendekatan yang diusulkan adalah bahwa pendekatan ini bekerja langsung dengan file biner, sehingga menghilangkan kebutuhan untuk menulis ulang kode yang ada dalam bahasa yang dapat diverifikasi secara formal.
Sumber: opennet.ru
