程序員都是凡人，但數(shù)學(xué)則是不朽的。通過(guò)讓編程變得更數(shù)學(xué)化，計(jì)算機(jī)科學(xué)家希望能消除向黑客敞開(kāi)大門(mén)的編程錯(cuò)誤。研究人員在 GitHub 上發(fā)布了加密工具 EverCrypt，向這個(gè)目標(biāo)邁出了一大步。

        就像證明畢達(dá)哥拉斯定理難以，他們能證明 EverCrypt 可完全避開(kāi)多種黑客攻擊。

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

        EverCrypt 始于 2016 年，是微軟研究院項(xiàng)目 Project Everest 的一部分，當(dāng)時(shí)加密庫(kù)是許多軟件的薄弱環(huán)節(jié)，存在大量 bug。