Anthropic компаниясы қолданыстағы жобалардың сенімділігі мен қауіпсіздігін ресми түрде тексеру үшін жасанды интеллект модельдерін пайдаланып жүргізілген тәжірибелердің нәтижелерін ұсынды. Тәжірибе барысында OSS Fuzz инфрақұрылымында сыналған 123 ашық бастапқы кодты кітапхана үшін жад қателерінің жоқтығының математикалық дәлелдерін жасау үшін жасанды интеллект модельдері пайдаланылды.
Тексеру RISC-V архитектурасы үшін компиляцияланған ассемблер коды деңгейінде жүргізілді. Жасалған дәлелдемелердің жалпы көлемі Rocq Prover тексеру жүйесі үшін шамамен 180 миллион жол кодын құрады (18 000 RISC-V нұсқаулары бар екілік файлға шамамен 600 000 жол). Дәлелдемелер бар фуззинг сынақтарын ресми сипаттамаларға автоматты түрде түрлендіру арқылы жасалды, содан кейін Claude AI моделі бағдарламаның 64 МБ дейінгі кез келген кіріс деректері үшін ақаусыз екенін дәлелдеді.
Дәлелдеу процесінде жасанды интеллект моделі бұрын fuzz тестілеуі арқылы анықталмаған жүздеген қателерді анықтап, түзетулер дайындай алды. Басқа нәрселермен қатар, бұларға белгілі бір кіріс деректерін өңдеу кезінде буфердің толып кету осалдықтары (мысалы, libexpat ішіндегі CVE-2026-56132), сондай-ақ логикалық қателер кірді. Сонымен қатар, жасанды интеллект моделі ядроның zlib алгоритмін іске асыруының сәйкестігін дәлелдеу үшін пайдаланылды. Linux RFC 1950 сипаттамалары.
Python тілінің ішкі жиынына арналған интерпретатор Rust бағдарламасында да жасалды, ол үшін Verus құралдар жинағын пайдаланып CPython семантикасына сәйкестіктің ресми дәлелі дайындалды. CPython-мен мінез-құлықты салыстыру үшін кездейсоқ түрде жасалған 1.7 миллионнан астам Python бағдарламалары орындалды. 99.95% жағдайда бұл бағдарламаларды жаңа іске асыруда және CPython бағдарламасында орындау нәтижелері сәйкес келді, ал табылған кез келген сәйкессіздіктер белгілі шеткі жағдайлар болды.
Ресми тексеру спецификацияға сәйкестікті кепілдейді, бірақ ол қауіпсіздік мәселелерін толығымен жоймайды, себебі көп ағынды мәселелерден, динамикалық байланыстырудан және нақты аппараттық құралдардағы аномальды мінез-құлықтан туындайтын тәуекелдер бейресми болып қала береді. Ұсынылған тәсілдің негізгі артықшылығы - ол екілік файлдармен тікелей жұмыс істейді, бұл бар кодты ресми түрде тексерілетін тілдерде қайта жазу қажеттілігін жояды.
Ақпарат көзі: opennet.ru
