Python 已內建 15,000 行形式化驗證密碼學程式碼！

2022 年 11 月，我在 Python 的 GitHub 倉庫提出了 issue 99108，指出 Python 的 SHA3 實作曾爆出 CVE 漏洞，因而主張 Python 應全面採用經過形式化驗證的程式碼來支持所有雜湊相關基礎建設。

https://github.com/python/cpython/issues/99108
上週，該issue正式關閉：Python 默認提供的所有雜湊與 HMAC 演算法，如今皆由經過形式化驗證的密碼學程式庫 HACL* 負責實作。功能毫無刪減，對使用者而言轉換過程完全無感。Python 目前直接內含來自 HACL* 的 15,000 行形式化驗證過的 C 程式碼；未來欲同步上游版本，只需執行腳本即可自動完成。HACL* 亦成功實作多項新功能，以滿足 Python 的所有需求，包括：為 Blake2 演算法家族新增更多模式、提供涵蓋所有 Keccak 變體的全新 SHA3 API、導入嚴謹的抽象層次以解決建置系統難題、完善的錯誤管理（尤其是記憶體配置失敗），以及在 HMAC 演算法中實例化 HACL* 通用「串流」機制，並加入需同時保留兩個雜湊狀態的最佳化。
https://github.com/project-everest/hacl-star/
此專案歷時兩年半，若無 Aymeric Fromherz 承擔大部分實作工作，將無法完成；Son Ho 在早期亦關鍵地將 HACL* 的「串流」機制泛化，以支援需「前置輸入」的區塊演算法——該改動對在底層同時保留兩個雜湊狀態、打造高效 HMAC 不可或缺。Python 方面的 Gregory P. Smith、Bénédikt Tran 與後來的 Chris Eibl 皆是推手。HACS 工作坊則串起社群（向 Paul Kehrer 致意！）並提供推進動能。感謝所有密碼學與形式化驗證社群伙伴！
以下揭開幕後技術細節，評論一些在學術論文中通常看不見的底層有趣技術。
流式 API 入門
許多密碼學演算法都是區塊演算法，意味著它們假設輸入以區塊為單位提供，並對第一區塊和最後區塊進行特殊處理。眾所周知的區塊演算法包括雜湊（hash）演算法、訊息認證碼（MAC）演算法（如 Poly1305、HMAC）等。在實際應用中，區塊 API 並不友好：極少有情況下使用者一開始就已將數據分割成區塊；而且，每次計算結果（例如雜湊值）都會讓區塊演算法的內部狀態失效，這使得例如計算 TLS 會話中間雜湊變得困難。
基於這些原因，密碼學函式庫通常會提供流式（streaming）API，允許客戶端提供任意長度的輸入；函式庫會自動在內部做緩衝，並在積累到一整個區塊時立即處理並清空緩衝區。流式 API 通常也支援在不破壞當前狀態的前提下，提取中間雜湊值。
實作流式 API 相當棘手，因為它們必須操作具備複雜不變式的長期存在狀態：未經驗證的 SHA3 參考實現於 2022 年爆出重大 CVE，而 Python 因為沿用了該實現，也「繼承」了這項漏洞。
https://nvd.nist.gov/vuln/detail/cve-2022-37454
流式 API 的困難還在於底層區塊演算法在諸多細節上各不相同：除了 Blake2 之外，所有雜湊演算法都允許最後一個區塊為空；有些演算法需要在執行階段保留密鑰（如 Poly1305），有些則可在初始化後丟棄密鑰（如 HMAC，或其最佳化版本）；有些需要先輸入少量數據才能處理密鑰（如 Blake2），有些則不需要……等等。
鑑於這些內在複雜性，流式演算法非常適合作為形式化驗證對象：我們在 2021 年曾針對這一問題撰寫過一篇研究論文。
https://arxiv.org/abs/2102.01644
全泛型驗證
論文中的主要想法是：可以使用依賴類型（dependent types）來刻畫何謂「區塊演算法」。一旦完成這項刻畫，就只需基於這個抽象的區塊演算法定義，一勞永逸地撰寫並驗證一次泛型流式構造。接著，就像在 C++ 中實例化模板那樣，只要將這個泛型流式構造套用到具體的區塊 API 上，即可「免費」獲得該區塊演算法的流式 API。
第一個障礙在於：論文中所呈現的範例（見 Listing 12）與程式庫中的實際實作之間，存在相當大的差異。具體來說，要涵蓋任意的區塊演算法，需要極高的泛化能力：
https://github.com/hacl-star/hacl-star/blob/897e23d315c08f7a375408d60d1a4918477fcaa0/code/streaming/Hacl.Streaming.Interface.fsti#L254
最終摘要長度可選

使用者可以選擇是否指定最終輸出摘要（digest）的長度。例如，SHA3 各變體的輸出長度固定，但 Shake 系列則允許使用者自訂輸出長度。

