比特幣和其他區塊鏈（如 Liquid）的安全性依賴於數位簽名算法，如 ECDSA 和 Schnorr 簽名。一個名為 libsecp256k1 的 C 庫提供這些算法，並被比特幣核心和 Liquid 共同使用。這些算法使用一種稱為模數反的計算，這是過程中的一個昂貴部分。
在《快速常數時間 gcd 計算和模數反轉》中，Daniel J. Bernstein 和 Bo-Yin Yang 創建了一種新的模數反轉算法，稱為“safegcd”。這個算法在 2021 年由 Peter Dettman 實現到 libsecp256k1 中。Blockstream Research 使用 Coq 證明助手正式驗證了該算法的設計，顯示它正確計算了 256 位輸入的模數反。
然而，實現 safegcd 算法需要調整數學描述以適應 C 程序語言，該語言僅原生支持高達 64 位的整數。添加了幾個優化使實現更快，導致 libsecp256k1 中有四個不同的 safegcd 算法實現。
為了確保 C 代碼正確實現 safegcd 算法，使用了 Verifiable C，這是經過驗證的軟件工具鏈的一部分，與 Coq 定理證明器一起使用。這涉及為每個正在進行驗證的函數指定前置條件和後置條件，使用分離邏輯。然後，驗證過程從函數的前置條件開始，在函數主體中的每個語句後建立一個新的不變性，直到在函數主體結尾或返回語句達到後置條件。
大多數的形式化工作花費在將每個 C 表達式的原始操作轉換為有關所操作數據結構在數學上代表什麼的高級語句上。驗證結果是一個正式的證明，經過 Coq 證明助手的驗證，證明了 libsecp256k1 的 64 位變量時間實現的 safegcd 模數反算法是功能上正確的。
然而，功能正確性證明有一些限制。Verifiable C 中使用的分離邏輯僅證明部分正確性，這意味著它僅顯示 C 代碼在返回時返回正確的結果，但並不證明終止本身。為了解決這個問題，之前對 safegcd 算法邊界的 Coq 證明被用來證明主循環的循環計數器值從未超過 11 次迭代。
另一個限制是 C 語言本身沒有正式規範。相反，Verifiable C 項目使用 CompCert 編譯器項目來提供 C 語言的正式規範。這保證了當一個經過驗證的 C 程序用 CompCert 編譯器編譯時，生成的匯編代碼將符合其規範，但不保證其他編譯器生成的代碼必然可用。
此外，Verifiable C 不支持傳遞、返回或賦值結構。在 libsecp256k1 中，結構總是通過指針傳遞，這在 Verifiable C 中是被允許的，但有幾個場合使用了結構賦值。總之，Blockstream Research 正式驗證了 libsecp256k1 的模數反函數的正確性，提供了進一步的證據，表明 C 代碼的驗證在實踐中是可能的。
這項工作還突顯出 libsecp256k1 中實現的其他函數也可以進行驗證，從而使庫能夠實現最高可能的軟件正確性保證。
來源
<p>該文章《數位簽名如何使比特幣安全！》首次出現在 CoinBuzzFeed.</p>
