计算机科学家可以像数学家可以证明定理一样肯定地证明程序中没有错误。这些进步被用于增强从无人机到Internet的各个领域的安全性。

在2015年春季，一群黑客试图闯入名为Little Bird（“鸟”）的无人驾驶直升机。该直升机与美国特种部队最喜欢的飞机的载人版本相似，位于亚利桑那州的波音公司。黑客有一个先机：在工作之初，他们就可以访问控制计算机的子系统之一。他们只能破解主要的机载飞行计算机并获得对无人机的控制权。

在项目开始之初，红队黑客团队就可以像在家中使用WiFi一样轻松地破解直升机系统。在接下来的几个月中，DARPA工程师实施了一种新的安全机制，即一种无需强制征收的软件系统。小鸟系统的关键参数不能使用现有技术来破解，其代码可以作为数学证据。而且，尽管该团队可以使用六周时间来访问无人机，并且对计算机系统的访问超出了真正的黑客团队的访问能力，但他们无法破解Bird的防御能力。

“他们无法破解或破坏运营，” 凯瑟琳·费舍尔（Kathleen Fisher）说，塔夫茨大学（University of Tufts University）计算机科学教授，高保障网络军事系统（HACMS）项目经理。 “结果，DARPA代表站起来说，哦，天哪，您实际上可以在重要系统中使用该技术。”

反对黑客的技术是一种称为形式确认的编程风格。与通过非正式方式编写并通常仅通过性能评估的普通代码不同，经过正式验证的软件看起来像是数学证明：每个语句在逻辑上都遵循前一个语句。可以以与数学定理相同的确定性来验证整个程序。

“您编写了描述程序行为的数学公式，并使用概念验证工具测试了此语句的有效性，” Microsoft Research正式确认和安全性研究人员Brian Parno说。

创建正式确认的程序的愿望几乎一直存在于计算机科学本身的领域。长期以来，这仍然是不可能的，但是过去十年在“形式方法”领域的成就使这种方法更接近于常规实践。如今，正在资助的学术团体，美国军事项目以及微软和亚马逊等技术公司中研究软件的正式确认。

随着在线进行的重要任务数量的增加，人们的兴趣也在增加。当计算机孤立地存在于家庭和办公室中时，编程错误只是个麻烦。现在，他们在网络上的计算机上打开了安全漏洞，使任何知识渊博的人都能渗透到计算机系统中。普林斯顿大学计算机科学教授，程序验证负责人安德鲁·阿佩尔（Andrew Appel）

说：“在20世纪，当程序出错时，它很糟糕，很可能会跌落，好吧，上帝保佑她。” 但是在21世纪，错误可以为黑客提供一种控制程序并窃取您的数据的方式。他说：“从一个可以容忍的错误开始，它已经成为一个漏洞，而且情况更加糟糕。” 凯瑟琳·费舍尔

完美程序的梦想

1973年10月，Essger Dijkstra提出了创建无错误代码的想法。晚上，在会议上的一家旅馆里，他突然想到了如何使编程更加数学化。后来，他解释了这个想法，他说：“我激动地头脑，早上2点30分起床，写了一个多小时。”该材料是他1976年硕果累累的《编程学科》的开篇，该书与查尔斯·霍亚尔（Charles Hoare）（像获得图灵奖的迪杰斯特拉（Dijkstra ）一样）一起定义了在编写程序中使用正确性证明的观点。

但是计算机科学没有遵循这个想法，主要是因为多年来使用形式逻辑规则来确定程序的功能似乎是不切实际的，甚至是不可能的。

形式化定义是一种确定程序具体功能的方法。形式确认是一种毫无疑问地证明程序代码完全符合此定义的方法。想象一下，您正在编写一个自动机器人程序，将您带到杂货店。在操作级别，您可以确定机器人必须达到的目标运动-它可以在路径的起点和终点转动，减速或加速，打开或关闭。您的程序将包括这些基本操作，并以正确的顺序排列，以便最终您可以到达商店，而不是机场。

