Firma Anthropic przedstawiła wyniki eksperymentów dotyczących wykorzystania modeli AI do formalnej weryfikacji niezawodności i bezpieczeństwa już istniejących projektów. W trakcie eksperymentu, przy pomocy modeli AI, stworzono matematyczne dowody braku błędów związanych z pamięcią dla 123 otwartych bibliotek, przetestowanych w infrastrukturze OSS Fuzz.
Sprawdzanie przeprowadzono na poziomie skompilowanego kodu assemblerowego dla architektury RISC-V. Całkowita objętość wygenerowanych dowodów wyniosła około 180 milionów linii kodu dla systemu weryfikacji Rocq Prover (około 600 tysięcy linii na plik binarny zawierający 18 tysięcy instrukcji RISC-V). Dowody formułowano poprzez automatyczne przekształcenie istniejących testów fuzzingowych w formalne specyfikacje, po czym model AI Claude udowodnił, że przy dowolnych danych wejściowych o objętości do 64 MB w programie nie występują awarie.
W trakcie budowy dowodów model AI zdołał zidentyfikować i przygotować poprawki do setek błędów, które wcześniej zostały niezauważone podczas testów fuzzingowych. Wśród nich zidentyfikowano podatności prowadzące do przepełnienia bufora podczas przetwarzania określonych danych wejściowych (na przykład CVE-2026-56132 w libexpat), a także błędy logiczne. Dodatkowo, model AI został wykorzystany do udowodnienia zgodności implementacji algorytmu zlib w jądrze Linux z specyfikacją RFC 1950.
Ponadto, w języku Rust wygenerowano interpreter dla podzbioru języka Python, dla którego za pomocą narzędzi Verus przygotowano formalny dowód zgodności z semantyką CPython. Dla porównania zachowania z CPython przeprowadzono ponad 1,7 miliona losowo wygenerowanych programów Python. W 99,95% przypadków wyniki wykonania tych programów w nowej implementacji i w CPython były identyczne, a zaobserwowane różnice okazały się znanymi przypadkami granicznymi.
Przeprowadzona formalna weryfikacja zapewnia zgodność ze specyfikacją, ale nie eliminuje całkowicie problemów z bezpieczeństwem, ponieważ nie wszystkie ryzyka związane z problemami z wielowątkowością, dynamicznym wiązaniem i anormalnym zachowaniem rzeczywistego sprzętu są formalnie ujęte. Kluczową zaletą zaproponowanego podejścia jest praca bezpośrednio z plikami binarnymi, co pozwala uniknąć konieczności przepisywania istniejącego kodu na formalnie weryfikowalnych językach.
Źródło: opennet.ru
