邁向密碼管理器密碼生成演算法的形式化驗證

1. 簡介

密碼管理器是提升安全性的重要工具，它讓使用者能夠使用強度足夠且唯一的密碼，而無需承擔記憶的認知負擔。儘管有其優點，使用者的信任度仍是其普及的一大障礙。本文探討一個影響信任的關鍵功能：隨機密碼生成演算法。我們提出一個使用 EasyCrypt 框架進行形式化驗證的參考實作，旨在證明其功能正確性與安全性質，目標是為密碼管理器中的密碼生成建立一個可信賴的標準。

2. 現行密碼生成演算法

本研究調查了 15 款密碼管理器，並針對三個廣泛使用的開源範例進行詳細分析：Google Chrome 密碼管理器、Bitwarden 和 KeePass。目標是了解常見的演算法並找出適合進行形式化驗證的領域。

3. 形式化驗證方法

本文採用 EasyCrypt 證明輔助工具來形式化並驗證密碼生成演算法。驗證著重於兩個關鍵性質：

• 功能正確性： 演算法總是產生一個滿足使用者定義組成原則的密碼。
• 安全性（隨機性）： 假設使用密碼學安全的亂數產生器，輸出密碼在計算上與從原則定義的字母表中抽取的、相同長度的真正隨機字串無法區分。這是使用基於遊戲的密碼學證明方法來建模的。

這種形式化方法超越了傳統測試，提供了關於演算法行為的數學保證。

4. 技術細節與數學公式化

安全性質被形式化為一個密碼學遊戲。令 $\mathcal{A}$ 為一個機率多項式時間對手。令 $\text{Gen}(policy)$ 為密碼生成演算法，$\text{Random}(policy)$ 為一個理想的產生器，它從所有滿足 $policy$ 的字串中均勻隨機地輸出一個字串。$\mathcal{A}$ 區分兩者的優勢定義為：

$\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) = |\Pr[\mathcal{A}(\text{Gen}(policy)) = 1] - \Pr[\mathcal{A}(\text{Random}(policy)) = 1]|$

如果對於所有 PPT 對手 $\mathcal{A}$，此優勢皆可忽略不計，則該演算法被視為是安全的，意即 $\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) \leq \epsilon(\lambda)$，其中 $\epsilon$ 是安全參數 $\lambda$ 中的可忽略函數。EasyCrypt 中的證明建構了一系列遊戲（Game$_0$, Game$_1$, ...）來界定此優勢，通常依賴於底層 PRG 是安全的假設。

5. 實驗結果與圖表說明

雖然 PDF 主要著重於形式化規格與證明策略，但實際成果是一個經過驗證的參考實作。這裡的「實驗」是指在 EasyCrypt 環境中成功完成形式化證明。這可作為正確性的藍圖。

概念性圖表說明： 流程圖能有效視覺化經過驗證的演算法：

1. 開始： 使用者輸入原則（長度 L，字元集 S1...Sn 及其最小/最大計數）。
2. 步驟 1 - 滿足最小值： 對於每個 min_i > 0 的字元集 Si，從 Si 生成 min_i 個隨機字元。計數器：已生成 $\sum min_i$ 個字元。
3. 步驟 2 - 填滿至長度 L： 令 $\text{Remaining} = L - \sum min_i$。當 Remaining > 0 時：從所有 current_count(Si) < max_i 的字元集 Si 建立一個池。從此池中選擇一個隨機字元。Remaining 減 1。
4. 步驟 3 - 隨機排列： 對 L 個字元的列表應用密碼學安全的隨機排列（Fisher-Yates 洗牌演算法）。
5. 步驟 4 - 輸出： 輸出最終隨機排列後的字串。此步驟的綠色勾選標記標示為「形式化驗證 (EasyCrypt)：正確性與隨機性」。

6. 分析框架：範例案例

情境： 驗證當啟用「排除相似字元」選項（例如，排除 'l', 'I', 'O', '0'）時，演算法能避免細微的偏差。

潛在缺陷（未經驗證）： 一個簡單的實作可能會先從完整字元集生成密碼，然後移除被排除的字元，這可能導致密碼長度變短，或改變剩餘字元集的分佈，從而違反原則或引入偏差。

形式化驗證方法： 在 EasyCrypt 中，我們會將字元集指定為 $\text{Alphabet}_{\text{final}} = \text{Alphabet}_{\text{full}} \setminus \text{ExcludedSet}$。接著，證明將展示生成過程（上述步驟 1 和 2）會從相關字元集的 $\text{Alphabet}_{\text{final}}$ 中均勻取樣，並且最小/最大限制會針對這個縮減後的集合正確評估。這從建構上消除了該缺陷。

