Introducere

Securitatea Bitcoin și a altor blockchains, cum ar fi Liquid, depinde de utilizarea algoritmilor de semnătură digitală, cum ar fi ECDSA și semnăturile Schnorr. O bibliotecă C numită libsecp256k1, numită după curba eliptică pe care biblioteca operează, este utilizată atât de Bitcoin Core, cât și de Liquid, pentru a oferi aceste algoritmi de semnătură digitală. Acești algoritmi utilizează o calculare matematică numită invers modular, care este un component relativ costisitor al calculului.

În „Calculul rapid al gcd-ului în timp constant și inversarea modulară”, Daniel J. Bernstein și Bo-Yin Yang dezvoltă un nou algoritm de inversare modulară. În 2021, acest algoritm, denumit „safegcd”, a fost implementat pentru libsecp256k1 de Peter Dettman. Ca parte a procesului de examinare pentru acest nou algoritm, Blockstream Research a fost prima care a finalizat o verificare formală a designului algoritmului folosind asistentul de dovadă Coq pentru a verifica formal că algoritmul se termină cu adevărat cu rezultatul corect al inversului modular pe intrări de 256 de biți.

Lipsa dintre algoritm și implementare

Efortul de formalizare din 2021 a arătat doar că algoritmul conceput de Bernstein și Yang funcționează corect. Cu toate acestea, utilizarea acelui algoritm în libsecp256k1 necesită implementarea descrierii matematice a algoritmului safegcd în cadrul limbajului de programare C. De exemplu, descrierea matematică a algoritmului efectuează înmulțirea matricelor de vectori care pot fi la fel de largi ca întregi semnați de 256 de biți, cu toate acestea, limbajul de programare C va oferi nativ doar întregi de până la 64 de biți (sau 128 de biți cu unele extensii de limbaj).

Implementarea algoritmului safegcd necesită programarea înmulțirii matricelor și a altor calcule folosind întregi de 64 de biți din C. În plus, au fost adăugate multe alte optimizări pentru a face implementarea rapidă. La final, există patru implementări separate ale algoritmului safegcd în libsecp256k1: două algoritmi de timp constant pentru generarea semnăturilor, unul optimizat pentru sisteme de 32 de biți și unul optimizat pentru sisteme de 64 de biți, și doi algoritmi de timp variabil pentru verificarea semnăturilor, din nou unul pentru sisteme de 32 de biți și unul pentru sisteme de 64 de biți.

Verifiable C

Pentru a verifica că codul C implementează corect algoritmul safegcd, toate detaliile implementării trebuie verificate. Folosim Verifiable C, parte a Verificatului Software Toolchain pentru raționarea despre codul C folosind teorema proverului Coq.

Verificarea progresează prin specificarea precondițiilor și postcondițiilor folosind logica separării pentru fiecare funcție supusă verificării. Logica separării este o logică specializată pentru raționarea despre subroutines, alocările de memorie, concurență și altele.

Odată ce fiecare funcție are o specificație, verificarea progresează începând de la precondiția unei funcții și stabilind o nouă invariantă după fiecare instrucțiune din corpul funcției, până la stabilirea condiției post la sfârșitul corpului funcției sau la sfârșitul fiecărei instrucțiuni de returnare. Cele mai multe eforturi de formalizare sunt cheltuite „între” liniile de cod, folosind invarianta pentru a traduce operațiile brute ale fiecărei expresii C în declarații de nivel superior despre ce reprezintă structurile de date manipulate din punct de vedere matematic. De exemplu, ceea ce limbajul C consideră a fi un tablou de întregi de 64 de biți poate fi de fapt o reprezentare a unui întreg de 256 de biți.

Rezultatul final este o dovadă formală, verificată de asistentul de dovadă Coq, că implementarea de timp variabil de 64 de biți a algoritmului inversului modular safegcd din libsecp256k1 este funcțional corectă.

Limitările Verificării

Există unele limitări în dovada corectitudinii funcționale. Logica separării utilizată în Verifiable C implementează ceea ce se cunoaște sub numele de corectitudine parțială. Aceasta înseamnă că dovedește doar că codul C returnează cu rezultatul corect dacă returnează, dar nu dovedește terminarea în sine. Mitigăm această limitare folosind dovada noastră anterioară Coq a limitelor algoritmului safegcd pentru a dovedi că valoarea contorului buclei din bucla principală de fapt nu depășește niciodată 11 iterații.

O altă problemă este că limbajul C nu are o specificație formală. În schimb, proiectul Verifiable C folosește proiectul CompCert pentru a oferi o specificație formală a limbajului C. Acest lucru garantează că, atunci când un program C verificat este compilat cu compilatorul CompCert, codul de asamblare rezultat va respecta specificația sa (sub rezerva limitării de mai sus). Cu toate acestea, acest lucru nu garantează că codul generat de GCC, clang sau orice alt compilator va funcționa neapărat. De exemplu, compilatoarele C pot avea ordine de evaluare diferite pentru argumente în cadrul unei apeluri de funcție. Și chiar dacă limbajul C ar avea o specificație formală, orice compilator care nu este el însuși verificat formal ar putea în continuare să compileze greșit programele. Acest lucru se întâmplă în practică.

În cele din urmă, Verifiable C nu suportă transmiterea structurilor, returnarea structurilor sau atribuirea structurilor. Deși în libsecp256k1 structurile sunt întotdeauna transmise prin pointer (ceea ce este permis în Verifiable C), există câteva ocazii în care se folosește atribuirea structurilor. Pentru dovada corectitudinii inversei modulare, au fost 3 atribuiri care au trebuit înlocuite cu un apel de funcție specializat care efectuează atribuirea structurilor câmp cu câmp.

Rezumat

Blockstream Research a verificat formal corectitudinea funcției de inversare modulară a libsecp256k1. Această lucrare oferă dovezi suplimentare că verificarea codului C este posibilă în practică. Utilizarea unui asistent de dovadă de uz general ne permite să verificăm software-ul construit pe argumente matematice complexe.

Nimic nu împiedică restul funcțiilor implementate în libsecp256k1 să fie verificate de asemenea. Astfel, este posibil ca libsecp256k1 să obțină cele mai înalte garanții posibile de corectitudine a software-ului.

Aceasta este o postare de invitat de Russell O’Connor și Andrew Poelstra. Părerele exprimate sunt în întregime ale lor și nu reflectă neapărat cele ale BTC Inc sau Bitcoin Magazine.

Sursa: Bitcoin Magazine

Postarea Safegcd’s Implementation Formally Verified a apărut prima dată pe Crypto Breaking News.