{"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\/pl\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic rozwija technologie do formalnej weryfikacji istniej\u0105cego oprogramowania za pomoc\u0105 AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Firma Anthropic przedstawi\u0142a wyniki eksperyment\u00f3w dotycz\u0105cych wykorzystania modeli AI do formalnej weryfikacji niezawodno\u015bci i bezpiecze\u0144stwa ju\u017c istniej\u0105cych projekt\u00f3w. W trakcie eksperymentu, przy pomocy modeli AI, stworzono matematyczne dowody braku b\u0142\u0119d\u00f3w zwi\u0105zanych z pami\u0119ci\u0105 dla 123 otwartych bibliotek, przetestowanych w infrastrukturze OSS Fuzz. <\/p>\n
Sprawdzanie przeprowadzono na poziomie skompilowanego kodu assemblerowego dla architektury RISC-V. Ca\u0142kowita obj\u0119to\u015b\u0107 wygenerowanych dowod\u00f3w wynios\u0142a oko\u0142o 180 milion\u00f3w linii kodu dla systemu weryfikacji Rocq Prover (oko\u0142o 600 tysi\u0119cy linii na plik binarny zawieraj\u0105cy 18 tysi\u0119cy instrukcji RISC-V). Dowody formu\u0142owano poprzez automatyczne przekszta\u0142cenie istniej\u0105cych test\u00f3w fuzzingowych w formalne specyfikacje, po czym model AI Claude udowodni\u0142, \u017ce przy dowolnych danych wej\u015bciowych o obj\u0119to\u015bci do 64 MB w programie nie wyst\u0119puj\u0105 awarie. <\/p>\n
W trakcie budowy dowod\u00f3w model AI zdo\u0142a\u0142 zidentyfikowa\u0107 i przygotowa\u0107 poprawki do setek b\u0142\u0119d\u00f3w, kt\u00f3re wcze\u015bniej zosta\u0142y niezauwa\u017cone podczas test\u00f3w fuzzingowych. W\u015br\u00f3d nich zidentyfikowano podatno\u015bci prowadz\u0105ce do przepe\u0142nienia bufora podczas przetwarzania okre\u015blonych danych wej\u015bciowych (na przyk\u0142ad CVE-2026-56132 w libexpat), a tak\u017ce b\u0142\u0119dy logiczne. Dodatkowo, model AI zosta\u0142 wykorzystany do udowodnienia zgodno\u015bci implementacji algorytmu zlib w j\u0105drze Linux z specyfikacj\u0105 RFC 1950.<\/p>\n
Ponadto, w j\u0119zyku Rust wygenerowano interpreter dla podzbioru j\u0119zyka Python, dla kt\u00f3rego za pomoc\u0105 narz\u0119dzi Verus przygotowano formalny dow\u00f3d zgodno\u015bci z semantyk\u0105 CPython. Dla por\u00f3wnania zachowania z CPython przeprowadzono ponad 1,7 miliona losowo wygenerowanych program\u00f3w Python. W 99,95% przypadk\u00f3w wyniki wykonania tych program\u00f3w w nowej implementacji i w CPython by\u0142y identyczne, a zaobserwowane r\u00f3\u017cnice okaza\u0142y si\u0119 znanymi przypadkami granicznymi.<\/p>\n
Przeprowadzona formalna weryfikacja zapewnia zgodno\u015b\u0107 ze specyfikacj\u0105, ale nie eliminuje ca\u0142kowicie problem\u00f3w z bezpiecze\u0144stwem, poniewa\u017c nie wszystkie ryzyka zwi\u0105zane z problemami z wielow\u0105tkowo\u015bci\u0105, dynamicznym wi\u0105zaniem i anormalnym zachowaniem rzeczywistego sprz\u0119tu s\u0105 formalnie uj\u0119te. Kluczow\u0105 zalet\u0105 zaproponowanego podej\u015bcia jest praca bezpo\u015brednio z plikami binarnymi, co pozwala unikn\u0105\u0107 konieczno\u015bci przepisywania istniej\u0105cego kodu na formalnie weryfikowalnych j\u0119zykach. \n \u0179r\u00f3d\u0142o: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"