W ramach naszych eksperymentów z wykorzystaniem sztucznej inteligencji do audytowania systemów kryptograficznych, skierowaliśmy nasze narzędzie zkao na OpenVM – środowisko typu zkVM (Zero-Knowledge Virtual Machine). Nasze działania doprowadziły do wykrycia krytycznego błędu w bibliotece openvm-pairing, który pozwalał złośliwemu dowodzącemu (prover) na sfałszowanie dowolnej równości parowań. Warto zaznaczyć, że problem nie dotyczył samego systemu dowodzenia zkVM, lecz konkretnej implementacji biblioteki. Błąd został zarejestrowany pod numerem CVE-2026-46669 i naprawiony w wersji 1.6.0 systemu OpenVM.
Wyzwania w automatyzacji audytów zkVM
Nasze wcześniejsze próby skanowania OpenVM przy użyciu standardowych modeli językowych (LLM) nie przyniosły sukcesu. Choć modele te potrafiły wskazać potencjalne problemy, żadne z nich nie było podatne na rzeczywiste wykorzystanie. Hipoteza badawcza wskazywała, że złożoność zkVM przekracza możliwości standardowych modeli, nawet przy dużym oknie kontekstowym. W przeciwieństwie do typowych bibliotek, gdzie moduły można audytować w izolacji, w przypadku zkVM zależności między komponentami są niezwykle gęste. Bezpieczne moduły A i B połączone razem mogą tworzyć lukę, dlatego audyt wymaga zrozumienia założeń i niezmienników, a nie tylko analizy pojedynczych linii kodu.
Zastosowanie zkao, naszego wyspecjalizowanego narzędzia, pozwoliło na przełamanie tej bariery. Po ponad dziewięciu godzinach skanowania, zkao zidentyfikowało krytyczny błąd w mechanizmie sprawdzania parowań. Poniżej przedstawiamy szczegóły wykrytej luki:
Mechanizm błędu w weryfikacji parowań
Parowania stanowią fundament wielu protokołów, takich jak Groth16, PLONK z KZG czy podpisy BLS. Weryfikator sprawdza, czy iloczyn parowań jest równy jedności. Obliczenie parowania składa się z pętli Millera oraz końcowego potęgowania. Ponieważ końcowe potęgowanie jest kosztowne obliczeniowo, w systemach typu zkVM stosuje się optymalizację, w której dowodzący dostarcza „wskazówkę” (hint) w postaci współczynnika skalowania, co pozwala na sprawdzenie równości znacznie mniejszym kosztem.
Zgodnie z literaturą przedmiotu, aby ta optymalizacja była bezpieczna, współczynnik skalowania musi należeć do odpowiedniego podciała (w tym przypadku Fp6). Błąd w OpenVM polegał na tym, że system sprawdzał jedynie, czy wskazówka nie jest zerem, pomijając weryfikację przynależności do podciała. W efekcie złośliwy użytkownik mógł podstawić własne wartości, które sprawiały, że równanie weryfikacyjne było zawsze spełnione, niezależnie od poprawności oryginalnego parowania.
Skutki i naprawa
Możliwość sfałszowania parowania ma poważne konsekwencje dla bezpieczeństwa systemów opartych na OpenVM:
Naprawa polegała na dodaniu brakującego testu przynależności do podciała. Kod weryfikuje teraz, czy współczynniki o nieparzystych indeksach są równe zeru. Jeśli współczynnik skalowania nie spełnia tego warunku, system odrzuca dowód, co skutecznie eliminuje możliwość przeprowadzenia ataku. Koszt naprawy w przeliczeniu na złotówki jest pomijalny w porównaniu do potencjalnych strat, a sama poprawka została wdrożona w wersji 1.6.0.
To doświadczenie potwierdziło, że automatyzacja audytów kryptograficznych wymaga nie tylko mocy obliczeniowej, ale przede wszystkim głębokiego osadzenia narzędzi AI w wiedzy eksperckiej i literaturze naukowej. Nasz proces triażu, który ewoluował w stronę eliminacji fałszywych alarmów, pozostaje kluczowym elementem pracy nad bezpieczeństwem systemów typu zkVM.