非程式碼產物： EasyCrypt 中用於字元選擇步驟的形式化規格，將在邏輯上定義取樣池，確保被排除的字元永遠不會成為來源的一部分。

7. 核心洞見與分析師觀點

核心洞見： 本文的根本貢獻在於，將密碼管理器的信任模型從「希望透過程式碼審查和測試來確保安全」轉變為「透過形式化驗證獲得數學證明上的安全」。它正確地將密碼產生器視為信任的關鍵樞紐——一個單點故障，若有缺陷，將破壞管理器整個安全前提。這項工作是應用密碼學中一個關鍵但未被充分重視的趨勢的一部分，類似於 TLS 協定（Project Everest）或密碼學函式庫（HACL*）的形式化驗證工作。

邏輯流程： 論點是合理的：1) 由於安全性的不透明，使用者信任度低。2) 密碼生成是一個關鍵且複雜的元件，容易出現細微的錯誤（例如偏差、違反原則）。3) 形式化方法提供了最高程度的保證。4) EasyCrypt 為此驗證提供了一個實用的框架。5) 經過驗證的參考實作可以作為業界的黃金標準。

優點與缺陷： 優點： 專注於一個具體且影響重大的問題非常出色。使用 EasyCrypt 這個成熟的基於遊戲證明的工具是務實的。對現實世界密碼管理器演算法的分析使研究立足於實踐。缺陷： 本文是一篇「邁向」性質的論文——它奠定了基礎，但並未為主要密碼管理器的所有原則提供一個完整、經過實戰考驗的驗證實作。真正的挑戰在於商業密碼原則的複雜性（如 KeePass 廣泛的選項），這可能會使驗證狀態空間爆炸性增長。它也迴避了房間裡的大象：密碼管理器周圍系統（使用者介面、記憶體、儲存、自動填入）的安全性同樣關鍵，正如 NCC Group 等組織的研究所指出的。

可執行的見解： 1) 對密碼管理器供應商： 採用此驗證過的參考實作或與之交叉比對。即使完整的 UI 原則引擎仍未驗證，也應從驗證核心生成邏輯開始。2) 對安全稽核人員： 要求對核心密碼學模組進行形式化驗證，將其視為一種新的最佳實踐，類似於使用經過審查的密碼學原語。3) 對研究人員： 擴展此工作以驗證產生器與 CSPRNG 及系統熵源的整合——一條鏈的強度取決於其最弱的一環。該領域應以驗證端到端元件為目標，類似於 seL4 等經過驗證的作業系統背後的願景。

8. 應用前景與未來方向

最直接的應用是建立一個可直接替換、經過驗證的密碼生成函式庫，可以整合到如 Bitwarden 和 KeePass 等開源密碼管理器中，顯著提升其可信度。展望未來：

• 標準化： 這項工作可以為制定密碼學安全密碼生成的形式化標準（例如 IETF RFC）提供參考，類似於 NIST SP 800-63B，但具有可驗證的實作。
• 瀏覽器與作業系統整合： 主要平台如 Chrome、Firefox 和 iOS/macOS 鑰匙圈可以採用經過驗證的產生器，為數十億使用者提高安全基線。
• 擴展至其他領域： 此方法論可直接應用於其他隨機字串生成需求，例如生成 API 金鑰、權杖或復原代碼。
• 自動化原則合規性： 未來的工具可以為使用者自訂的原則自動生成形式化證明，讓具有獨特原則需求的企業密碼管理器也能使用高保證度的生成功能。
• 混合方法： 將形式化驗證與模糊測試（例如使用 AFL++ 等工具）結合，用於密碼管理器堆疊中未經驗證的部分，可以提供穩健的多層防禦。

最終方向是逐步對整個關鍵安全子系統進行形式化驗證，推動產業從被動修補轉向主動證明安全。

9. 參考文獻

1. Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv preprint arXiv:2106.03626.
2. Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., & Strub, P. Y. (2014). EasyCrypt: A framework for formal cryptographic proofs. Journal of Cryptology.
3. Shoup, V. (2004). Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive.
4. NCC Group. (2023). Password Manager Security Review. Retrieved from https://www.nccgroup.com
5. Klein, G., et al. (2009). seL4: Formal verification of an OS kernel. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles.
6. National Institute of Standards and Technology (NIST). (2017). Digital Identity Guidelines: Authentication and Lifecycle Management (SP 800-63B).