EverCrypt跨平臺(tái)的現(xiàn)代加密庫(kù)
程序員都是凡人，但數(shù)學(xué)則是不朽的。通過(guò)讓編程變得更數(shù)學(xué)化，計(jì)算機(jī)科學(xué)家希望能消除向黑客敞開(kāi)大門的編程錯(cuò)誤。研究人員在 GitHub 上發(fā)布了加密工具 EverCrypt，向這個(gè)目標(biāo)邁出了一大步。就像證明畢達(dá)哥拉斯定理那樣，他們能證明 EverCrypt 可完全避開(kāi)多種黑客攻擊。
EverCrypt 沒(méi)有采用常見(jiàn)的編程方法編寫，而是利用了形式化驗(yàn)證。他們首先明確代碼能做什么，然后證明只能這么做，排除了代碼在特殊情況下偏離的可能性。
EverCrypt 始于 2016 年，是微軟研究院項(xiàng)目 Project Everest 的一部分，當(dāng)時(shí)加密庫(kù)是許多軟件的薄弱環(huán)節(jié)，存在大量 bug。EverCrypt 使用 F*（發(fā)音 F star）編程語(yǔ)言編寫和驗(yàn)證，然后編譯為 C（使用專用編譯器 KreMLin 編譯）和匯編語(yǔ)言的混合。
EverCrypt 支持的算法
EverCrypt 支持的許多算法仍在開(kāi)發(fā)中。在即將發(fā)布的版本中，目標(biāo)是：
- 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 | ??1 | ?? | |
| Hashes | |||
| MD5 | ??2 | ?? | |
| SHA1 | ??2 | ?? | |
| SHA2 | ?? | ?? | |
| SHA3 | ?? | ||
| Blake2 | ?? | ||
| MACS | |||
| HMAC | ??? | ?? | |
| Poly1305 | ??3 (+ AVX + AVX2) | ?? (X64) | |
| Key Derivation | |||
| HKDF | ??? | ?? | |
| ECC | |||
| Curve25519 | ?? | ?? (BMI2 + ADX) | |
| Ed25519 | ??? | ||
| Ciphers | |||
| Chacha20 | ?? | ||
| AES128, 256 | ?? (AES NI + PCLMULQDQ) | ||
| AES CTR | ?? (AES NI + PCLMULQDQ) |
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