Anthropic-ը ներկայացրեց արհեստական բանականության մոդելների օգտագործմամբ փորձերի արդյունքները՝ գոյություն ունեցող նախագծերի հուսալիությունն ու անվտանգությունը պաշտոնապես ստուգելու համար: Փորձի ընթացքում արհեստական բանականության մոդելներն օգտագործվել են OSS Fuzz ենթակառուցվածքում փորձարկված 123 բաց կոդով գրադարանների հիշողության սխալների բացակայության մաթեմատիկական ապացույցներ ստեղծելու համար:
Ստուգումը կատարվել է RISC-V ճարտարապետության համար կազմված ասեմբլեր կոդի մակարդակով: Ստեղծված ապացույցների ընդհանուր ծավալը կազմել է Rocq Prover ստուգման համակարգի համար մոտավորապես 180 միլիոն տող կոդ (մոտավորապես 600 տող յուրաքանչյուր երկուական ֆայլում՝ 18 RISC-V հրահանգներով): Ապացույցները ստեղծվել են առկա fuzzing թեստերը ավտոմատ կերպով փոխակերպելով ֆորմալ սպեցիֆիկացիաների, որից հետո Claude AI մոդելը ապացուցել է, որ ծրագիրը անթերի է մինչև 64 ՄԲ ցանկացած մուտքային տվյալների համար:
Ապացույցների կառուցման գործընթացի ընթացքում արհեստական բանականության մոդելը կարողացավ նույնականացնել և պատրաստել հարյուրավոր սխալների ուղղումներ, որոնք նախկինում չէին հայտնաբերվել fuzz թեստավորման միջոցով: Այլ բաների շարքում, դրանց թվում էին բուֆերի արտահոսքի խոցելիությունները որոշակի մուտքային տվյալների մշակման ժամանակ (օրինակ՝ CVE-2026-56132 libexpat-ում), ինչպես նաև տրամաբանական սխալները: Ավելին, արհեստական բանականության մոդելն օգտագործվել է միջուկի կողմից zlib ալգորիթմի իրականացման համապատասխանությունը ապացուցելու համար: Linux RFC 1950 տեխնիկական բնութագրերը։
Rust-ում Python-ի ենթաբազմության համար նույնպես ստեղծվեց մեկնաբան, որի համար Verus գործիքակազմի միջոցով պատրաստվեց CPython-ի սեմանտիկայի հետ համապատասխանության պաշտոնական ապացույց: CPython-ի հետ վարքագիծը համեմատելու համար կատարվել է ավելի քան 1.7 միլիոն պատահականորեն ստեղծված Python ծրագրեր: Դեպքերի 99.95%-ում այս ծրագրերի կատարման արդյունքները նոր իրականացման մեջ և CPython-ում համընկնում էին, և հայտնաբերված բոլոր անհամապատասխանությունները հայտնի եզրային դեպքեր էին:
Ֆորմալ ստուգումը երաշխավորում է սպեցիֆիկացիաների համապատասխանությունը, սակայն այն ամբողջությամբ չի վերացնում անվտանգության խնդիրները, քանի որ բազմաշերտ խնդիրների, դինամիկ կապի և իրական սարքավորումների վրա աննորմալ վարքագծի հետևանքով առաջացած ռիսկերը մնում են չֆորմալացված։ Առաջարկվող մոտեցման հիմնական առավելությունն այն է, որ այն աշխատում է անմիջապես երկուական ֆայլերի հետ՝ վերացնելով գոյություն ունեցող կոդը ֆորմալ ստուգելի լեզուներով վերաշարադրելու անհրաժեշտությունը։
Source: opennet.ru
