（给Python开发者加星标，提升Python技能）
转自：solidot
程序员都是凡人，但数学则是不朽的。通过让编程变得更数学化，计算机科学家希望能消除向黑客敞开大门的编程错误。研究人员在 GitHub 上发布了加密工具 EverCrypt，向这个目标迈出了一大步。
https://github.com/project-everest/hacl-star
就像证明毕达哥拉斯定理难以，他们能证明 EverCrypt 可完全避开多种黑客攻击。
EverCrypt 没有采用常见的编程方法编写，而是利用了形式化验证。他们首先明确代码能做什么，然后证明只能这么做，排除了代码在特殊情况下偏离的可能性。
EverCrypt 始于 2016 年，是微软研究院项目 Project Everest 的一部分，当时加密库是许多软件的薄弱环节，存在大量 bug。
推荐阅读
（点击标题可跳转阅读）
如何用树莓派和 Kali Linux 搭建一个便携式的黑客工作站
觉得本文对你有帮助？请分享给更多人
关注「Python开发者」加星标，提升Python技能
喜欢就点一下「好看」呗~