程序员都是凡人，但数学则是不朽的。通过让编程变得更数学化，计算机科学家希望能消除向黑客敞开大门的编程错误。研究人员在 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
| Algorithm | C version | ASM version | Agile API |
|---|---|---|---|
| AEAD | |||
| AES-GCM | ✔︎ (AES-NI + PCLMULQDQ) | ✔︎ | |
| ChachaPoly | ✔︎¹ | ✔︎ | |
| Hashes | |||
| MD5 | ✔︎² | ✔︎ | |
| SHA1 | ✔︎² | ✔︎ | |
| SHA2 | ✔︎ | ✔︎ | |
| SHA3 | ✔︎ | ||
| Blake2 | ✔︎ | ||
| MACS | |||
| HMAC | ✔︎⁴ | ✔︎ | |
| Poly1305 | ✔︎³ (+ AVX + AVX2) | ✔︎ (X64) | |
| Key Derivation | |||
| HKDF | ✔︎⁴ | ✔︎ | |
| ECC | |||
| Curve25519 | ✔︎ | ✔︎ (BMI2 + ADX) | |
| Ed25519 | ✔︎⁵ | ||
| Ciphers | |||
| Chacha20 | ✔︎ | ||
| AES128, 256 | ✔︎ (AES NI + PCLMULQDQ) | ||
| AES CTR | ✔︎ (AES NI + PCLMULQDQ) |
¹: does not multiplex (yet) over the underlying Poly1305 implementation
²: insecure algorithms provided for legacy interop purposes
³: 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
