Dowód braku awarii w 123 bibliotekach nie ocenia wymagań

Formalna weryfikacja oprogramowania to dowód matematyczny, że program zawsze spełnia ustalone reguły. Anthropic, twórca czatu Claude, opisał 22 października takie dowody dla 123 bibliotek, czyli gotowych fragmentów kodu używanych przez inne programy. Według wpisu Claude najpierw naprawił znalezione błędy, a potem udowodnił, że 239 punktów wejścia, czyli funkcji wywoływanych z zewnątrz, nie ulega awarii przy danych do 64 MB.

Test sprawdza wybrane przypadki, a to, czego nie wypróbowano, pozostaje niewiadomą. Dowód obejmuje cały zadany zakres naraz. Według Anthropic programiści zamieniają w tym celu kod na model matematyczny i dowodzą, że spełnia on zasady bezpieczeństwa.

Dowód dotyczy 239 punktów wejścia w 123 bibliotekach z OSS-Fuzz, projektu sprawdzającego biblioteki otwartego oprogramowania losowymi danymi, czyli fuzzingiem. Obowiązuje dla danych do 64 MB.

Dowody zapisano w języku Rocq, przeznaczonym do zapisu dowodów matematycznych. Ich poprawność sprawdza program kontrolny. Według Anthropic zaufać trzeba trzem rzeczom: modelom matematycznym procesora RISC-V (rodzaju procesora, dla którego skompilowano badane programy) i procesów Linuksa, dokładnemu brzmieniu udowodnionych twierdzeń oraz samemu programowi kontrolnemu.

Samo próbowanie dowodzenia wykryło, jak podaje Anthropic, setki błędów. Dokładnej liczby wpis nie podaje. Jeden przykład: w swojej kopii dekompresora, czyli programu rozpakowującego dane, Claude znalazł błąd prowadzący do zapisu poza przydzieloną pamięcią. Ujawniał się tylko przy danych o rozmiarze około 20 MB i jednym rzadkim układzie.

Część błędów nie powoduje awarii w ogóle. Przy dowodzie, że jedna z bibliotek nie robi błędów pamięci, Claude zauważył, że funkcja ograniczająca, jakie pliki program może wczytać, nie zawsze jest egzekwowana. Wpis opisuje też nieznany wcześniej błąd logiczny, ukryty w kodzie ponad dziesięć lat.

Przy próbie weryfikacji czytnika plików PDF zespół znalazł w tydzień tyle błędów bezpieczeństwa, ile zwykle zgłasza się w ciągu roku. Wpis określa program tylko jako powszechnie używany. Wśród opisanych błędów jest ponowne odkrycie znanej luki o numerze CVE-2026-56132 (numer w publicznym rejestrze luk) w libexpat, bibliotece do czytania plików XML. Red Hat, dostawca Linuksa dla firm, opisuje ją jako przepełnienie bufora na stercie, czyli zapis danych poza przydzieloną pamięcią.

Drobne błędy, niemożliwe do wykorzystania w ataku, z sześciu innych powszechnie używanych bibliotek są według wpisu w trakcie zgłaszania autorom. Wpis publikuje podzbiór dowodów do samodzielnego sprawdzenia.

„Formalnie zweryfikowany” nie znaczy „bez błędów”, zastrzega Anthropic. Program kontrolny potwierdza, że skompilowany program spełnia zapis wymagań. Zgodności zapisu z rzeczywistością nie sprawdza.

Dowody mają założenia. Program jest jednowątkowy, czyli robi jedną rzecz naraz, jest statycznym plikiem wykonywalnym, czyli programem w jednym kawałku, ma stały budżet pamięci i działa na procesorze RISC-V pod Linuksem.

Brak awarii to jedna właściwość z wielu możliwych. Anthropic sam pisze, że do naprawienia wszystkich możliwych błędów jest jeszcze daleko. Program może nie ulegać awarii i mimo to robić coś niewłaściwego, jak przy niewymuszanym ograniczeniu plików. Według serwisu Developers Digest słaby zestaw uruchamiający badaną funkcję pozbawia dowód treści.

Theorem współpracuje z Anthropic przy tym projekcie. We wpisie z 29 września pisał, że przegląd wykonywany przez człowieka powinien rosnąć ze złożonością zamierzonego zachowania oprogramowania. Theorem oferuje też uruchomienie procesu dla innych projektów otwartego oprogramowania, a według serwisu The Decoder jego plan obejmuje między innymi OpenSSL, bibliotekę szyfrującą połączenia w sieci.

Według serwisu The Decoder Anthropic spodziewa się, że formalna weryfikacja z AI wkrótce stanie się tak praktyczna jak zwykłe testowanie. Jeśli to się sprawdzi, deklaracje „sprawdzone formalnie” będą padać częściej.