Úvod

Bezpečnost Bitcoinu a dalších blockchainů, jako je Liquid, závisí na použití algoritmů digitálních podpisů, jako jsou ECDSA a Schnorr podpisy. Knihovna C nazvaná libsecp256k1, pojmenovaná podle eliptické křivky, na které knihovna pracuje, je používána jak Bitcoin Core, tak Liquid, k poskytování těchto algoritmů digitálních podpisů. Tyto algoritmy využívají matematický výpočet nazývaný modulární inverze, což je relativně nákladná součást výpočtu.

V článku „Rychlé výpočty gcd s konstantním časem a modulární inverze“ vyvinuli Daniel J. Bernstein a Bo-Yin Yang nový algoritmus pro modulární inverzi. V roce 2021 byl tento algoritmus, označovaný jako „safegcd“, implementován pro libsecp256k1 Peterem Dettmanem. Jako součást procesu schvalování tohoto nového algoritmu byla Blockstream Research první, kdo dokončil formální ověření návrhu algoritmu pomocí asistenta pro důkaz Coq, aby formálně ověřil, že algoritmus skutečně končí s správným výsledkem modulární inverze na 256bitových vstupech.

Mezera mezi algoritmem a implementací

Úsilí o formalizaci v roce 2021 ukázalo pouze to, že algoritmus navržený Bernsteinem a Yangem funguje správně. Nicméně použití tohoto algoritmu v libsecp256k1 vyžaduje implementaci matematického popisu algoritmu safegcd v jazyce C. Například matematický popis algoritmu provádí maticovou multiplicaci vektorů, které mohou mít šířku až 256 bitových celých čísel, nicméně jazyk C poskytuje nativně pouze celá čísla až do 64 bitů (nebo 128 bitů s některými rozšířeními jazyka).

Implementace algoritmu safegcd vyžaduje programování maticové multiplicace a dalších výpočtů pomocí 64bitových celých čísel jazyka C. Kromě toho byla přidána řada dalších optimalizací, aby byla implementace rychlá. Nakonec existují čtyři samostatné implementace algoritmu safegcd v libsecp256k1: dva algoritmy s konstantním časem pro generaci podpisů, jeden optimalizovaný pro 32bitové systémy a jeden optimalizovaný pro 64bitové systémy, a dva algoritmy s proměnlivým časem pro ověřování podpisů, opět jeden pro 32bitové systémy a jeden pro 64bitové systémy.

Ověřitelný C

Aby bylo možné ověřit, že kód C správně implementuje algoritmus safegcd, musí být zkontrolovány všechny detaily implementace. Používáme Verifiable C, což je součást ověřeného softwarového nástroje pro uvažování o kódu C pomocí Teorem Prover Coq.

Ověřování probíhá specifikováním preconditions a postconditions pomocí separační logiky pro každou funkci, která podléhá ověření. Separační logika je logika specializovaná na uvažování o podprogramových rutinách, alokacích paměti, souběžnosti a dalším.

Jakmile je každé funkci přidělena specifikace, ověřování probíhá od precondition funkce a vytváří novou invariantní hodnotu po každém příkazu v těle funkce, až nakonec ustanoví post podmínku na konci těla funkce nebo na konci každého návratového příkazu. Většina úsilí o formální úpravu se vynakládá „mezi“ řádky kódu, používající invarianty k překladu surových operací každého výrazu C do vyšších úrovní prohlášení o tom, co datové struktury, se kterými se manipuluje, představují matematicky. Například to, co jazyk C považuje za pole 64bitových celých čísel, může ve skutečnosti být reprezentací 256bitového celého čísla.

Konečným výsledkem je formální důkaz, ověřený pomocí asistenta pro důkaz Coq, že 64bitová variabilní časová implementace algoritmu safegcd libsecp256k1 je funkčně správná.

Omezení ověřování

Existují určitá omezení důkazu o funkční správnosti. Separační logika používaná v Ověřitelném C implementuje to, co je známo jako částečná správnost. To znamená, že pouze dokazuje, že kód C se vrací se správným výsledkem, pokud se vrací, ale nedokazuje samotnou terminaci. Toto omezení zmírňujeme použitím našeho předchozího důkazu Coq o hranicích na algoritmu safegcd k prokázání, že hodnota počítadla smyčky v hlavní smyčce ve skutečnosti nikdy nepřekročí 11 iterací.

Další problém je, že jazyk C sám o sobě nemá formální specifikaci. Místo toho projekt Verifiable C používá projekt kompilátoru CompCert k poskytnutí formální specifikace jazyka C. To zaručuje, že když je ověřený C program zkompilován kompilátorem CompCert, výsledný strojový kód bude splňovat jeho specifikaci (s ohledem na výše uvedené omezení). Nicméně to nezaručuje, že kód generovaný GCC, clangem nebo jiným kompilátorem bude nutně fungovat. Například kompilátory C mohou mít různé pořadí hodnocení argumentů v rámci volání funkce. A i kdyby měl jazyk C formální specifikaci, jakýkoli kompilátor, který není sám formálně ověřen, by stále mohl programy špatně zkompilovat. K tomu dochází v praxi.

Nakonec, Verifiable C nepodporuje předávání struktur, vracení struktur nebo přiřazování struktur. Zatímco v libsecp256k1 jsou struktury vždy předávány pomocí ukazatele (což je v Verifiable C povoleno), existuje několik příležitostí, kdy se používá přiřazení struktur. Pro důkaz správnosti modulárního inverzního algoritmu bylo třeba nahradit 3 přiřazení specializovaným voláním funkce, která provádí přiřazení struktury pole po poli.

Shrnutí

Blockstream Research formálně ověřil správnost funkce modulární inverze libsecp256k1. Tato práce poskytuje další důkaz, že ověřování kódu C je v praxi možné. Použití asistenta pro důkaz obecného určení nám umožňuje ověřit software postavený na složitých matematických argumentech.

Nic nebrání tomu, aby zbytek funkcí implementovaných v libsecp256k1 byl také ověřen. Je tedy možné, aby libsecp256k1 získal nejvyšší možné záruky správnosti softwaru.

Toto je příspěvek hosta od Russella O'Connora a Andrewa Poelstry. Vyjádřené názory jsou zcela jejich vlastní a nemusí nezbytně odrážet názory BTC Inc nebo Bitcoin Magazine.

Zdroj: Bitcoin Magazine

Příspěvek Ověřená implementace Safegcd se poprvé objevil na Crypto Breaking News.