Facebook 的大规模静态分析

静态分析工具可以在不运行目标程序的情况下检查后者的源代码，并获得关于它的结论。Facebook一直在开发高级静态分析工具，这些工具采用了类似程序验证的推理技术。本文介绍的工具（Infer和Zoncolan）针对的是与服务崩溃和安全性相关的问题，它们会执行可以很复杂的，跨越许多过程或文件的推理，并以尽可能平滑的方式集成到工程流程中创造价值。

要点

• 高级静态分析技术针对源代码执行深度推理，这种技术可以扩展到大型（如 1 亿 LOC）工业级代码库上。

• 静态分析应该很好地平衡遗漏的错误（假负）和无处理报告（假正）。

• 所谓"diff-time"部署，也就是在代码审查中向开发者提交问题的过程，对于及早发现错误和提升修复率是很重要的。

这些工具在代码更改和代码审查过程中被用作机器辅助手段。Infer 针对的是我们的移动应用及后端C++代码，涉及的代码库有数千万行的规模；它已帮助开发人员在代码进入生产环境前修复了超过 10 万个报告的问题。Zoncolan 针对的是1亿行Hack代码，并且集成在安全工程师的工作流程中。它帮助工程师修复了成千上万的安全和隐私错误，比 Facebook 针对此类漏洞的其他检测方法表现都更加出色。我们将展示在开发和部署这些分析工具时遇到的人力和技术挑战，以及我们所学到的经验教训。

工业和学术界已经在静态分析领域做了大量的工作，这里就不再赘述。我们会使用类似学术前沿可能遇到的复杂技术来实现大规模扩展，并展示我们的理论基础和成果。我们的目的是为其他关于工业级静态分析和形式方法的报告提供补充，希望这些观点能够助力静态分析未来的研究与进一步的工业应用。

接下来将讨论推动我们工作的三大方面：严重错误、人员和已处理/遗漏的错误。剩余内容涉及我们开发和部署分析工具的经验、它们的影响以及支撑它们的技术。

Facebook 静态分析的背景

严重错误

我们使用静态分析来预防可能影响产品的错误，并凭借工程师的判断及生产数据来告诉我们哪些错误最重要。

静态分析开发人员必须意识到错误的影响是有高有低的：根据其上下文和性质，不同的错误可能具有不同级别的重要性或严重性。很少使用的服务上的内存泄漏错误可能就不如允许攻击者访问未授权信息的漏洞那么重要。此外，错误类型的频率也可能影响其重要性。如果某种崩溃（例如 Java 中的空指针错误）每小时发生一次，那么它可能就比每年只发生一次的严重性类似的错误更重要。

我们有几种方法来收集关于严重错误的数据。首先，Facebook 会维护生产中的崩溃等错误的统计数据；其次，我们有一个“错误赏金”计划，第三方可以在 Facebook 或 Facebook 系应用（如 Messenger、Instagram 或 WhatsApp）中报告漏洞；第三，我们有一个内部计划来跟踪最严重的错误（SEV）。

Facebook 对严重错误的理解使我们开始关注高级分析技术。相比之下，最近的一篇论文指出：“谷歌内广泛部署的所有静态分析工具都比较简单，但有些团队会针对有限的领域（例如 Android 应用程序）开发特定于项目的分析框架进行过程间分析”，并且他们给出了完全合理的理由。本文中我们会解释为什么 Facebook 决定广泛部署过程间分析（跨越多个流程）工具。

人员和部署

并非所有的错误都是相同的，用户也是一个道理；因此，我们根据目标受众（也就是分析工具要部署到的位置涉及的人员）使用不同的部署模型。

对于给定平台上的所有或各种工程师涉及的多种错误类别，我们使用了“diff-time”部署：分析器作为机器人参与代码审查，在工程师提交代码更改时自动添加注释。之后我们统计出了惊人的数据：diff-time 部署的修复率达到 70％，而传统的“离线”或“批量”部署（在工作流程之外向工程师提供错误列表）的修复率为 0％ 。

如果目标受众是公司中一小批领域安全专家，我们会使用另外两个部署模型。在“diff-time”中，安全相关问题被推送给待命的安全工程师，因此她可以按需注释正在进行的代码更改。此外还有离线检查，用来在代码库中查找给定错误的所有实例或搜索历史数据，这个功能提供了用于查询、过滤和分类所有警报的用户界面。

