程序員都是凡人，但數學則是不朽的。通過讓編程變得更數學化，計算機科學家希望能消除向黑客敞開大門的編程錯誤。研究人員在 GitHub 上發布了加密工具?EverCrypt，向這個目標邁出了一大步。就像證明畢達哥拉斯定理那樣，他們能證明 EverCrypt?可完全避開多種黑客攻擊。

EverCrypt 沒有采用常見的編程方法編寫，而是利用了形式化驗證。他們首先明確代碼能做什么，然后證明只能這么做，排除了代碼在特殊情況下偏離的可能性。

EverCrypt 始于 2016 年，是微軟研究院項目?Project Everest?的一部分，當時加密庫是許多軟件的薄弱環節，存在大量 bug。EverCrypt 使用?F*（發音 F star）編程語言編寫和驗證，然后編譯為 C（使用專用編譯器?KreMLin?編譯）和匯編語言的混合。

EverCrypt 支持的算法

EverCrypt 支持的許多算法仍在開發中。在即將發布的版本中，目標是：

• fallback C versions for all algorithms
• NIST P curves
• AES-CBC
• an up-to-date Ed25519

1: does not multiplex (yet) over the underlying Poly1305 implementation
2: insecure algorithms provided for legacy interop purposes
3: achieved via C compiler intrinsincs; no verification results claimed for the AVX and AVX2 versions whose verification is not complete yet
?: HMAC and HKDF on top of the agile hash API, so HMAC-SHA2-256 and HKDF-SHA2-256 leverage the assembly version under the hood
?: legacy implementation

參考?https://www.solidot.org/story?sid=60154