Anthropic mavjud loyihalarning ishonchliligi va xavfsizligini rasman tekshirish uchun AI modellaridan foydalangan holda o'tkazilgan tajribalar natijalarini taqdim etdi. Tajriba davomida OSS Fuzz infratuzilmasida sinovdan o'tgan 123 ta ochiq kodli kutubxonalar uchun xotira xatolarining yo'qligining matematik isbotlarini yaratish uchun AI modellaridan foydalanildi.
Tekshirish RISC-V arxitekturasi uchun kompilyatsiya qilingan assembler kodi darajasida amalga oshirildi. Yaratilgan isbotlarning umumiy hajmi Rocq Prover tekshirish tizimi uchun taxminan 180 million kod satrini tashkil etdi (har bir ikkilik fayl uchun taxminan 600 000 satr, 18 000 ta RISC-V ko'rsatmalari bilan). Isbotlar mavjud fuzzing testlarini rasmiy spetsifikatsiyalarga avtomatik ravishda o'zgartirish orqali yaratildi, shundan so'ng Claude AI modeli dasturning 64 MB gacha bo'lgan har qanday kirish ma'lumotlari uchun xatosiz ekanligini isbotladi.
Isbot yaratish jarayonida AI modeli ilgari fuzz testi orqali aniqlanmagan yuzlab xatolarni aniqlay oldi va tuzatishlarni tayyorlay oldi. Boshqa narsalar qatorida, bularga ma'lum kirish ma'lumotlarini (masalan, libexpatdagi CVE-2026-56132) qayta ishlashda buferning toshib ketishi bilan bog'liq zaifliklar, shuningdek, mantiqiy xatolar kiradi. Bundan tashqari, AI modeli yadroning zlib algoritmini amalga oshirishga mos kelishini isbotlash uchun ishlatilgan. Linux RFC 1950 texnik xususiyatlari.
Pythonning bir qismi uchun tarjimon ham Rustda yaratildi, buning uchun Verus asboblar to'plami yordamida CPython semantikasiga muvofiqlikning rasmiy isboti tayyorlandi. CPython bilan xatti-harakatlarni taqqoslash uchun 1.7 milliondan ortiq tasodifiy yaratilgan Python dasturlari bajarildi. 99.95% hollarda, ushbu dasturlarni yangi amalga oshirishda va CPythonda bajarish natijalari mos keldi va topilgan har qanday nomuvofiqliklar ma'lum chekka holatlar edi.
Rasmiy tekshirish spetsifikatsiyaga muvofiqlikni kafolatlaydi, ammo bu xavfsizlik muammolarini to'liq bartaraf etmaydi, chunki ko'p oqimli muammolar, dinamik bog'lanish va haqiqiy apparatdagi anomal xatti-harakatlar tufayli yuzaga keladigan xavflar rasmiylashtirilmaganligicha qolmoqda. Taklif qilinayotgan yondashuvning asosiy afzalligi shundaki, u to'g'ridan-to'g'ri ikkilik fayllar bilan ishlaydi va mavjud kodni rasmiy tekshiriladigan tillarda qayta yozish zaruratini yo'q qiladi.
Manba: opennet.ru
