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

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

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

EverCrypt 支持的算法

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

• 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