Naukowcy Ethereum ścigają się z czasem, by zamknąć lukę bezpieczeństwa zkEVM przed grudniowym terminem

Konkurs Ethereum better.codes przekształcił lukę w kryptograficznym dowodzie w publiczny, odtwarzalny pomiar, który naukowcy mogą przesuwać z obu stron.

21 sierpnia o 15:44:47 UTC na żywej tabeli wyników widniały 63,99-bitowy dolny certyfikat i 116,13-bitowy górny certyfikat dla koalaIRS12. Po dziewięciu promowanych zgłoszeniach od siedmiu solverów między dwiema granicami pozostaje 52,14 bitów nierozstrzygniętych.

KoalaIRS12 to stały profil parametryczny przeplotowej redukcji Reeda–Solomona wykorzystywanej w badaniach nad systemami dowodowymi. Pytania o bliskość Reeda–Solomona tego rodzaju są fundamentalne, a nie poboczne: FRI, czyli Fast Reed–Solomon IOP of Proximity, to technika, której STARK-i i inne oparte na funkcjach skrótu SNARK-i używają do sprawdzania, czy ciąg objęty zobowiązaniem (commitment) leży blisko wielomianu niskiego stopnia. Repozytorium wyzwania definiuje jego wynik jako wielkość kontrolną (spot-check) i wyraźnie wyklucza interpretowanie go jako minus-log2 niezawodności całego systemu albo jako bezpieczeństwa pełnego protokołu. Naukowcy mają teraz publiczną miarę odległości między tym, co wyzwanie udowodniło jako bezpieczne, a tym, co jego górny certyfikat nadal uznaje za niebezpieczne.

Co dowodzi tabela wyników

Konkurs prowadzi dwa tory zaprojektowane tak, aby zamykać przedział z przeciwnych kierunków.

Tor niezawodności (soundness) podnosi dolny certyfikat. Przy certyfikowanym promieniu udane zgłoszenie dowodzi, że wykonywalna granica błędu redukcji benchmarku spełnia zakodowany cel, a następnie odwzorowuje ten promień na wynik wyświetlany w tabeli.

Tor ataku obniża górny certyfikat. Jego twierdzenie certyfikuje niebezpieczny sufiks przy warunku gęstości zbioru wygrywającego benchmarku, a repozytorium obejmuje ten sufiks bezpośrednio, ponieważ formalizacja nie zakłada twierdzenia o monotoniczności gęstości zbioru wygrywającego. Wynik toru górnego certyfikatu opisuje formalną granicę dla koalaIRS12; koszt ataku na Ethereum wymagałby odrębnej analizy całego systemu.

Zgodnie z ogłoszeniem startowym Ethereum Foundation sformułowanie twierdzenia, punkt parametryczny i narzędzie weryfikacyjne (verification harness) są przypięte. Każde zgłoszenie eksportuje wymagane twierdzenie, komparator porównuje to sformułowanie z celem, a jądro Lean weryfikuje dowód przed promocją. Lean to interaktywny system dowodzenia twierdzeń, którego małe, zaufane jądro maszynowo sprawdza każdy krok dowodu. Zaakceptowany wynik dowodzi złożonego twierdzenia wewnątrz tego przypiętego środowiska.

Zapewnienie jakości na poziomie produkcyjnym sięga jednak dalej. Musi również obejmować kompletność modelu, założenia wbudowane w jego definicje, wierność implementacji oraz kompozycję oddzielnie analizowanych komponentów. Majowy przegląd Fundacji dotyczący wysiłku formalnej weryfikacji SP1 — maszyny zkVM opracowanej przez Succinct — pokazuje, dlaczego te dodatkowe warstwy mają znaczenie: specyfikacje i sformułowania twierdzeń są kodem, dane wejściowe i wersje wymagają odtwarzalnego przypinania, a wyniki na poziomie komponentów wymagają szerszego rozumowania, zanim będą mogły wspierać wnioski dotyczące pełnego systemu.

