ビットコインや Liquid などの他のブロックチェーンのセキュリティは、ECDSA やシュノール署名のようなデジタル署名アルゴリズムに依存しています。libsecp256k1 と呼ばれる C ライブラリがこれらのアルゴリズムを提供し、ビットコインコアと Liquid の両方で使用されています。これらのアルゴリズムは、プロセスの高コスト部分であるモジュラー逆数と呼ばれる計算を使用します。
「高速定数時間 gcd 計算とモジュラー逆数」では、ダニエル・J・バーンスタインとボー・イン・ヤンが「safegcd」と呼ばれる新しいモジュラー逆数アルゴリズムを作成しました。このアルゴリズムは、2021 年にピーター・デットマンによって libsecp256k1 に実装されました。Blockstream Research は、Coq 証明助手を使用してアルゴリズムの設計を正式に検証し、256 ビットの入力に対してモジュラー逆数を正しく計算することを示しました。
ただし、safegcd アルゴリズムを実装するには、数学的な説明を C プログラミング言語に適合させる必要があり、これは 64 ビットまでの整数しかネイティブにサポートしていません。実装を迅速にするためにいくつかの最適化が追加され、libsecp256k1 には safegcd アルゴリズムの 4 つの別々の実装が存在します。
C コードが safegcd アルゴリズムを正しく実装していることを確認するために、Verified Software Toolchain の一部である Verifiable C が Coq 定理証明器と共に使用されました。これには、分離論理を使用して検証を受けるすべての関数に対して前提条件と後続条件を指定することが含まれました。検証プロセスは、その後、関数の前提条件から始まり、関数本体の各文の後に新しい不変条件を確立し、関数本体の最後または返り値の文で後続条件に達するまで続きました。
形式化の大部分の努力は、各 C 式の生の操作を、操作されるデータ構造が数学的に何を表すかについての高レベルのステートメントに翻訳することに費やされました。この検証は、libsecp256k1 の 64 ビット変数時間実装の safegcd モジュラー逆数アルゴリズムが機能的に正しいことを確認するために Coq 証明助手によって検証された形式的証明をもたらしました。
ただし、機能的正確性の証明にはいくつかの制限があります。Verifiable C で使用される分離論理は部分的な正確性しか証明せず、C コードが結果を返す場合に正しい結果を返すことを示すだけで、終了そのものを証明するものではありません。これに対処するために、safegcd アルゴリズムの境界に関する以前の Coq 証明を使用して、メインループのループカウンタ値が 11 回の反復を超えないことを証明しました。
もう一つの制限は、C 言語自体に正式な仕様がないことです。代わりに、Verifiable C プロジェクトは、C 言語の正式な仕様を提供するために CompCert コンパイラプロジェクトを使用しています。これにより、検証された C プログラムが CompCert コンパイラでコンパイルされると、結果として得られるアセンブリコードがその仕様を満たすことが保証されますが、他のコンパイラによって生成されたコードが必ずしも機能することが保証されるわけではありません。
さらに、Verifiable C は構造体の受け渡し、返却、または代入をサポートしていません。libsecp256k1 では、構造体は常にポインタによって渡されますが、これは Verifiable C で許可されています。しかし、構造体の代入が使用される場合がいくつかあります。要約すると、Blockstream Research は libsecp256k1 のモジュラー逆数関数の正確性を正式に検証し、C コードの検証が実際に可能であることを示すさらなる証拠を提供しました。
この作業は、libsecp256k1 に実装された他の関数も検証できることを強調しており、ライブラリが可能な限り最高のソフトウェアの正確性の保証を達成できるようにしています。
ソース
<p>ビットコインを安全にするデジタル署名の方法に関する投稿は、最初に CoinBuzzFeed に掲載されました。 </p>