测试程序运行状况的传统方法是通过测试。程序员为程序提供了大量输入数据（单元测试），以确保其行为正常。如果您的程序定义了机器人移动的算法，则可以测试它在许多不同点之间的行程。这样的测试可确保在大多数情况下程序的正确运行，这对于大多数应用程序是足够的。但是单元测试不能保证该软件将始终正常运行-您无法对照所有可能的输入数据检查程序。即使该算法适用于所有目的地，也始终有可能在极少数情况下（或如他们所说的在“边界条件”下）会表现出不同的行为，并打开安全漏洞。在实际程序中，此类错误可能很简单，例如缓冲区溢出，程序会复制比实际所需更多的数据，并覆盖计算机内存的一部分。这个看似无害的错误很难消除，并且为黑客攻击提供了一个漏洞-薄弱的门铰链打开了通往城堡的道路。

“软件中某个地方有一个漏洞，这是一个漏洞。 “很难检查所有可能输入的所有路径，” Parno说。

这些规范比去商店要复杂得多。例如，程序员可能需要一个程序，按照收到文件的顺序对文件的接收日期进行公证并加注日期。在这种情况下，规范应指示计数器始终在增加，并且程序不应允许用于签名的密钥泄漏。

用人类语言，这很容易描述。将规范转换为计算机可以理解的正式语言要困难得多-这解释了编写程序的主要问题。

“在本质上，构建一个计算机可以理解的正式规范是困难的，” Parno说。“在顶层很容易说出“不要让密码泄漏”，但是您需要考虑如何将其转化为数学定义。”

另一个示例是对数字列表进行排序的程序。试图为她的规范制定规范的程序员可以提出以下建议：

对于列表中的每个项目j，请确保j≤j + 1

但是即使在此正式规范中（要确保列表中的每个元素都小于或等于下一个元素），也会出现错误。程序员假定输出将包含修改后的输入。如果列表为[7，3，5]，则他希望程序返回[3，5，7]。但是程序[1、2]的输出将满足规范-因为“它也是一个排序列表，但不是您可能期望的列表，” Parno说。

换句话说，很难将程序应该做什么的想法变成正式规范，以排除对程序的任何不正确解释。给出的示例描述了最简单的排序程序。现在，想象一下更抽象的描述，例如密码保护。“这在数学上是什么意思？对于这样的定义，可能有必要写一个数学描述来说明“保持秘密”的含义，或者对于加密算法来说是安全的。” Parno说。“我们考虑了所有这些问题，并在他们的研究中取得了进步，但实施起来可能非常棘手。”

块安全

实际上，有必要写出规范和附加注释，以便软件得出有关代码的结论。一个程序，包括其正式确认，可能是为相同目的编写的常规程序大小的五倍。

使用适当的工具（可以帮助程序员创建防弹程序的编程语言和辅助程序）可以稍微减轻这种负担。但在1970年代，它们不存在。 “当时，科学和技术的许多方面还不够成熟，因此到1980年代，计算机科学的许多领域对此都失去了兴趣，”经过正式验证的计算机系统组织DeepSpec的首席研究员Appel说。

尽管工具有所改进，但在确认程序时仍遇到了另一个障碍：完全不确定是否需要它。尽管对该方法的爱好者表示，小的错误会导致大的问题，但其他方法引起了人们的注意，即基本上计算机程序运行良好。是的，有时它们崩溃了，但是-丢失了一些未保存的数据，或者有时重新启动了系统，似乎不必为将程序的每个部分毫不费力地转换为形式逻辑语言而付出代价。随着时间的流逝，即使那些起源于计划确认的人也开始怀疑其好处。在1990年代，甚至Hoar也承认规范可能是解决不存在的问题的耗时解决方案。在1995年，他写道：

( ) , … , , .

然后是互联网，它对空中旅行代码中的错误所做的处理与感染时相同：当所有计算机相互连接时，不舒服但可以容忍的错误会导致日益严重的安全问题。

“我们还不完全了解，”阿佩尔说。 “有一些程序可供所有Internet黑客使用，如果该程序有错误，则可能会成为漏洞。”