前置輸入（pre-input）
某些演算法在處理資料區塊前，必須先接收一段預先輸入的數據。以 SHA2 為例，前置輸入為空；而在 Blake2 的有鍵雜湊模式下，前置輸入即為密鑰區塊。
緩衝管理的複雜性
並非所有演算法都允許最後一個區塊為空（例如 Blake2 就不允許），這大幅增加了緩衝區管理的難度，且需與前置輸入協同運作。
長期狀態中的額外資訊
某些演算法需在整個流式運行過程中保留額外狀態。例如，Blake2 的密鑰長度可在初始化時調整，卻必須持續保留於長期狀態中。
不中斷原狀態的中間摘要提取
為了在提取中間摘要（intermediary digest）時不破壞原本的區塊狀態，流式 API 會在內部複製該狀態。有時在棧上分配副本較為方便，有時則更適合使用堆分配。
API 粒度的抉擇
單一演算法對應一套 API：如 SHA2-{224,256,384,512} 各自擁有獨立的 API。
演算法家族共用一套 API：如 Keccak 家族中的 4 種 SHA3 變體與 2 種 Shake 變體，共用同一套 API。
為了達成如此高度的泛化，專案經歷了多輪迭代，每一輪皆由 Python 生態系統的需求所驅動。最終在將 HMAC 作為 Python 中最後落地的演算法時，我們發現事先撰寫的證明和定義已足夠通用，無須任何額外調整，即可直接將通用流式 API 應用於 HMAC，順利完成驗證與實作。
堅實的建置流程
向 Python 投遞 PR 意謂著：其 CI 涵蓋逾 50 款工具鏈與架構，遠超平日測試範圍。好處是漏洞無所遁形；壞處則是古老角落全被踩到。
在處理 HMAC 時，出現了一個特別棘手的構建問題。提醒一下，HMAC 是一種通用構造，它以雜湊演算法為基礎，提供帶密鑰的訊息認證碼──簡而言之，有一段高階的 HMAC 程式碼，會將大部分工作委派給各個雜湊演算法。每種雜湊演算法本身也可能有多種實現：例如，HMAC‑Blake2b 同時有 HMAC‑Blake2b‑32（常規實現）和 HMAC‑Blake2b‑256（AVX2 寬向量實現）。
https://en.wikipedia.org/wiki/HMAC
這已經引發了問題：如果 Python 在具備 AVX2 支援的機器上運行，HMAC.c 可能會調用 Blake2b_256.c 中的函數。然而，唯有 Blake2b_256.c 可以使用 -mavx2 來編譯；而 HMAC.c 的程式碼必須在所有機器（包括不支援 AVX2 的機器）上都能執行，因此它絕不能以 -mavx2 來編譯。到此為止，一切似乎都在預期範圍內，而這也是我們之前曾經做過的處理方式。
問題出在 HMAC.c 需要為 Blake2b_256.c 建立初始狀態時，程式碼如下：

對大多數工具鏈而言，這段程式碼並無問題──immintrin.h 定義了 __m256i 型別，即便 HMAC.c 無法假設 AVX2 指令一定可用，編譯器也能在不使用 AVX2 指令的情況下，將 blake2b_256_state 進行零初始化……但有些舊版編譯器若未加上 -mavx2，就會拒絕處理 immintrin.h，這便完全破壞了原本的設計初衷。
為了解決這個問題，我們不得不大幅重構程式碼，採用眾所周知的「C 抽象結構（abstract struct）」模式，基本上是在 C 中定義一個抽象型別：
額外的困難在於，這些 C 程式碼是從 F* 自動產生的，而 F* 對抽象性的定義與 C 大相逕庭。負責將 F* 轉譯為 C 的編譯器 krml，必須全面改造以執行更細緻的可見性分析（涵蓋公用函數、函式庫內部函數、翻譯單元內部函數等），才能正確處理這類「抽象結構」。
https://github.com/FStarLang/karamel/
處理記憶體分配失敗
雖然我們最初在 F* 中對 C 的建模就允許對記憶體分配失敗進行推理，但實際上從未有人在生成的程式碼中落實這部分功能。對於 Python 而言，我們希望能夠將記憶體分配失敗的資訊向上層傳播。這意味著必須細化我們對可變狀態（如區塊狀態）、對區塊演算法（如 SHA2‑256）及對通用流式構造的定義，讓它們都能將記憶體分配失敗的狀態一路傳遞到呼叫端。幸好，這並不算太複雜：我們沿路插入了 option 型別，且因為只有一套通用流式構造，對 15 多個具體流式 API 實例的實作和證明，只需更新一次即可。
在產生的 C 程式碼中，這些 option 型別被轉譯為標籤聯合（tagged unions），雖然寫起來比較冗長，但我們也可能調整對狀態的定義，改用一個在執行時就可檢測記憶體分配是否失敗的 has_failed 函數，這樣雖然會增加一些複雜度和驗證工作，但可能更為簡潔。
從上游 HACL* 向 Python 推送變更
最初的 Python 拉取請求（PR）中，我加入了一個 shell 腳本，能自動從上游 HACL* 倉庫抓取所需檔案；透過精心撰寫的 sed 指令移除標頭檔中多餘的定義；並在原地微調幾條 include 路徑，同樣使用我最喜愛的重構工具 sed。這樣做的好處是，最初的 PR 保持了精簡與乾淨。
後來，當確認上游程式碼相對穩定且易於維護後，我們移除了那一大堆 sed，因為即使標頭檔多了幾個冗餘定義，也不至於影響全局，反而讓維護更簡單。
現在，任何想要更新 HACL* 的人，只要在自己的 Python 倉庫中執行該 shell 腳本，並在 Python 的 SBOM（software bill of materials）中更新預期的雜湊值，就能輕鬆整合最新的改進。