Wprowadzenie

Bezpieczeństwo Bitcoina i innych blockchainów, takich jak Liquid, opiera się na użyciu algorytmów podpisów cyfrowych, takich jak ECDSA i podpisy Schnorra. Biblioteka C o nazwie libsecp256k1, nazwana na cześć krzywej eliptycznej, na której działa, jest używana zarówno przez Bitcoin Core, jak i Liquid, do dostarczania tych algorytmów podpisów cyfrowych. Algorytmy te korzystają z obliczeń matematycznych zwanych odwrotnością modularną, która jest stosunkowo kosztownym składnikiem obliczeń.

W „Szybkiej obliczaniu gcd w stałym czasie i odwrotności modularnej”, Daniel J. Bernstein i Bo-Yin Yang opracowują nowy algorytm odwrotności modularnej. W 2021 roku algorytm ten, określany jako „safegcd”, został zaimplementowany dla libsecp256k1 przez Petera Dettmana. W ramach procesu weryfikacji tego nowego algorytmu, Blockstream Research był pierwszym, który zakończył formalną weryfikację projektu algorytmu, używając asystenta dowodów Coq do formalnej weryfikacji, że algorytm rzeczywiście kończy się poprawnym wynikiem odwrotności modularnej dla 256-bitowych danych wejściowych.

Luka między algorytmem a implementacją

Wysiłek formalizacyjny w 2021 roku pokazał jedynie, że algorytm zaprojektowany przez Bernsteina i Yanga działa poprawnie. Jednak użycie tego algorytmu w libsecp256k1 wymaga implementacji matematycznego opisu algorytmu safegcd w języku programowania C. Na przykład, matematyczny opis algorytmu wykonuje mnożenie macierzy wektorów, które mogą być tak szerokie jak 256-bitowe liczby całkowite ze znakiem, jednak język programowania C zapewnia natywnie jedynie liczby całkowite do 64 bitów (lub 128 bitów z niektórymi rozszerzeniami języka).

Implementacja algorytmu safegcd wymaga programowania mnożenia macierzy i innych obliczeń za pomocą 64-bitowych liczb całkowitych w C. Dodatkowo, wprowadzono wiele innych optymalizacji, aby przyspieszyć implementację. Ostatecznie w libsecp256k1 znajdują się cztery oddzielne implementacje algorytmu safegcd: dwa algorytmy o stałym czasie dla generacji podpisów, jeden zoptymalizowany dla systemów 32-bitowych i jeden zoptymalizowany dla systemów 64-bitowych, oraz dwa algorytmy o zmiennym czasie dla weryfikacji podpisów, znów jeden dla systemów 32-bitowych i jeden dla systemów 64-bitowych.

Verifiable C

Aby zweryfikować, że kod C poprawnie implementuje algorytm safegcd, muszą zostać sprawdzone wszystkie szczegóły implementacji. Używamy Verifiable C, części Weryfikowanego Zestawu Narzędzi Oprogramowania, do rozumowania o kodzie C z użyciem prover'a twierdzeń Coq.

Weryfikacja postępuje poprzez określenie warunków wstępnych i końcowych przy użyciu logiki separacyjnej dla każdej funkcji poddawanej weryfikacji. Logika separacyjna to logika specjalizowana do rozumowania o podprogramach, alokacjach pamięci, współbieżności i nie tylko.

Gdy każdej funkcji przypisana jest specyfikacja, weryfikacja postępuje od warunku wstępnego funkcji i ustala nową inwariantę po każdym zdaniu w ciele funkcji, aż do ostatecznego ustalenia warunku końcowego na końcu ciała funkcji lub na końcu każdego wyrażenia return. Większość wysiłku formalizacyjnego spędza się „pomiędzy” liniami kodu, wykorzystując inwarianty do przetłumaczenia surowych operacji każdego wyrażenia C na wyższe poziomy stwierdzeń o tym, co reprezentują manipulowane struktury danych matematycznie. Na przykład, to co język C uważa za tablicę 64-bitowych liczb całkowitych, może być w rzeczywistości reprezentacją 256-bitowej liczby całkowitej.

Ostatecznym wynikiem jest formalny dowód, zweryfikowany przez asystenta dowodów Coq, że 64-bitowa implementacja algorytmu odwrotności modularnej safegcd w libsecp256k1 jest funkcjonalnie poprawna.

Ograniczenia weryfikacji

Istnieją pewne ograniczenia dotyczące dowodu poprawności funkcjonalnej. Logika separacyjna użyta w Verifiable C implementuje to, co nazywa się poprawnością częściową. Oznacza to, że udowadnia jedynie, że kod C zwraca poprawny wynik, jeśli zwraca, ale nie udowadnia samego zakończenia. Łagodzimy to ograniczenie, korzystając z naszego wcześniejszego dowodu Coq dotyczącego granic algorytmu safegcd, aby udowodnić, że wartość licznika pętli głównej w rzeczywistości nigdy nie przekracza 11 iteracji.

Innym problemem jest to, że sam język C nie ma formalnej specyfikacji. Zamiast tego projekt Verifiable C wykorzystuje projekt kompilatora CompCert do dostarczenia formalnej specyfikacji języka C. Gwarantuje to, że gdy zweryfikowany program C jest kompilowany za pomocą kompilatora CompCert, powstały kod asemblera spełni swoją specyfikację (z zastrzeżeniem powyższego ograniczenia). Jednak nie gwarantuje to, że kod generowany przez GCC, clang lub jakikolwiek inny kompilator będzie działał. Na przykład kompilatory C mogą mieć różne kolejności ewaluacji argumentów w ramach wywołania funkcji. A nawet jeśli język C miałby formalną specyfikację, każdy kompilator, który nie jest formalnie zweryfikowany, mógłby nadal źle kompilować programy. Tak się dzieje w praktyce.

Na koniec, Verifiable C nie wspiera przekazywania struktur, zwracania struktur ani przypisywania struktur. Chociaż w libsecp256k1 struktury są zawsze przekazywane przez wskaźnik (co jest dozwolone w Verifiable C), są pewne przypadki, w których używana jest przypisanie struktur. W przypadku dowodu poprawności odwrotności modularnej, było 3 przypisania, które musiały zostać zastąpione specjalizowanym wywołaniem funkcji, które wykonuje przypisanie struktury pole po polu.

Podsumowanie

Blockstream Research formalnie zweryfikował poprawność funkcji odwrotności modularnej libsecp256k1. Praca ta dostarcza dalszych dowodów na to, że weryfikacja kodu C jest możliwa w praktyce. Użycie ogólnego asystenta dowodów pozwala nam weryfikować oprogramowanie zbudowane na złożonych argumentach matematycznych.

Nic nie uniemożliwia weryfikacji pozostałych funkcji zaimplementowanych w libsecp256k1. Dlatego możliwe jest, aby libsecp256k1 uzyskał najwyższe możliwe gwarancje poprawności oprogramowania.

To jest gościnny post autorstwa Russella O’Connora i Andrew Poelstry. Wyrażone opinie są wyłącznie ich własnymi i niekoniecznie odzwierciedlają te z BTC Inc lub Bitcoin Magazine.

Źródło: Bitcoin Magazine

Post Safegcd’s Implementation Formally Verified pojawił się po raz pierwszy w Crypto Breaking News.