Osobny artykuł naukowy autorstwa Gala Arnona, Dana Boneha i Giacomo Fenziego wskazuje dekodowanie listowe, luki bliskości Reeda–Solomona, zgodność skorelowaną oraz wzajemną zgodność skorelowaną jako otwarte pytania dla zwięzłych systemów dowodowych. Opublikowany przed obecnym zrzutem tabeli wyników wyjaśnia znaczenie tej rodziny problemów, nie oceniając dzisiejszych wyników.

Fundacja przedstawia better.codes jako maszynowo sprawdzaną ścieżkę badawczą dla bezpieczeństwa opartych na funkcjach skrótu SNARK-ów, a doskonalenie certyfikatów koalaIRS12 wyostrzyłoby jedną redukcję w ramach tego programu. Certyfikat 116,13-bitowy ma ten sam ograniczony zasięg: dotyczy punktu parametrycznego zakodowanego w wyzwaniu, podczas gdy inne wybory parametrów, konstrukcje i komponenty systemowe pozostają odrębnymi pytaniami badawczymi.

To właśnie dwustronny format czyni przedział informatywnym. Każda promocja zmienia weryfikowalną granicę, a przypięte twierdzenie sprawia, że kolejne wyniki pozostają porównywalne.

Luka do grudniowego celu Ethereum

Grudniowy harmonogram bezpieczeństwa zkEVM Fundacji z 2025 roku zakładał 128-bitowe udowodnione bezpieczeństwo — poprzeczkę konwencjonalnie odczytywaną jako atak wymagający rzędu 2^128 operacji — wraz z końcowym rozmiarem dowodu 300 KiB lub mniejszym oraz formalnym argumentem niezawodności dla architektury rekurencji. Lutowa aktualizacja sprintu bezpieczeństwa przesunęła termin M3 na początek grudnia 2026 roku i powiązała argument bezpieczeństwa architektury z rezultatem zaplanowanym na 1 grudnia. Harmonogram wymaga od zespołów powiązania granic komponentów z audytowalnym pakietem systemowym.

Dla koalaIRS12 dolny certyfikat osiągający zakodowany cel 128-bitowy rozstrzygnąłby stronę niezawodności benchmarku w jego stałym punkcie parametrycznym. Produkcyjne twierdzenie o zkEVM wymagałoby dodatkowo rozliczenia niezawodności w każdym istotnym komponencie, zgodności z limitem rozmiaru dowodu, udokumentowanej topologii rekurencji, argumentu dotyczącego sposobu łączenia się jego części oraz dowodu, że specyfikacje odpowiadają implementacjom.

Publiczna strona postępów Fundacji, ostatnio zsynchronizowana 20 sierpnia, wymienia wyniki gotowości zkVM i zgodności z ISA oraz wskazuje dowodzenie w czasie rzeczywistym i integrację soundcalc jako kryteria. Jej wyrenderowane tabele nie zawierają znacznika ukończenia pełnego pakietu na początek grudnia i milczą na temat prac śledzonych gdzie indziej.

Majowa aktualizacja dotycząca opcjonalnych dowodów wykonania opisywała fazę niekrytyczną dla konsensusu, w której dowody zkEVM uzupełniają testy mainnetu, podczas gdy zwykłe ponowne wykonywanie przez klientów wykonawczych nadal napędza atestację. Ta opcjonalna rola utrzymuje bezpośredni skutek tabeli wyników w domenie badawczej: ruch certyfikatów zmienia materiał dowodowy dostępny dla przyszłych argumentów bezpieczeństwa, nie zmieniając obecnej krytycznej dla konsensusu ścieżki walidacji Ethereum.

Na better.codes zgłoszenia niezawodności mogą podnosić 63,99-bitowy dolny certyfikat, a zgłoszenia ataku mogą obniżać 116,13-bitowy górny certyfikat. W ramach harmonogramu zkEVM zespoły muszą opublikować rozliczenie na poziomie systemu, rozmiary dowodów, argumenty dotyczące rekurencji i dowody implementacyjne wymagane do przeglądu zaplanowanego na początek grudnia.

Na razie przedział 52,14 bitów pozostaje żywą miarą niedokończonej pracy nad koalaIRS12. Produkcyjny przypadek 128-bitowy Ethereum będzie zależał od tego, jak ten materiał dowodowy dotyczący komponentów wpasuje się w większy dowód.

Źródło: CryptoNews