4 月 2 日发布的 EverCrypt 加密代码工具号称能防黑客，真的这么厉害吗？

负责该项目的计算机科学家在《科学》杂志上写道，通过将计算机代码视为数学证明，事实证明该图书馆无法抵御大多数黑客攻击。

据称是一个涵盖简单算术的“软件库”，包括几何和素数。

通常，程序员团队创建软件来实现他们希望实现的某些目标。完成后，他们测试代码；如果软件实现了其目标而没有造成不良后果，则程序员可以断定该软件按预期工作。

软件编码错误通常发生在极端的“危急情况”下，是由“不可能的事情”的完美风暴引发的重大漏洞。近年来许多最具破坏性的黑客攻击都与这种极端情况有关。

相比之下，大多数代码的编写方式没有遵循。卡内基梅隆大学计算机科学家 Bryan Parno 表示：“你可以将问题简化为代码在数学公式中的表现，然后检查该公式是否成立。如果成立，你就知道你的代码具有此属性。”谁参加了。 ”

这项工作于 2016 年开始，是微软研究院领导的工作的一部分。它是用F*语言编写和验证的。 F*是微软研究院开发的基于F♯的依赖型函数式编程语言。