@ 2019.04.10 , 22:14

利用数学工具写出黑客无法攻陷的软件

程序员是人类,但数学是不朽的。通过使编程更具数学性,计算机科学家希望消除可能被黑客利用、泄露数字机密并对现代社会造成普遍困扰的程序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)发布。


支付宝打赏 [x]
您的大名: 打赏金额:

赞一个 (9)