分类
麻省理工学院新闻

自动加密代码生成器正在帮助保护web

系统自动编写优化算法,加密数据在谷歌Chrome浏览器和web应用程序。

几乎每次你打开一个安全的谷歌Chrome浏览器,麻省理工学院开发的一个新的加密系统都会帮助你更好地保护你的数据。

在最近IEEE安全与隐私研讨会上发表的一篇论文中,麻省理工学院的研究人员详细介绍了一个系统,该系统首次自动生成优化的加密代码,这些代码通常是手工编写的。该系统于2018年初投入使用,目前已被谷歌和其他科技公司广泛使用。

本文现在为该领域的其他研究人员演示了如何实现自动化方法来防止在生成密码时出现人为错误,以及如何对系统组件进行关键调整来帮助实现更高的性能。

为了保证在线通信的安全,密码协议运行复杂的数学算法,这些算法对大量数据执行一些复杂的运算。然而,在幕后,一小群专家手工编写和重写这些算法。对于每种算法,它们必须权衡各种数学技术和芯片架构,以优化性能。当底层的数学或架构发生变化时,它们实际上是从头开始的。除了劳动密集型之外,这个手工过程还会产生非最优算法,并经常引入bug,这些bug稍后会被捕获并修复。

计算机科学与人工智能实验室(CSAIL)的研究人员转而设计了“菲亚特密码学”,这是一个为所有硬件平台自动生成并同时验证优化密码算法的系统。在测试中,研究人员发现他们的系统可以生成与最佳手写代码性能匹配的算法,但速度要快得多。

研究人员自动生成的代码填充了谷歌的BoringSSL,这是一个开源的密码库。谷歌Chrome、Android应用程序和其他程序使用BoringSSL生成用于加密和解密数据的各种密钥和证书。据研究人员称,目前大约90%的安全Chrome通信运行他们的代码。

密码学是通过对大数进行运算来实现的。[菲亚特密码学]使它更容易实现的数学算法…因为我们自动化建设的代码并提供证明,代码是正确的,”论文作者亚当Chlipala说CSAIL的研究员和电气工程和计算机科学副教授、编程语言和验证。“这基本上就像取一个在人脑中运行的过程,并充分理解它,以便编写模仿该过程的代码。”

微软研究院(Microsoft Research)的密码学专家乔纳森•普罗岑科(Jonathan Protzenko)没有参与这项研究,他认为这项工作代表着行业思维的转变。

他表示:“在BoringSSL中使用菲亚特加密技术有利于整个(加密)社区。”“(这)是一个迹象,表明时代正在改变,大型软件项目正在认识到,不安全的密码学是一种负担,(并表明)经过验证的软件已经足够成熟,可以进入主流。我希望越来越多的已建立的软件项目将转向验证密码学。或许在未来几年内,经过验证的软件不仅可以用于密码算法,还可以用于其他应用领域。”

加入Chlipala论文的有:第一作者Andres Erbsen和合著者Jade Philipoom和Jason Gross,他们都是CSAIL的研究生;还有罗伯特·斯隆的孟’ 17。

把位

密码学协议使用数学算法来生成公钥和私钥,它们基本上是一长串比特。算法使用这些密钥在浏览器和服务器之间提供安全的通信通道。椭圆曲线密码术(ECC)是目前最流行的一种高效、安全的密码算法。基本上,它通过沿着图形上的一条编号曲线随机选择数值点,为用户生成各种大小的键。

大多数芯片无法将这么大的数字存储在一个地方,因此他们将这些数字简单地分割成较小的数字,存储在称为寄存器的单元上。但是寄存器的数量和它们所提供的存储量因芯片的不同而不同。Chlipala说:“你必须将这些位元分割到许多不同的位置,但事实证明,如何分割这些位元会产生不同的性能结果。”

传统上,编写ECC算法的专家在他们的代码中手工实现这些位分割决策。在他们的工作中,麻省理工学院的研究人员利用这些人类的决定,为任何硬件自动生成一个优化的ECC算法库。

他们的研究人员首先用C编程和汇编语言探索了现有的手写ECC算法的实现,并将这些技术转移到他们的代码库中。这将为每个体系结构生成一个最佳性能算法列表。然后,它使用一个编译器——一个将编程语言转换成计算机能理解的代码的程序——这个编译器已经被证明是正确的。基本上,该编译器生成的所有代码都会经过数学验证。然后,它模拟每个算法,并为每个芯片体系结构选择性能最佳的算法。

接下来,研究人员正在研究如何让编译器在搜索优化算法时运行得更快。

优化编译

还有一个额外的创新可以确保系统快速地选择最佳的位分割实现。研究人员为他们基于coq的编译器配备了一种优化技术,称为“部分评估”,它基本上是预先计算某些变量,以便在计算过程中加快速度。

在研究人员的系统中,它预先计算了所有的位分裂方法。当将它们匹配到给定的芯片架构时,它会立即丢弃所有不适用于该架构的算法。这大大减少了搜索库所需的时间。在系统锁定最优算法后,完成了代码的编译。

在此基础上,研究人员积累了一个最佳方法库,用于为各种芯片架构拆分ECC算法。它现在在BoringSSL中实现,所以用户主要从研究人员的代码中提取。对于新的体系结构和新的数学类型,库也可以自动进行类似的更新。

Chlipala说:“我们实际上已经编写了一个库,它可以一劳永逸地适用于所有可能拆分数字的方法。”“你可以自动探索大数的可能表示空间,编译每种表示来衡量性能,并在给定的场景中选择运行速度最快的一种。”

新闻旨在传播有益信息,英文原版地址:http://news.mit.edu/2019/fiat-cryptography-chrome-android-0617