安全与性能（I）
原文标题：Safe and Efficient, Now 作者：Oleg Kiselyov 原文地址：Lightweight Static Guarantees 本文确立了一种严谨的编程风格（事实上，十多年前就有人确立过）。这一风格通过利用成熟的、实用的语言（如 OCaml、Scala、Haskell 等，某种程度上 Java 和 C++ 也可纳入这一范畴）中的现有类型系统，从而静态地保障一系列广泛的安全性质。 永远不会对空指针解引用，或取空列表的头部元素。 始终对用户提供的输入进行消毒。 只使用数组界内的索引值访问（动态分配的）数组，且数组大小不需要静态可知。 这一技术与模块化开发、分离编译、命令式编程、原生的可变数组、间接索引以及一般递归等编程语言特性兼容。使用这种技术编写的程序所需的运行时检查更少，因此不但更可靠，而且更高效。这一技术并非旨在取代基础的代码形式化验证方法，而是补充并结构化了这种方法：我们可以用形式化方法证明（小而简单的）安全内核的正确性，然后用这一技术将安全内核的静态保障从内核扩展到整个程序。 在研究的过程中，我们发现有两个点令人惊讶：首先，我们上面所列举的内容居然是可行的；其次，这些技术是如此古老（可追溯到 Morris 1973 年的论文），如此简单，但却鲜为人知。 导言 OpenSSL 的心血［Heartbleed］漏洞给人们带来的惨痛回忆已逐渐淡去——毕竟，可被利用的安全漏洞常常都有。但心血漏洞仍然令人瞩目，因为漏洞本身是如此的微不足道，人们却花费了大量精力来修复它的影响。 与许多其他的此类性质的漏洞一样，心血漏洞的出现并未经过太多的酝酿——正如 SSL 的心跳［heartbeat］功能开发者所解释：「我当时正在改进 OpenSSL，提交了大量的漏洞修复，并添加了一些新功能。不幸的是，在其中一个新功能中，我漏了验证某带长度的变量的长度。」而 OpenSSL 的代码审核——「显然也没有注意到这一遗漏。」这位开发者又补充道：「因此这个漏洞从开发分支进入了发布版本。」最终在发布版本中潜藏了两年，一直未被（公开）发现。 最终修复这一漏洞的 OpenSSL 补丁证明：这一漏洞本身确实微不足道，不过是一条语句 memcpy(bp, pl, payload); 这条语句从输入数据包（自指针 pl 开始）中拷贝 payload 大小的数据载荷，然后将拷贝出来的内容放入输出数据包缓冲（自指针 bp 开始）。payload 值是从之前的输入数据包中读取的，当恶意攻击者发送的数据包声明它的载荷量是最大有效值，但实际却没有携带任何数据载荷时，问题就来了：在这种情况下 memcpy 没法从接受到的数据包中拷贝（因为已经结束），反而是从 OpenSSL 输入缓冲区的剩余垃圾中拷贝数据。这些「垃圾」实际上是之前剩余的数据，通常包含密码等敏感信息。 另一个令人不安的点在于：如果禁止程序员直接使用 memcpy 这样的低级函数，而是强制其通过一些封装（例如强制检查 pl + payload 地址是否仍在输入数据包内）来调用，像心血漏洞这样的问题本来很容易避免（因为输入数据包的边界很容易获得）。这种调用限制可以在任何具有模块［module］或命名空间［namespace］抽象机制的语言（C++ 等）中实现，甚至也可以在 C 语言中实现： 「抽象」就是关键所在：通过对内部数据和函数的抽象，迫使程序员使用带有安全检查的公开 API。抽象还能通过「避免外部程序污染内部状态」，从而确保一些已经通过安全检查验证的不变式［invariant］在任何情况下都成立——这样，就不必反复地进行某些安全检查了，甚至可以完全不需要检查。因此我们的口号是：「安全和高效，我全都要。」 这编程风格背后的思想其实稀松平常，甚至可以追溯到计算机的洪荒年代：由硬件保障的内存和设备的访问限制。硬件保护层将计算系统分为（受信任的）内核（在特权模式下运行，可执行底层操作）和用户态［user-level］程序，后者只能通过内核公开的 API（系统调用）访问设备，而内核 API（系统调用）会检查正确性和访问权限。譬如，用户态程序不能随意写入磁盘，它们只能执行 open 系统调用；在经过权限和一系列检查后，系统调用返回一个不透明的标记，即文件描述符［file descriptor］。这一描述符代表了「执行规定的的操作的能力［capability］」，还代表了一种「授权成功」的事实，在进一步的操作中就无需重复验证授权。Jame Morris 1973 年发表的论文 «Protection in Programming Language» 首次将操作系统中的部分理念应用到软件开发中，这些理念包括内存保护、身份验证、整理、作用域控制等等。该论文还展示了软件/语言的保护层是如何帮助我们对程序进行本地化、模块化的推理。而自 1973 年以来，编程语言中的抽象设施变得更加广泛和普及，现在是时候充分利用 Morris 的这一洞见了。...