总体而言，我们的部署主要关注这些工具服务的人员和他们的工作方式。

已处理报告（actioned report）和遗漏的错误（missed bug）

工业级静态分析工具的宗旨是帮助人们工作：在 Facebook，这意味着直接帮助我们的工程师，并间接帮助使用我们产品的用户。我们已经看到了部署模型对工具成功与否的影响。为了进一步理解这种关系并改进我们的工具，我们引入了两个概念：已处理报告和（可观察到的）遗漏的错误。

根据报告的错误执行的处理类型取决于部署模型及错误的类型。在 diff-time 中，一项处理（Action）是对 diff 的更新，其会移除静态分析报告。在 Zoncolan 的离线部署中，如果问题足够严重，需要产品团队跟进，则报告可以触发安全专家为产品工程师创建任务。与人工安全审查或错误赏金报告相比，Zoncolan 发现的 SEV 数量更多。根据我们的统计，有 43.3％的严重安全漏洞是通过 Zoncolan 检测到的。截至发稿时 Zoncolan 的“处理率”高于 80％，而我们观察到了大约 11 个“遗漏的错误”。

遗漏的错误是以某种方式被观察到，但分析工具没有报告的错误。观察手段取决于错误的类型。针对安全漏洞，我们有错误赏金报告、安全审查或 SEV 审查方法。针对移动应用，我们会记录移动设备上发生的崩溃和应用程序无响应事件。

已处理报告和遗漏的错误涉及静态分析学术领域中"真正（true positive）"和"假负（false negative）"的经典概念。"真正"是对一个潜在错误的报告，这个错误理论上可以在程序运行时出现（实践中是否出现是另一回事）；“假正"则是不可能发生的错误。静态分析的常识是，控制假正非常重要，因为它们会让工程师产生"狼来了"的印象，不再重视新的警报。之前关于工业级静态分析的文章中已经强调了这一点。“假负"是指可能有害但长时间未被发现的错误。影响安全性或隐私的错误未被发现可能导致有人偷偷利用漏洞。在实践中，较少的"假正"通常（尽管并非总是）意味着更多的"假负”，反过来更少的"假负"意味着更多的"假正”。例如，一种控制假正的方法是当你不确定一个错误是否真实时就不报告；但这种方式在减少分析报告（比如通过忽略某些路径或启发式过滤策略）的同时也会遗漏某些错误。反过来说，如果你想发现并报告更多错误，可能就会引入更多虚假行为。

我们之所以对高级静态分析感兴趣，用经典术语来理解可能就是：假负对我们很重要。但需要指出的是，众所周知假负的数量是难以量化的（未知错误到底有多少？）。同样，人们很少意识到假正率对于大规模且快速变化的代码库来说是一项挑战：人们在代码发生变化时判断所有报告的真假是非常耗时的。

虽然真正和假负是有价值的概念，但我们更关注的是处理率和（观察到的）遗漏的错误。

挑战：速度、规模和准确性

第一个挑战是 Facebook 代码库的庞大规模和它的更改速度。我们在服务端有超过 1 亿行 Hack 代码，Zoncolan 在 30 分钟内就能处理完毕。此外我们还有数百万行移动（Android 和 Objective C）代码和后端 C++代码。Infer 在 diff-time 部署中快速处理代码修改（平均在 15 分钟内）。所有代码库每天都有成千上万的更改，我们的工具会检查每一次更改。对于 Zoncolan 来说，这相当于每天分析一万亿行代码（LOC）。

基于简单的局部流程检查来扩展分析程序是相对容易的。最简单的形式是 linters，它提供语法风格建议（例如“你调用的方法是弃用的，请考虑重写”）。这种简单检查自有其价值，并在包括 Facebook 在内的主流公司中广泛部署，这里就不多谈。但是如果需要超越局部检查的推理，比如说学术前沿的静态分析方法，那么扩展到千万级或亿级的 LOC 上就很困难了；支持 diff-time 报告所需的增量可扩展性也是如此。

Infer 和 Zoncolan 都使用了与前沿学术领域类似的技术。Infer 使用一种基于分离逻辑理论的分析技术，并使用一种新颖的定理证明器通过推理技术来猜测假设。另一种 Infer 分析技术涉及最近发表的关于并发分析的研究结果。Zoncolan 实现了一种新的模块化并行污点分析算法。

