„Anthropic“ pristatė eksperimentų, atliktų naudojant dirbtinio intelekto modelius, rezultatus, siekiant formaliai patikrinti esamų projektų patikimumą ir saugumą. Eksperimento metu dirbtinio intelekto modeliai buvo naudojami matematiniams atminties klaidų nebuvimo įrodymams generuoti 123 atvirojo kodo bibliotekose, išbandytose OSS Fuzz infrastruktūroje.
Patikrinimas buvo atliktas kompiliuoto asemblerio kodo lygmeniu RISC-V architektūrai. Bendras sugeneruotų įrodymų kiekis sudarė maždaug 180 milijonų kodo eilučių, skirtų „Rocq Prover“ patikros sistemai (maždaug 600 000 eilučių dvejetainiame faile su 18 000 RISC-V instrukcijų). Įrodymai buvo sugeneruoti automatiškai konvertuojant esamus apytikslio suliejimo testus į formalias specifikacijas, po kurių Claude'o dirbtinio intelekto modelis įrodė, kad programa veikia be klaidų esant bet kokiems įvesties duomenims iki 64 MB.
Įrodymų kūrimo proceso metu dirbtinio intelekto modelis sugebėjo identifikuoti ir paruošti pataisymus šimtams klaidų, anksčiau neaptiktų atliekant „fuzz“ testavimą. Be kita ko, tai apėmė buferio perpildymo pažeidžiamumus apdorojant tam tikrus įvesties duomenis (pvz., CVE-2026-56132 „libexpat“), taip pat logines klaidas. Be to, dirbtinio intelekto modelis buvo naudojamas siekiant įrodyti branduolio zlib algoritmo įgyvendinimo atitiktį. Linux RFC 1950 specifikacijos.
„Rust“ aplinkoje taip pat buvo sugeneruotas „Python“ poaibio interpretatorius, kuriam naudojant „Verus“ įrankių rinkinį buvo parengtas oficialus atitikties CPython semantikai įrodymas. Norint palyginti elgseną su CPython, buvo vykdoma daugiau nei 1.7 milijono atsitiktinai sugeneruotų „Python“ programų. 99.95 % atvejų šių programų vykdymo rezultatai naujoje įgyvendinimo versijoje ir CPython sutapo, o visi rasti neatitikimai buvo žinomi kraštiniai atvejai.
Formalus patikrinimas garantuoja atitiktį specifikacijoms, tačiau jis visiškai nepašalina saugumo problemų, nes daugiasriegiškumo, dinaminio susiejimo ir anomalinio elgesio realioje aparatinėje įrangoje keliama rizika lieka neformalizuota. Pagrindinis siūlomo metodo privalumas yra tas, kad jis veikia tiesiogiai su dvejetainiais failais, todėl nereikia perrašyti esamo kodo formaliai patikrinamomis kalbomis.
Šaltinis: opennet.ru
