{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/ro\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic dezvolt\u0103 tehnici pentru verificarea formal\u0103 a software-ului existent cu ajutorul AI.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Compania Anthropic a prezentat rezultatele experimentelor privind utilizarea modelelor AI pentru verificarea formal\u0103 a fiabilit\u0103\u021bii \u0219i securit\u0103\u021bii proiectelor existente. \u00cen cadrul experimentului, cu ajutorul modelelor AI, au fost generate dovezi matematice privind absen\u021ba erorilor \u00een gestionarea memoriei pentru 123 de biblioteci open-source testate \u00een infrastructura OSS Fuzz. <\/p>\n
Verificarea a fost efectuat\u0103 la nivelul codului de asamblare compilat pentru arhitectura RISC-V. Volumul total de dovezi generate a fost de aproximativ 180 de milioane de linii de cod pentru sistemul de verificare Rocq Prover (aproximativ 600 de mii de linii pentru un fi\u0219ier binar cu 18 mii de instruc\u021biuni RISC-V). Dovezile au fost generate prin transformarea automat\u0103 a testelor existente fuzzing \u00een specifica\u021bii formale, dup\u0103 care modelul AI Claude a demonstrat c\u0103, pentru orice date de intrare de p\u00e2n\u0103 la 64 MB, programul nu sufer\u0103 e\u0219ecuri. <\/p>\n
\u00cen procesul de construire a dovezilor, modelul AI a reu\u0219it s\u0103 identifice \u0219i s\u0103 preg\u0103teasc\u0103 remedieri pentru sute de erori, care anterior nu fuseser\u0103 observate \u00een testarea fuzzing. Printre altele, au fost identificate vulnerabilit\u0103\u021bi care duc la dep\u0103\u0219irea buffer-ului la procesarea anumitor date de intrare (de exemplu, CVE-2026-56132 \u00een libexpat), precum \u0219i erori logice. \u00cen plus, modelul AI a fost utilizat pentru a demonstra conformitatea implement\u0103rii algoritmului zlib \u00een nucleul Linux cu specifica\u021bia RFC 1950.<\/p>\n
De asemenea, un interpret pe limbajul Rust a fost generat pentru un subset al limbajului Python, pentru care, cu ajutorul instrumentului Verus, a fost preg\u0103tit\u0103 o dovad\u0103 formal\u0103 a conformit\u0103\u021bii cu semantica CPython. Pentru a compara comportamentele cu CPython, au fost efectuate peste 1,7 milioane de programe Python generate aleatoriu. \u00cen 99,95% din cazuri, rezultatele execu\u021biei acestor programe \u00een noua implementare \u0219i \u00een CPython s-au coincis, iar discrepan\u021bele observate s-au dovedit a fi cazuri limit\u0103 cunoscute.<\/p>\n
Verificarea formal\u0103 efectuat\u0103 garanteaz\u0103 conformitatea cu specifica\u021bia, dar nu elimin\u0103 complet apari\u021bia problemelor de securitate, deoarece riscurile cauzate de problemele de multitasking, legarea dinamic\u0103 \u0219i comportamentul anormal al echipamentului real r\u0103m\u00e2n neachitate. Principalul avantaj al abord\u0103rii propuse este lucrul direct cu fi\u0219ierele binare, ceea ce elimin\u0103 necesitatea de a rescrie codul existent \u00een limbaje formal verificate. \n Sursa: opennet.ro<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"