但 Infer 和 Zoncolan 是怎样扩展的呢？他们共享的核心技术特性是组合性和精心设计的抽象性。本文主要谈论 Infer 和 Zoncolan 的功能，而非其技术属性；但我们会概述它们的基础理念，更多技术细节可参阅在线附录。

与准确度相关的挑战则与已处理报告和遗漏的错误紧密相关。我们试图基于错误类别和目标受众的情况在这些问题之间取得平衡。可能错过的问题越严重，对遗漏错误的容忍度就越低。因此，对于移动应用（如 Messenger、WhatsApp、Instagram 或 Facebook）中可能引起崩溃或性能下降的问题，我们对遗漏错误的容忍度就比风格化的 lint 建议（例如，不要使用弃用的方法）之类更低。对于可能影响我们基础设施安全性或用户隐私的问题，我们对假正的容忍度也很高。

Facebook 的软件开发

Facebook 实行持续软件开发策略：几千名程序员向主代码库（master）提交代码更改（diff）。Master 和 diff 分别类似 GitHub 的 master 分支和拉取请求。开发人员共享代码库的访问权限，并将通过审查的 diff 提交给代码库。有一套持续集成系统（CI 系统）用来确保代码持续构建并通过某些测试。更改代码时分析工具会介入，工具会直接在代码审查工具里把它们发现的情况注释出来。

Facebook 网站最初是用PHP编写的，然后移植到Hack，后者是 Facebook 开发的 PHP 进化版本。Hack 代码库有超过 1 亿行代码。它包括 Web 前端、内部 Web 工具、用于从第一方和第三方应用访问社交图的 API、隐私感知数据抽象以及针对查看者和应用程序的隐私控制逻辑。Facebook、Messenger、Instagram 和 WhatsApp 这些移动应用大都是用 Objective-C 和 Java 编写的。多数后端服务选择了 C++语言。移动和后端代码都有几千万行之多。

我们之所以很重视 Facebook 的高级静态分析，用经典术语可以这么说：假负对我们来说很重要。

虽然网站和移动应用使用相同的开发模型，但它们的部署方式是不同的。这会影响错误重要性的判断和修复错误的方式。在网站这边，Facebook 把新代码直接部署到自己的数据中心，错误修复可以直接上传到我们的数据中心，而且每天上传多次，还能按需立即上传。在移动应用这边，Facebook 需要用户从 Android 或苹果商店下载新版本；新版本每周都会更新，但我们对移动端的错误控制力没那么强——因为即便修复版本已经上线了，也可能没法下载到某些用户的手机上。

常见的运行时错误——例如空指针异常和除零错误等——在移动端比服务端更难修复。另一方面，服务端安全和隐私错误会严重影响 Web 端和移动端的 Facebook 用户，因为隐私检查是在服务端执行的。因此 Facebook 投资了很多工具来增强移动应用的可靠性与服务端代码的安全性。

使用 Infer 快速前进

Infer 是 Facebook 中用在 Java、Objective C 和 C++代码上的静态分析工具。它能报告内存安全、并发性和安全性（信息流）相关的错误，及 Facebook 开发人员建议的许多特定错误类型。Infer 运行在 Facebook、Instagram、Messenger 和 WhatsApp 的 Android 和 iOS 应用内部，以及我们的后端 C++和 Java 代码上。

Infer 源于一项关于分离逻辑的程序分析的学术研究，围绕这项研究诞生了一家创业公司（Monoidics Ltd.），它于 2013 年被 Facebook 收购。Infer于 2015 年开源 ，并被亚马逊、Spotify 和 Mozilla 等许多公司采用。

Diff-time 连续推理

Infer 的主要部署模型基于对代码更改的快速增量分析。当 diff 被提交给代码审查时，在 Facebook 的内部 CI 系统中会运行一个 Infer 实例（图 1）。Infer 分析一个 diff 时不需要处理整个代码库，因此速度很快。

图 1 持续开发

