計(jì)算機(jī)科學(xué)家發(fā)布不會(huì)被黑的加密代碼

作者：愛(ài)集微 2019-04-08

來(lái)源：solidot #代碼# #加密#

1.8w

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

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

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

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