程序员是人类，但数学是不朽的。通过使编程更具数学性，计算机科学家希望消除可能被黑客利用、泄露数字机密并对现代社会造成普遍困扰的程序bug。

现在，随着EverCrypt(一款数字加密工具)的发布，一组计算机科学家朝着宏伟目标迈出了重要的一步。研究人员能够证明——证明毕达哥拉斯定理的那种证明——对于黑客用来攻陷以往程序的主要手段，最新的安全工具是完全无懈可击的。“我们的意思是，我们通过数学方法证明，我们的代码不会受到这种攻击。”巴黎Inria的计算机科学家Karthik Bhargavan表示。

EverCrypt程序并非是按照常见的方式编写。通常，程序员团队先创建他们希望能够满足某些需求的软件。完成后，他们会测试。如果它顺顺当当地完成了目标，并且不会出现预期外的行为，程序员就得出结论：该软件能用了。

然而，bug通常只出现在极端的“边界情况corner cases”下。近年来，许多最具破坏性的黑客工具都利用了极端情况。

相比之下，卡内基梅隆大学计算机科学家Bryan Parno和同事已经明确限定了他们程序的功能，然后证明了它的行为真的被局限在已知的范围内，排除了在特殊情况下代码可能以意想不到的方式偏离正轨的可能性。这种策略被称为“形式验证”。

因为完全定义复杂软件系统(如网络浏览器)的功能几乎是不可能的，所以研究人员转而关注那些既重要又适合数学定义的程序。 EverCrypt是处理密码或私人信息编码和解码的软件库。这些加密库具有天生的数学性。它们涉及算术与素数和对规范几何对象(如椭圆曲线)的操作。定义加密库并不是一件容易的事。

EverCrypt的开发始于2016年，作为Project Everest的一部分，后者是由微软研究院主持的项目。当时——现在仍然如此——加密库是许多软件应用程序中的一个软肋。它们运行缓慢，拖累了所属应用程序的整体性能，且充满bug。

创建EverCrypt的主要挑战是发明出一款一体化的开发平台，可以容纳研究人员为经过验证的加密库添加的所有不同属性。该平台既需要C++这样的传统编程语言的能力，又能如Isabelle和Coq这样的证明辅助程序一样提供逻辑语法和结构——数学家们已经使用了这两款软件很多年。当EverCrypt项目启动时，还并没有这样的一体化平台，因此他们自己开发了一种——名为F *的编程语言。它把数学和编程放到了平等的地位。

“我们将这些事情统一到一个连贯的框架中，这样就可以减少编写程序和数学证明之间差异，”Bhargavan说，“你可以像软件开发人员一样写代码，但同时你也可以写数学证明。”

他们证明，EverCrypt并没有可供黑客利用的bug，如缓冲区溢出。实际上，可以证明它排除了对所有可能的极端情况的敏感性。他们还证明，EverCrypt每次都能获得正确的数学加密结果——它从不执行错误的运算。

但EverCrypt最引人注目的承诺来自对完全不同方向上的安全弱点——当坏人通过观察程序如何操作来推断加密消息的内容时，就会出现的情况——的防护。

例如，有经验的观察者可能知道加密算法为值赋予“0”时，程序的运行速度稍快，而在向值添加“1”时稍慢。通过测量算法加密消息所花费的时间量，观察者可以判断出消息的二进制表示是否包含更多的0或1——并最终推断出完整的消息。

“传统加密算法的原理本身，或者实现算法的方式，正在泄露你的信息。”Bhargavan说。这种“旁道攻击”是近年来几次最臭名昭着的黑客事件的幕后推手，其中包括幸运13袭击。研究人员证明，EverCrypt绝不会被利用以上述方式泄露信息。

虽然EverCrypt可以免疫许多攻击类型，但它并不意味着绝对安全的软件时代已然来临。Protzenko指出，人们总是会想出未知的方式来利用程序漏洞，无法证明EverCrypt是永远安全的。

此外，即使是经过验证的加密库也必须与许多其他软件(如操作系统和许多常见的桌面应用程序)协同工作，这些软件通常是未经验证的，并且可能在可预见的未来也不会通过形式验证。

由于未经验证的协同应用可能会抵消加密库的安全性，Project Everest希望使用尽可能多地使用经过验证的软件来配合EverCrypt。该计划的首要目标是完成安全超文本传输协议(HTTPS)的全面验证，该协议可保护大多数网络通信的安全。

本文译自 quantamagazine，由译者 majer 基于创作共用协议(BY-NC)发布。