Die Implementierung des effizienten modularen Inversionsalgorithmus "safegcd" in der Krypto-Bibliothek libsecp256k1, die von Bitcoin und Liquid verwendet wird, wurde formal verifiziert. Mittels des Coq-Theorembeweisers und Verifiable C wurde die funktionale Korrektheit der 64-Bit-Variante mit variabler Zeit bewiesen, wobei die Terminierung des Algorithmus jedoch noch aussteht. Diese Verifikation erhöht die Sicherheit und das Vertrauen in die zugrundeliegenden kryptographischen Operationen der Blockchains.
Die Sicherheit von Bitcoin und anderen Blockchains wie Liquid hängt von der Verwendung digitaler Signaturalgorithmen wie ECDSA und Schnorr-Signaturen ab. Eine C-Bibliothek namens libsecp256k1, benannt nach der elliptischen Kurve, auf der die Bibliothek operiert, wird sowohl von Bitcoin Core als auch von Liquid verwendet, um diese digitalen Signaturalgorithmen bereitzustellen. Diese Algorithmen verwenden eine mathematische Berechnung namens modularer Inverser, die eine relativ teure Komponente der Berechnung ist. Wie bitcoinmagazine.com berichtet, wurde im Jahr 2021 ein neuer modularer Inversionsalgorithmus namens "safegcd" für libsecp256k1 implementiert. Blockstream Research führte die erste formale Verifikation des Algorithmusdesigns durch und verwendete den Coq-Proof-Assistant, um formal zu verifizieren, dass der Algorithmus tatsächlich mit dem korrekten modularen inversen Ergebnis für 256-Bit-Eingaben terminiert.
Die Formalisierung im Jahr 2021 zeigte nur, dass der von Bernstein und Yang entworfene Algorithmus korrekt funktioniert. Die Verwendung dieses Algorithmus in libsecp256k1 erfordert jedoch die Implementierung der mathematischen Beschreibung des safegcd-Algorithmus in der Programmiersprache C. Die mathematische Beschreibung des Algorithmus führt beispielsweise eine Matrixmultiplikation von Vektoren durch, die so breit wie 256-Bit-Integer mit Vorzeichen sein können, die C-Programmiersprache bietet jedoch nur Integer bis zu 64 Bit (oder 128 Bit mit einigen Spracherweiterungen) nativ an.
Die Implementierung des safegcd-Algorithmus erfordert die Programmierung der Matrixmultiplikation und anderer Berechnungen mithilfe von 64-Bit-Integern von C. Darüber hinaus wurden viele weitere Optimierungen hinzugefügt, um die Implementierung zu beschleunigen. Letztendlich gibt es vier separate Implementierungen des safegcd-Algorithmus in libsecp256k1: zwei Algorithmen mit konstanter Zeit für die Signaturerstellung, eine für 32-Bit-Systeme und eine für 64-Bit-Systeme optimiert, und zwei Algorithmen mit variabler Zeit für die Signaturprüfung, wiederum eine für 32-Bit-Systeme und eine für 64-Bit-Systeme.
Um zu überprüfen, ob der C-Code den safegcd-Algorithmus korrekt implementiert, müssen alle Implementierungsdetails überprüft werden. Dafür wird Verifiable C verwendet, ein Teil der Verified Software Toolchain, um mit dem Coq-Theorembeweiser über C-Code nachzudenken. Die Verifizierung erfolgt durch Angabe von Vorbedingungen und Nachbedingungen mithilfe der Separationslogik für jede zu verifizierende Funktion. Die Separationslogik ist eine Logik, die auf die Argumentation über Unterprogramme, Speicherzuweisungen, Parallelität und mehr spezialisiert ist.
Sobald jede Funktion eine Spezifikation erhalten hat, beginnt die Verifizierung mit der Vorbedingung einer Funktion und legt nach jeder Anweisung im Hauptteil der Funktion eine neue Invariante fest, bis schließlich die Nachbedingung am Ende des Funktionshauptteils oder am Ende jeder return-Anweisung festgelegt ist. Der größte Teil des Formalisierungsaufwands wird „zwischen“ den Codezeilen aufgewendet, wobei die Invarianten verwendet werden, um die Rohvorgänge jedes C-Ausdrucks in übergeordnete Anweisungen darüber zu übersetzen, was die manipulierten Datenstrukturen mathematisch darstellen. Was die C-Sprache beispielsweise als ein Array von 64-Bit-Integern betrachtet, kann tatsächlich eine Darstellung eines 256-Bit-Integers sein.
Das Endergebnis ist ein formaler Beweis, der vom Coq-Proof-Assistant verifiziert wurde, dass die 64-Bit-Implementierung des safegcd-Algorithmus mit variabler Zeit von libsecp256k1 funktional korrekt ist. Es gibt jedoch einige Einschränkungen des funktionalen Korrektheitsbeweises. Die in Verifiable C verwendete Separationslogik implementiert die sogenannte partielle Korrektheit. Das bedeutet, dass nur bewiesen wird, dass der C-Code mit dem korrekten Ergebnis zurückkehrt, wenn er terminiert. Es wird nicht bewiesen, dass der Code tatsächlich terminiert.