Infer 的目标是针对每个 diff 平均运行 15 到 20 分钟以内，其中包括了检查源代码存储库、构建 diff 以及在基本和（可能的）父提交上运行的时间。一般来说它不会超时，但我们会持续监控性能指标以检测出需要更长时间的回归，发现这种情况后我们会努力缩短其运行时间。处理完一个 diff 之后，Infer 会将注释写入代码审查系统。在最常用的默认模式下它只报告回归：也就是 diff 引入的新问题。“新”问题是使用错误等效值计算出来的，这个值使用了错误类型和与位置无关的错误信息的哈希值，并且对重构、删除或添加代码导致的文件移动和行号更改非常敏感；其目的是避免展示的警告被开发人员误认为是已经存在的。快速报告需要与开发人员的工作流程紧密结合。相比之下，当 Infer 运行在完整程序模式下时可能需要一个多小时才能处理完毕（具体取决于应用）——对于 Facebook 的 diff-time 来说太慢了。

人为因素

Infer 的 diff-time 推理有多重要，出现失败时就能明显感受到了。第一次部署是批量而非连续的。在这种模式下，Infer 会在整个 Facebook Android 代码库上每晚运行一次，并生成一系列问题。我们手动查看了问题，并将它们分配给我们认为最有能力解决问题的开发人员。

反馈是令人惊讶的：几乎什么回应都没有。我们向开发人员分配了 20-30 个问题，结果几乎没有一个被解决。我们努力将假正率降低到了看来低于 20％的水平，然而修复率——也就是报告的问题中开发人员解决掉的比例——几乎为零。

接下来我们把 Infer 切换到了 diff-time 上。工程师的反应同样令人惊叹：修复率飙升至 70％以上。程序分析一样，假正率没变，但部署在 diff-time 时效果要好得多。

虽然这种结果让 Infer 团队的静态分析专家感到惊讶，但 Facebook 的开发人员觉得很正常。他们向我们提供的解释可以概括为下面的术语：

diff-time 部署解决的一个问题是心理背景切换的影响。如果开发人员正在解决一个问题，同时又看到了另一个问题的报告，那么他们必须把心理背景切换到第二个问题上，这可能又费时又打断人的思路。如果代码审查中有机器人参与，背景切换问题就在很大程度上得到了解决：程序员打开审查工具与人类审查者讨论他们的代码，此时心理背景已经切换好了。这也说明了及时性有多重要：如果机器人在一个 diff 上了运行一小时或更久，它参与的效率可能就很差了。

diff-time 部署解决的第二个问题是相关性。在代码库中发现一个问题时，是不是将其分配给正确的人员可能并不重要。极端情况下引发这个问题的人员可能已经离职了。此外，就算你认为自己找到了熟悉这部分代码的人，这个问题也可能与他们过去或当前的工作无关。但如果我们注释一个引入问题的 diff，那么它很有可能（但并不绝对）是相关的。

心理背景切换一直都是心理学研究的主题，正是 Facebook 工程师向我们传授的集体智慧，让我们意识到它和相关性都是如此重要。请注意，其他人也提到了在代码审查期间给出报告的一些好处。

在 Facebook，我们正在积极努力将其他测试技术迁移到 diff-time 部署上。我们还支持学界研究用于 diff-time 报告的增量模糊测试和符号执行技术。

过程间错误

Infer 发现的许多错误涉及跨越多个过程或文件的推理。OpenSSL 的一个例子如下：

apps/ca.c:2780: NULL _ DEREFERENCE
pointer 'revtm' last assigned on line 2778 could be null
and is dereferenced at line 2780, column 6
2778. revtm = X509 _ gmtime _ adj (NULL, 0); 2779.
2780. i = revtm->length + 1;

这个问题是过程 X509 _ gmtime _ adj()在某些情况下可以返回 null。总的来说，Infer 找到的错误跟踪有 61 个步骤，而 null 的源头——对 X509 _ gmtime _ adj()的调用有 5 步的深度，并在调用深度 4 处遇到 null 返回。这个错误是我们向 OpenSSL 报告的 15 个问题中的一个，它们都已经修复了。

Infer 通过组合推理发现了这个错误，组合推理能发现过程间错误，同时扩展到数百万 LOC 上。它推导出一个前置条件/​​后置条件规范，近似于 X509 _ gmtime _ adj 的行为，然后在推理其调用时使用该规范。这个规范包含 0 作为其中一个返回值，这会触发错误。

在 2017 年，我们查看了几个类别的错误修复，发现对于一些（空引用、数据争用和安全问题）错误来说，超过 50％的修复是针对过程间错误。如果我们只部署局部过程分析的话就会遗漏过程间错误。

并发

Infer 最近添加了名为 RacerD 分析的并发功能，这也是程序分析研究者与产品工程师间良好互动的一个例子。这个功能是在 2016 年初开始开发的，一开始由并发分离逻辑推动。项目进行 10 个月后，来自 Android 的 News Feed 的工程师发现了我们的工作并联系了我们。 他们计划将 Facebook 的 Android 应用的一部分从顺序架构转换为多线程架构。这样就必须在并发上下文中使用为单线程架构编写的几百个类：这种转换可能会引入并发错误。 他们要求提供过程间功能，因为 Android UI 排列在树中，每个节点一个类。 跨过程调用链（有时跨越多个类别）可能会导致争用，而最高层级几乎不会出现变异：局部过程分析会遗漏大多数争用。

我们之前计划用一年时间来开发校对工具，但彼时 Android 工程师的项目已经开始了，需要尽快提供帮助。所以我们转向一个最小可行产品为工程师提供服务——它必须够快，具有可处理的报告，并且不会遗漏太多产品代码的错误（但不用管基础设施代码）。该工具借鉴了并行分离逻辑的思想，但我们放弃了彻底解决争用的理想。相反，我们建立了一个“完整性”定理，就是说在某些假设下，分析器的理论变量只报告真正。

学术研究中涉及的高级静态分析可以大规模部署并为一般代码提供价值。

这个分析工具会检查 Java 程序中的数据争用——两个并发的内存访问，其中一个是写入。图 2（顶部）中的示例说明：如果我们在此代码上运行 Infer 则不会发现问题。未受保护的读取和受保护的写入不会因为它们位于同一线程而争用。但如果我们包含其他争用方法，那么 Infer 将报告争用，如图 2 底部所示。

图 2。一个简单的例子，捕获了 Android 应用中一个常见的安全模式

成果

自 2014 年以来，Facebook 的开发人员已经解决了由 Infer 标记的 100,000 多个问题。Infer 的大部分成果来自 diff-time 部署，但它也会批量运行以跟踪 master 中和 fixathon 中提出的问题及其他计划。

截至 2018 年 3 月，RacerD 数据争用检测器已经处理了超过 2,500 个修复。它通过搜索潜在的数据争用帮助 Facebook 的 Android 应用程序从单线程转换为多线程架构，这一过程无需程序员插入注释来说明哪些内存是由哪个锁保护。这种转换提升了滚动性能。谈到分析器的作用时，Facebook 的 Android 工程师 Benjamin Jaeger 表示：“没有 Infer，News Feed 中的多线程就没法实现。” 截至 2018 年 3 月，尚未发现 Infer 在过去一年中遗漏了哪个 Android 数据争用错误。

2018 年 3 月并发分析的修复率约为 50％，低于之前的一般 diff 分析。我们的开发人员强调他们很欣赏这些报告，因为并发错误很难调试。这也佐证了我们之前关于平衡处理率和错误严重性的观点。

总的来说，Infer 报告了 30 多种类型的问题，从深入的过程间检查到简单的局部过程检查和 lint 规则都有所涉及。并发支持包括对死锁和饥饿的检查，在过去一年中修复了数百个“应用未响应”错误。Infer 最近还实现了一项安全性分析（“污点”分析），该分析已应用于 Java 和 C++代码；它借用了 Zoncolan 的想法理念。

用 Zoncolan 保证安全性

我们一开始开发并使用 Hack 的一个目的是想对 Facebook 核心代码库做更强大的分析。Zoncolan 是我们构建的静态分析工具，我们用它在 Hack 代码库中查找可能导致安全或隐私侵害的代码和数据路径。

图 3 中的代码就是 Zoncolan 找到的一个漏洞。如果第 21 行的 member_id 变量包含值…/…/users/delete_user/，则可以将此表单重定向到 Facebook 上的其他任何表单。在提交表单时，它将调用一个指向https://face-book.com/groups/add_member/…/…/users/delete_user/的请求，该请求将删除用户的帐户。图 3 中漏洞的机制是攻击者控制在

图 3. Zoncolan 阻止的错误示例。它可能导致攻击者删除用户帐户。攻击者可以在第 5 行提供输入，导致重定向到第 20 行的 Facebook 上的其他任何表单。

面向 SEV 的静态分析开发

Zoncolan 是我们与 Facebook 应用安全团队合作设计并开发的。Zoncolan 报告的警报参考了应用安全团队发现的安全漏洞。

Zoncolan 的设计始于安全工程师提供给我们的 SEV 列表。看着这些错误，我们会问自己：“我们如何用静态分析来捕获它？” 大多数历史错误都不会再现，因为编程语言或安全框架阻止了它们复现——例如，XHP 广泛应用后我们就能构建无 XSS 网页了。我们意识到剩下的错误涉及到不可信数据的过程间流动，这些数据会直接或间接地流入某些特权 API。使用静态污点流分析可以自动检测出此类错误，这种分析会跟踪来自某些不可信源的数据，调查它们如何接触或影响代码库（汇点）的某些敏感部分中的数据。

当安全工程师发现新漏洞时，我们会评估该类漏洞是否适合静态分析。如果答案是肯定的，我们会设计出新规则的原型，并根据工程师的反馈进行迭代来优化，最终达到假正/假负的合理平衡。当我们觉得新规则已经够好了之后，它就会在生产环境中的所有 Zoncolan 运行中启用。我们采用标准的 Facebook 应用安全严重性框架来确定每个漏洞的影响程度，级别从 1（最佳实践）到 5（SEV）。安全影响级别为 3 或更高的漏洞被认为是严重的。

分析扩展

我们面临的一大挑战就是将 Zoncolan 扩展到超过 1 亿 LOC 的代码库。由于我们设计了一种新的并行、组合式和非均匀静态分析方法，Zoncolan 在 24 核服务器上只用不到 30 分钟就完成了代码库的全面分析。

Zoncolan 构建了一个依赖图，将方法与其潜在的调用者关联起来。它用这张图来安排针对各个方法的并行分析。在相互递归方法的例子中，调度器会迭代对方法的分析，直到它稳定下来——也就是说不再发现新的流。合适的运算符（静态分析学科中称为拓宽）确保迭代的收敛。值得一提的是，即使学术界已经有了完善的污点分析的概念，我们也要开发新算法才能扩展到我们的代码库这么大的规模上。

漏斗部署

图 4 是 Zoncolan 部署模型的图形示意。这个漏斗部署模型优化了错误检测，目的是支持 Facebook 的安全性：Zoncolan 的 master 分析会查找新发现漏洞的所有现有实例。Zoncolan 的 diff 分析可以避免在代码库中（重新）引入漏洞。

图 4。Zoncolan 的漏斗部署

Zoncolan 定期分析整个 Facebook Hack 代码库以更新 master 列表。目标受众是执行安全审查的安全工程师。在 master 分析中，我们公开了所有发现的警报。安全工程师对给定项目或给定类别的所有警报都感兴趣。他们使用仪表板分类这些警报，仪表板可以按项目、代码位置、数据源和/或目标、跟踪的长度或功能来过滤。当安全工程师发现错误时，他/她向产品组提交任务并提供如何加强代码安全性的指导。当警报是假正时，他/她向 Zoncolan 的开发人员提交任务，并解释警报为假的原因。随后 Zoncolan 开发人员会改进工具以提高分析的精确度。对某个类别进行了广泛测试后，Zoncolan 团队与应用安全团队一起评估是否可以推广到 diff 分析。这个过程中我们通常会通过输出过滤来改善信号，例如根据过程间跟踪的长度和端点的可见性（外部还是内部？）等因素来过滤。截至发稿时，大约 1/3 的 Zoncolan 类别可用于 diff 分析。

Zoncolan 会分析每段 Hack 代码更改，如果 diff 引入了新的安全漏洞就会报告警报。目标受众是：diff 的作者和审查者（Facebook 软件工程师，非安全专家），以及当值轮换的安全工程师（拥有有限的时间预算）。在适当的时候，当值人员验证报告的警报，阻止 diff，并提供支持来改善代码的安全性。对于信号非常高的类别，Zoncolan 则充当安全机器人：它绕过安全当值人员直接在 diff 上注释。注释提供了有关安全漏洞的详细说明和利用漏洞的方法，并包括了对过去事件（如 SEV）的引用。

最后请注意，漏斗部署模型可以扩展安全修复，而不会降低 Zoncolan 实现的整体覆盖范围（也就是说不会遗漏错误）：如果 Zoncolan 确认新问题的信号水平不足以在 diff 上自动注释，但需要由专家查看，就会将其推送到待命队列。如果警报的级别更低，那么问题将在 diff 提交后进入 Zoncolan 的 master 分析。

成果

Zoncolan 已经在 Facebook 部署了两年多，首先提供给安全工程师，然后是软件工程师。它已经成功阻止了数千个漏洞进入 Facebook 的代码库。图 5 比较了六个月时间中 Zoncolan 与安全工程师采用的传统程序（例如人工代码审查/测试和错误赏金报告）预防的 SEV（也就是严重级别 3-5 的错误）数量。如图所示，Zoncolan 比人工安全审查或错误赏金报告预防的 SEV 更多。根据我们的统计，有 43.3％的严重安全漏洞是通过 Zoncolan 检测到的。

图 5。六个月时间内 Zoncolan 与安全审查和错误赏金报告找出的严重错误的数量对比（颜色越深越严重）。

图 6 中的图表显示了 Zoncolan 在部署漏斗的不同阶段发现的处理错误基于安全影响级别的分布。数量最多的类别是 master 分析的，因此它显然是最大的存储桶。但只看 SEV 时，diff 分析大幅超过了 master 分析——diff-time 阻止了 211 个严重问题，而 master 分析中检测到了 122 个。总的来说，我们的数据显示 Zoncolan 的错误处理率接近 80%。

图 6。六个月内修复的所有错误基于 Zoncolan 的漏斗部署和错误严重性（颜色越深越严重）的分布。

我们还使用传统的安全程序来统计遗漏的错误（也就是存在 Zoncolan 类别的漏洞），但该工具未能报告它们。到目前为止，我们已经有大约 11 个遗漏的错误，其中一些是由工具中的错误或不完整的建模引起的。

组合和抽象

支撑我们分析工具的技术特性是组合和抽象。

组合的概念来自语言学语义：如果复合短语的含义是根据其各个部分的含义和组合它们的方式来定义的，则这个语义是组合的。同样的道理可以应用在程序分析上：如果复合程序的分析结果是根据其各个部分的分析结果和组合它们的方法来定义的，则程序分析是组合的。在程序分析中应用组合性时有两个关键问题：

1. 如何简洁地表示程序的含义？

2. 如何有效地组合意义？

对于（1），我们需要抽象出过程的完整行为来找出组件含义的近似，并只关注与分析相关的属性。例如对于安全分析而言，当输入参数包含用户控制的字符串，并丢弃字符串的有效值时，我们可能只对函数返回用户控制的值感兴趣。更正式地说，静态分析的设计者定义了一个适当的数学结构，称为抽象域，允许我们更简洁地近似这个大函数空间。静态分析的设计需要抽象域足够精确来捕获感兴趣的属性，还要足够粗糙来让问题在计算上易于处理。“过程意义的抽象”在分析学科中通常被称为过程摘要。

问题（2）的答案主要取决于为摘要的表示选择的特定抽象域。之所以组合分析与精心设计的抽象域可以大规模扩展，直观来说是因为每个过程只需要访问几次，并且代码库中的许多过程可以独立分析，这样就容易并行化了。组合分析甚至可以具有运行时，这个运行时是时间的线性组合，从而分析各个过程。为此，合适的抽象域（例如限制或避免析取）还应包含分析单个过程的成本。

最后，组合性分析是自然增量的——改变一个过程不需要重新分析其他过程。这对于快速 diff-time 分析是很重要的。

总结

本文介绍了 Facebook 的静态分析项目，回顾了我们如何开发程序分析以响应来自生产代码和工程师要求的需求。Facebook 的重要代码和问题非常多，为此组建分析专家团队是值得的，我们已经看到了它给公司带来的好处（例如使用 Infer 支持多线程 Android News Feed，以及在 Zoncolan 的进化中检测 SEV 级别的问题）。虽然我们的主要职责是为公司服务，但我们相信这些经验和技术可以带来更广泛的影响力。例如，Infer 已被亚马逊、Mozilla 和 Spotify 等企业采用；我们还发现了新的科学成果，并提出了新的科学问题。事实上，我们作为（前）研究人员在工业组织中工作得出的经验是，在紧密的反馈循环中让科学和工程竞争前行是可行的，在工业中进行静态分析时甚至是有利的。

我们给行业专业人士的建议是：学术界提到的先进静态分析技术可以大规模部署，为一般代码提供价值。对于学者我们的建议是：从工业角度来看，这个领域似乎有许多路径尚待开发，因此存在很多研究机会，从中可以诞生许多面向未来的工具。

原文链接

Scaling Static Analyses at Facebook