研究人員來自 國立信息學與自動化研究所（INRIA), 微軟研究院和卡內基梅隆大學聯合發表 的第一個試用版 EverCrypt密碼庫 在珠穆朗瑪峰項目的框架內開發並使用形式驗證可靠性的數學方法。
對於其功能和性能， EverCrypt 與現有的加密庫非常接近 (OpenSSL)，但與它們不同的是，它提供了額外的可靠性和安全性保證。
例如： 驗證過程歸結為定義詳細規範 描述程序的所有行為 以及書面代碼的數學證明 符合準備的規格。
與基於證據的質量控制方法不同， 驗證提供可靠的保證 該程序將僅按照開發人員的預期運行，並且不存在特定類別的錯誤。
例如，符合規範 保證內存的安全工作並且不存在導致緩衝區溢出的錯誤、取消引用指針、訪問已釋放的內存區域或雙重釋放內存塊。
什麼是EverCrypt？
永遠的密碼 提供強大的類型和值檢查：組件永遠不會將參數傳遞給不兼容的其他組件，也不會訪問其他組件的內部狀態。
輸入/輸出行為 完全符合簡單的數學函數操作，在加密標準中定義。
防範攻擊 在第三方渠道中， 計算過程中的行為 （例如，執行的持續時間或對某些內存的訪問的存在） 它不依賴於處理的機密數據。
項目代碼 用功能語言F *編寫 （F星） , 提供依賴類型和細化的系統，這使得可以使用SMT公式和輔助測試工具為程序建立精確的規範（數學模型）並確保正確性和無差錯執行。
F* 代碼在 Apache 2.0 許可證下分發，最終的 C 模塊和彙編程序在 MIT 許可證下分發。
根據參考代碼F *， 生成彙編程序、C、OCaml、JavaScript 以及網絡彙編代碼。
代碼的某些部分 準備好的 該項目已在 Firefox、Windows 內核中使用 ， Tezos和VPN Wireguard。
EverCrypt組件
在本質上， EverCrypt 結合了 HACL* 和 Vale 之前兩個不同的項目，基於它們提供統一的API，使其適合在實際項目中使用。
HACL *用低寫* 旨在提供用於 C 程序的加密原語 他們使用 libsodium 和 NaCL 風格的 API。
該項目 淡水河谷開發了一種特定的語言 域以在彙編器中創建驗證。
約 110 萬行 HACL 代碼 * Low 語言 * 和 Vale 代碼 25 萬行 它們是用通用語言F*重寫的大約70萬行代碼，該語言也在開發中 作為Everest項目的一部分。
EverCrypt庫的第一個版本 具有經過驗證的功能 以下密碼算法 在 C 或彙編版本中建議的（當使用庫時）
其中，項目頁面重點介紹了：
- 哈希算法：SHA2、SHA3、SHA1 和 MD5 的所有變體
- 身份驗證代碼：HMAC over SHA1、SHA2-256、SHA2-384 和 SHA2-512，用於數據源身份驗證
- HKDF密鑰生成算法（基於HMAC的提取和擴展密鑰導出函數）
- ChaCha20 流密碼（未優化的 C 版本可用）
- Poly1305 消息認證算法 (MAC)（C 和彙編版本）
- 橢圓曲線 Curve25519 上的 Diffie-Hellman 協議（基於 BMI2 和 ADX 指令進行優化的 C 和彙編版本）
- 分組密碼模式 AEAD（認證加密）ChachaPoly（非優化C版本）
- AEAD AES-GCM 塊加密模式（具有 AES-NI 優化的彙編版本）。
在第一 alpha版本，代碼驗證已完成 很大程度上，但仍有一些未被覆蓋的區域。
另外， API尚未穩定，它將被擴展 在以下Alpha版本中 （計劃統一所有API的結構。
其中缺陷還包括對x86_64架構的支持（第一階段主要目標是可靠性，第二階段將實現優化和平台）。
來源： https://jonathan.protzenko.fr