Anthropic iliwasilisha matokeo ya majaribio kwa kutumia mifumo ya AI ili kuthibitisha rasmi uaminifu na usalama wa miradi iliyopo. Wakati wa jaribio, mifumo ya AI ilitumika kutoa uthibitisho wa hisabati wa kutokuwepo kwa makosa ya kumbukumbu kwa maktaba 123 za chanzo huria zilizojaribiwa katika miundombinu ya OSS Fuzz.
Uthibitishaji ulifanyika katika kiwango cha msimbo wa mkusanyiko uliokusanywa kwa ajili ya usanifu wa RISC-V. Jumla ya kiasi cha uthibitisho uliozalishwa kilifikia takriban mistari milioni 180 ya msimbo kwa ajili ya mfumo wa uthibitishaji wa Rocq Prover (takriban mistari 600 kwa kila faili ya jozi yenye maagizo 18 ya RISC-V). Uthibitisho huo ulitolewa kwa kubadilisha kiotomatiki majaribio yaliyopo ya fuzzing kuwa vipimo rasmi, baada ya hapo modeli ya Claude AI ilithibitisha kuwa programu hiyo haina dosari kwa data yoyote ya kuingiza hadi 64 MB.
Wakati wa mchakato wa kujenga uthibitisho, modeli ya AI iliweza kutambua na kuandaa marekebisho kwa mamia ya hitilafu ambazo hazikugunduliwa hapo awali na upimaji wa fuzz. Miongoni mwa mambo mengine, hizi zilijumuisha udhaifu wa bafa wakati wa kuchakata data fulani ya ingizo (k.m., CVE-2026-56132 katika libexpat), pamoja na makosa ya kimantiki. Zaidi ya hayo, modeli ya AI ilitumika kuthibitisha kufuata utekelezaji wa kernel wa algoriti ya zlib. Linux Vipimo vya RFC 1950.
Mtafsiri wa kikundi kidogo cha Python pia alitengenezwa katika Rust, ambapo uthibitisho rasmi wa kufuata semantiki ya CPython uliandaliwa kwa kutumia zana ya Verus. Ili kulinganisha tabia na CPython, zaidi ya programu milioni 1.7 za Python zilizotengenezwa kwa nasibu zilitekelezwa. Katika 99.95% ya visa, matokeo ya kutekeleza programu hizi katika utekelezaji mpya na katika CPython yalilingana, na tofauti zozote zilizopatikana zilikuwa kesi za ukingo zinazojulikana.
Uthibitishaji rasmi unahakikisha kufuata vipimo, lakini hauondoi kabisa masuala ya usalama, kwani hatari zinazosababishwa na masuala ya uunganishaji wa nyuzi nyingi, uunganishaji unaobadilika, na tabia isiyo ya kawaida kwenye vifaa halisi hubaki bila kurasimishwa. Faida kuu ya mbinu iliyopendekezwa ni kwamba inafanya kazi moja kwa moja na faili za binary, na hivyo kuondoa hitaji la kuandika upya msimbo uliopo katika lugha zinazoweza kuthibitishwa rasmi.
Chanzo: opennet.ru
