Anthropic ar Claude palīdzību formāli pierāda drošības īpašības 123 atvērtā koda bibliotēkās

MI uzņēmums Anthropic 22. oktobrī publicēja pētījumu, kurā kopā ar jaunuzņēmumu Theorem izmantoja modeli Claude, lai formāli pierādītu programmatūras drošības īpašības. Uzņēmuma ziņojumā teikts, ka Claude izveidoja pierādījumus 239 ieejas punktiem, ko izmanto testēšanā ar nejauši ģenerētiem ievades datiem (tā sauktajā fuzzing testēšanā), 123 atvērtā koda bibliotēkās no Google iniciatīvas OSS-Fuzz. Anthropic to sauc par pirmo plaša mēroga mēģinājumu ar MI palīdzību formāli verificēt reāli lietotu programmatūru mašīnkoda līmenī.

Formālā verifikācija nozīmē, ka programmas uzvedība tiek aprakstīta matemātiski un pēc tam pierādīts, ka tā vienmēr ievēro noteiktus noteikumus. Līdz šim šī metode prasīja ļoti daudz specializētu ekspertu darba, tāpēc to lietoja galvenokārt īpaši kritiskās sistēmās. Anthropic kā piemēru min operētājsistēmas kodolu seL4, kura izstrāde aizņēma divus cilvēkgadus, bet verifikācija – 20.

Pētījumā katras bibliotēkas esošais šāds tests tika pārvērsts specifikācijā: testam nav jāavārē ne ar vienu ievadi, kas mazāka par 64 MB. Pierādījumi attiecas uz kompilētām RISC-V programmām un pieņem, ka tās darbojas Linux vidē kā viena pavediena statiski saistītas programmas ar fiksētu atmiņas apjomu. Pierādījumus pārbauda rīks Rocq, tāpēc cilvēkiem tie nav jāpārskata rindu pa rindai. Kopā pieņemto pierādījumu apjoms ir ap 180 miljoniem rindu.

Pierādīšanas laikā Claude atrada arī simtiem kļūdu, no kurām daudzas parastā testēšana visticamāk nepamanītu. Starp tām minēta kļūda dekompresorā, kas izraisīja rakstīšanu ārpus atmiņas robežām tikai ar aptuveni 20 MB lielu ievadi ar retu struktūru, kā arī atkārtoti atrasta jau zināma ievainojamība bibliotēkā libexpat. Modelim ļāva atrastās kļūdas izlabot un pēc tam pierādīt jau labotā koda drošību.

Anthropic uzsver, ka formāli pārbaudīts kods nenozīmē kodu bez kļūdām. Pierādījumi neattiecas uz vairāku pavedienu darbību, kā arī uz x86 vai ARM procesoriem un dinamiski saistītām programmām, uz kurām šīs bibliotēkas lielākoties darbojas. Turklāt nav pārbaudīti visi bibliotēku ieejas punkti, un izmantotais atmiņas kļūdu noteikšanas rīks AddressSanitizer neatklāj visas atmiņas drošības kļūdas.

Uzņēmums publisko daļu pierādījumu un izmantotos RISC-V un Linux modeļus, lai tos varētu pārbaudīt neatkarīgi, bet nepublisko pierādījumus, kas varētu atklāt vēl nelabotas kļūdas. Theorem piedāvā to pašu procesu bez maksas piemērot arī citiem atvērtā koda projektiem, un tā tālākais mērķis ir verificēt Nix ekosistēmu, tostarp glibc, OpenSSL un cURL. Anthropic sagaida, ka, modeļiem uzlabojoties, šāda verifikācija kļūs lētāka un plašāk pieejama.