Az Anthropic c\u00e9g bemutatta az AI-modellek haszn\u00e1lat\u00e1nak k\u00eds\u00e9rleteinek eredm\u00e9nyeit, amelyek c\u00e9lja a megl\u00e9v\u0151 projektek megb\u00edzhat\u00f3s\u00e1g\u00e1nak \u00e9s biztons\u00e1g\u00e1nak form\u00e1lis verifik\u00e1ci\u00f3ja. A k\u00eds\u00e9rlet sor\u00e1n AI-modellek seg\u00edts\u00e9g\u00e9vel 123 ny\u00edlt forr\u00e1sk\u00f3d\u00fa k\u00f6nyvt\u00e1rra gener\u00e1ltak matematikai bizony\u00edt\u00e9kokat a mem\u00f3riahaszn\u00e1lat hib\u00e1inak hi\u00e1ny\u00e1r\u00f3l az OSS Fuzz infrastrukt\u00far\u00e1j\u00e1ban. <\/p>\n
A tesztel\u00e9s a RISC-V architekt\u00fara bin\u00e1ris assembler k\u00f3d szintj\u00e9n t\u00f6rt\u00e9nt. A gener\u00e1lt bizony\u00edt\u00e9kok \u00f6sszterjedelme k\u00f6r\u00fclbel\u00fcl 180 milli\u00f3 k\u00f3dsor volt a Rocq Prover verifik\u00e1ci\u00f3s rendszer sz\u00e1m\u00e1ra (k\u00f6r\u00fclbel\u00fcl 600 ezer sor egy 18 ezer RISC-V utas\u00edt\u00e1st tartalmaz\u00f3 bin\u00e1ris f\u00e1jlhoz). A bizony\u00edt\u00e9kokat a megl\u00e9v\u0151 fuzzing tesztek automatikus \u00e1talak\u00edt\u00e1s\u00e1val form\u00e1lis specifik\u00e1ci\u00f3kk\u00e1 hozt\u00e1k l\u00e9tre, majd a Claude AI-modell bizony\u00edtotta, hogy b\u00e1rmilyen 64 MB-ig terjed\u0151 bemenet eset\u00e9n a program nem omlik \u00f6ssze. <\/p>\n
A bizony\u00edt\u00e9kok fel\u00e9p\u00edt\u00e9se sor\u00e1n az AI-modell k\u00e9pes volt azonos\u00edtani \u00e9s jav\u00edt\u00e1sokat el\u0151k\u00e9sz\u00edteni sz\u00e1mos hiba sz\u00e1m\u00e1ra, amelyeket kor\u00e1bban nem \u00e9szleltek a fuzzing tesztel\u00e9s sor\u00e1n. T\u00f6bbek k\u00f6z\u00f6tt, felfedeztek sebezhet\u0151s\u00e9geket, amelyek a puffer t\u00falcsordul\u00e1s\u00e1hoz vezethetnek bizonyos bemeneti adatok feldolgoz\u00e1sa sor\u00e1n (p\u00e9ld\u00e1ul CVE-2026-56132 a libexpat-ben), valamint logikai hib\u00e1kat. Emellett az AI-modellt a Linux kernel zlib algoritmus\u00e1nak RFC 1950 specifik\u00e1ci\u00f3hoz val\u00f3 megfelel\u0151s\u00e9g\u00e9nek bizony\u00edt\u00e1s\u00e1ra is haszn\u00e1lt\u00e1k.<\/p>\n
Rust nyelven egy interpret\u00e1tort gener\u00e1ltak a Python nyelv egy r\u00e9szhalmaz\u00e1hoz, amelyhez a Verus eszk\u00f6zk\u00e9szlet\u00e9vel form\u00e1lis bizony\u00edt\u00e9kot k\u00e9sz\u00edtettek a CPython szemin\u00e1rium\u00e1nak val\u00f3 megfelel\u00e9sr\u0151l. A CPython-nal val\u00f3 viselked\u00e9s \u00f6sszehasonl\u00edt\u00e1sa \u00e9rdek\u00e9ben t\u00f6bb mint 1,7 milli\u00f3 v\u00e9letlenszer\u0171en gener\u00e1lt Python program futott. Az esetek 99,95%-\u00e1ban ezeknek a programoknak az \u00faj v\u00e9grehajt\u00e1si eredm\u00e9nyei \u00e9s a CPython egyeztek, a felfedezett elt\u00e9r\u00e9sek pedig ismert hat\u00e1rhesseket mutattak.<\/p>\n
A form\u00e1lis verifik\u00e1ci\u00f3 garant\u00e1lja a specifik\u00e1ci\u00f3knak val\u00f3 megfelel\u00e9st, de nem z\u00e1rja ki teljesen a biztons\u00e1gi probl\u00e9m\u00e1k megjelen\u00e9s\u00e9t, mivel a p\u00e1rhuzamos programoz\u00e1s, a dinamikus linking \u00e9s a val\u00f3s hardver anom\u00e1li\u00e1inak eredm\u00e9nyek\u00e9nt felmer\u00fcl\u0151 kock\u00e1zatok nincsenek formailag \u00e9rv\u00e9nyes\u00edtve. Az aj\u00e1nlott megk\u00f6zel\u00edt\u00e9s kulcsfontoss\u00e1g\u00fa el\u0151nye, hogy k\u00f6zvetlen\u00fcl a bin\u00e1ris f\u00e1jlokkal dolgozik, \u00edgy elker\u00fclhet\u0151 a megl\u00e9v\u0151 k\u00f3d \u00e1t\u00edr\u00e1sa form\u00e1lisan verifik\u00e1lhat\u00f3 nyelveken. \n Forr\u00e1s: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"