当研究人员开始了解由Internet构成的安全威胁的严重性时，程序确认即将返回。首先，研究人员在形式方法的基本部分上取得了进展。这是对Coq和Isabelle等辅助程序的改进；逻辑系统的发展（相关类型的理论）提供可帮助计算机评估代码的开发平台； “操作语义”是一种语言，具有正确的词来表达程序的要求。

“从人类语言规范开始，您就遇到了歧义，” 微软研究院副总裁珍妮特·温说。 -任何自然语言都包含歧义。在正式的规范中，您基于数学写下了准确的描述以解释您想要从程序中得到什么。”

Microsoft Research的Janette Wing

此外，正式的方法研究人员还重新定义了他们的目标。在1970年代和1980年代，他们希望创建经过全面测试的计算机系统，从电子电路到程序。如今，大多数研究人员致力于系统的小型但最关键或易受攻击的部分-例如，操作系统或加密协议。

Wing说：“我们并不是说我们将证明整个系统100％正确，甚至是电子电路。” -这样的说法是荒谬的。我们能做或不能做的都是准确的。”

HACMS项目展示了如何通过描述计算机系统的一小部分来实现出色的安全性保证。该项目的第一个目标是制造一款坚不可摧的娱乐直升机。 Quad随附的软件是整体的-也就是说，通过获得对其中一部分的访问权，黑客就可以访问所有其他部分。两年来，HACMS团队一直将控制计算机中的代码分为几部分。

团队使用Fisher所谓的“高可信度构建块”重写了软件体系结构-允许程序员证明代码纯净的工具。其中之一提供了证据，证明他们已进入其中一个单位，因此无法将特权升级到其他单位。

后来，程序员在“鸟”上安装了此类软件。在红队的测试中，她可以访问控制直升机某些部分的系统的一部分，例如摄像机，但不能访问主要功能。从数学上保证了黑客的失败。费舍尔说：“他们以机器可验证的方式证明了黑客将无法超越系统分区，因此这不足为奇。” “这与定理是一致的，但是进行测试总是有用的。”

审计后的第二年，DARPA将项目的工具和技术应用于军事技术的其他领域，例如卫星和自动卡车。新的举措与过去十年中正式确认的方式相吻合：每个成功的项目都会鼓励下一个。费舍尔说：“原谅这个原则的复杂性不再有效。”

上网查询

安全性和可靠性是启发形式方法的两个主要目标。每天，对改进的需求变得越来越明显。 2014年，一个正式描述会发现的小软件错误为Heartbleed错误开辟了道路，该错误有可能破坏互联网。一年后，几个“合法”黑客证实了对汽车联网的最严重担忧，从而获得了对吉普切诺基的远程控制。

随着比率的提高，正式方法研究人员设定了越来越雄心勃勃的目标。由Appel领导的DeepSpec团队（也在HACMS上工作）正在尝试构建一个复杂的，经过全面测试的系统，作为Web服务器。如果成功的话，该项目将从国家科学基金会获得1000万美元的资助，它将汇集过去十年中许多较小的成功项目。研究人员已经创建了多个经过验证的安全组件，例如操作系统的内核。 Appel说：“到目前为止，还没有将这些组件集成到特定于规范的接口中。”

在Microsoft Research，程序员有两个雄心勃勃的项目。第一个是Everest，其目标是创建经过验证的HTTPS版本，该协议是Wing称为“互联网的致命弱点”的一种用于保护Web浏览器安全的协议。

第二个是为复杂的网络物理系统（如无人机）创建已确认的规范。该项目有重大困难。尽管常规程序需要单独，明确的步骤，但无人机控制程序仍使用机器学习来基于连续的环境数据流做出概率决策。在如此程度的误差下如何做出逻辑决策或将其描述为正式规范，还远未达到显而易见的目的。但是直到最近十年，形式化方法才取得了长足的进步，负责项目的Wing乐观地认为研究人员将能够解决所有这些问题。

存在完整的代码

完美程序的梦想

块安全

上网查询

More articles: