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中漏洞的机制是攻击者控制在
元素的action字段中使用的member_id变量的值。Zoncolan会跟踪不可信数据（例如用户输入）的过程间流动，直到代码库的敏感部分。虚拟调用确实增加了过程间分析的难度，因为工具通常不知道对象的精确类型。为了避免遗漏路径（及错误），Zoncolan必须考虑调用可能解析到的所有函数。
图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）的答案主要取决于为摘要的表示选择的特定抽象域。之所以组合分析与精心设计的抽象域可以大规模扩展，直观来说是因为每个过程只需要访问几次，并且代码库中的许多过程可以独立分析，这样就容易并行化了。组合分析甚至可以具有运行时，这个运行时是时间的线性组合，从而分析各个过程。为此，合适的抽象域（例如限制或避免析取）还应包含分析单个过程的成本。
最后，组合性分析是自然增量的——改变一个过程不需要重新分析其他过程。这对于快速diff-time分析是很重要的。
总结
本文介绍了Facebook的静态分析项目，回顾了我们如何开发程序分析以响应来自生产代码和工程师要求的需求。Facebook的重要代码和问题非常多，为此组建分析专家团队是值得的，我们已经看到了它给公司带来的好处（例如使用Infer支持多线程Android News Feed，以及在Zoncolan的进化中检测SEV级别的问题）。虽然我们的主要职责是为公司服务，但我们相信这些经验和技术可以带来更广泛的影响力。例如，Infer已被亚马逊、Mozilla和Spotify等企业采用；我们还发现了新的科学成果，并提出了新的科学问题。事实上，我们作为（前）研究人员在工业组织中工作得出的经验是，在紧密的反馈循环中让科学和工程竞争前行是可行的，在工业中进行静态分析时甚至是有利的。
我们给行业专业人士的建议是：学术界提到的先进静态分析技术可以大规模部署，为一般代码提供价值。对于学者我们的建议是：从工业角度来看，这个领域似乎有许多路径尚待开发，因此存在很多研究机会，从中可以诞生许多面向未来的工具。
原文链接
- 发表于:
- 本文为 InfoQ 中文站特供稿件
- 首发地址：https://www.infoq.cn/article/l1D3pa3pyDeuhZqVxhy1
- 如有侵权，请联系 cloudcommunity@tencent.com 删除。
相关快讯
扫码
添加站长 进交流群
领取专属 10元无门槛券
私享最新 技术干货
腾讯云开发者
