程序静态分析（Program Static Analysis）是指在不运行代码的方式下，通过词法分析、语法分析、控制流、数据流分析等技术对程序代码进行扫描，验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术。目前静态分析技术向模拟执行的技术发展以能够发现更多传统意义上动态测试才能发现的缺陷，例如符号执行、抽象解释、值依赖分析等等并采用数学约束求解工具进行路径约减或者可达性分析以减少误报增加效率。目前的静态分析工具，无论从科研角度还是实用性角度还有很大的提高余地，国际最好分析工具误报率在5-10%之间。

对于Facebook来说，其开发人员一直在致力于开发高级静态分析工具，这些工具采用类似于程序验证的推理技术。而今天，我们在本文中描述的工具（Infer和Zoncolan）就专门针对与崩溃和Facebook安全性相关的问题，这些工具有时执行跨越许多进程或文件的复杂推理，并且它们试图集成到正常的工作流程中。

这些工具在代码修改时运行，在代码审查进程中起到木马（Bots）的作用。Infer是Facebook 的 Infer 是一个静态分析工具。可以分析 Objective-C， Java 或者 C 代码，报告潜在的问题。Infer的运行原理，捕获编译命令，将文件翻译成 Infer 内部的中间语言。这种翻译和编译类似，Infer 从编译过程获取信息，并进行翻译。这就是我们调用Infer 时带上一个编译命令的原因了，比如: Infer — clang -c file.c, Infer — javac File.java。结果就是文件照常编译，同时被 Infer 翻译成中间语言，留作第二阶段处理。特别注意的就是，如果没有文件被编译，那么也没有任何文件会被分析。总之，Infer的目标是Facebook的移动应用程序以及后端的c++代码，代码库包含数千万行代码。在代码投入运行之前，已经看到开发人员修复了超过10万个报告的问题。

而 Zoncolan的目标是1亿行Hack代码，并且它还被集成在安全工程师使用的工作流程中。目前，它已经修复了数千个安全和隐私漏洞，性能超过了Facebook针对此类漏洞使用的任何其他检测方法。我们将描述在开发和部署这些分析过程中遇到的人和技术挑战，以及我们学到的经验。

接下来，我们将从三个方面来讨论如何深入扩展Facebook上的静态分析：重要的漏洞，人员和相关操作行为的漏洞。

Facebook静态分析的背景

对于漏洞的判断

使用静态分析来防止可能影响产品的漏洞，不过静态分析开发人员必须意识到并非所有漏洞都是相同的：根据运行背景和性质，不同的漏洞可能具有不同级别的重要性或严重性。很少使用的服务上的内存泄漏可能不如允许攻击者访问未授权信息的漏洞那么重要。此外，漏洞类型的频率可能影响决定它的重要性。如果某种崩溃（例如Java中的空指针漏洞）每小时发生一次，那么肯定比一年只发生一次的类似严重漏洞更重要。

目前Facebook有几种方法可以收集有关漏洞的数据：首先，Facebook维护有关运行中发生的崩溃和其他漏洞的统计数据；其次，他们有一个“漏洞赏金”计划，公司外的人可以在Facebook开发的应用程序上报告漏洞，例如，Messenger，Instagram或WhatsApp；第三，他们有一个内部计划来跟踪发生的最严重的漏洞（SEV）。

我们对Facebook问题的理解推动了我们对高级分析的关注，最近的一篇论文指出：

“在Google上广泛部署的所有静态分析都相对简单，尽管一些团队针对有限的领域(如Android应用程序)开发特定于项目的分析框架，这些领域可以进行进程间分析。”

人员和部署情况

并非所有的漏洞都是相同的，因此如何部署模型，还取决于预期的受众(即使用分析工具的研究人员)。

对于针对给定平台上的所有或各种工程师的漏洞类别，我们倾向于“差异时间”部署，在这种部署中，分析人员作为木马参与代码评审，当工程师提交代码修改时自动进行注释。稍后，我们将描述一个惊人的情况，其中差异时间部署的修复率达到70％，其中更传统的“离线”或“批处理”部署（在工作流程之外向工程师提供漏洞列表）的修复率为0％ 。

如果目标用户是公司中规模较小的领域安全专家，我们将使用两个额外的部署模型。根据部署的“差异时间”，安全相关问题被推送给随叫随到的安全工程师，这样他们就可以在必要时对正在进行的代码更改进行评论。此外，为了在代码库中查找给定漏洞的所有实例或进行历史探索，离线检查提供了一个用于查询、筛选和分类所有警报的用户界面。

在所有情况下，我们的部署都关注于我们的工具所服务的人员及其工作方式。

采取的行动和遗漏的漏洞

我们已经了解了部署模型如何影响工具的使用，下面的两个案例会更详细地帮助我们理解这一点，并帮助我们改进已有的静态分析工具，以帮助研究人员采取行动和发现遗漏的漏洞。

由于报告的错误而采取的操作类型取决于部署模型和漏洞类型，在diff时，操作是对diff的更新，它就删除静态分析报告。在Zoncolan的离线部署中，如果漏洞非常重要，需要与产品团队一起跟进，则报告可以触发安全专家为产品工程师创建任务。与手动安全检查或漏洞赏金报告相比，Zoncolan获得的SEV更多。我们测量的43.3％的严重安全漏洞是通过Zoncolan检测到的，截至发稿时，在我们观察到大约11个“遗漏的漏洞”中，Zoncolan的“捕获率”超过了80％。

这些遗漏的漏洞是以某种方式被观察到的，至于观察的手段则取决于漏洞的种类。对于安全漏洞，Facebook有漏洞赏金报告，安全审查或SEV审查。对于我们的移动应用程序，我们会记录移动设备上发生的崩溃和应用程序没有响应的事件。

活跃的报告和遗漏的漏洞与学术静态分析文献中关于真阳性和假阴性的经典概念有关，静态分析中的常识是，保持对假阳性的控制很重要，因为它们会对使用这些工具的工程师产生负面影响，因为它们往往会导致对报告的警报漠不关心。另一方面，假阴性是一种潜在的有害漏洞，可能在很长一段时间内都不会被发现。影响安全性或隐私的未检测到的漏洞可能会导致未检测到的漏洞。在实践中，更少的假阳性通常意味着更多的假阴性，反之亦然。更少的假阴性意味着更多的假阳性（误报）。例如，控制误报的一种方法是，当你不确定漏洞是否存在时，就不报告。但是这种方式 (例如，通过忽略路径或启发式筛选)会产生遗漏漏洞的后果。

我们之所以对Facebook的高级静态分析如此感兴趣，是因为假阴性对我们很重要。然而，需要注意的是，漏洞否定的数量是出了名的难以量化。同样，尽管不太为人所知，但要测量一个快速变化的大型代码库的假阳性率也是一项挑战：随着代码的变化，要判断所有报告是假的还是真的，对人类来说将是极其耗时的。

虽然真阳性和假阴性是有价值的概念，但是我们不会对它们的速率进行研究，而是更多地关注操作速率和观察到的遗漏的漏洞。

静态分析的速度、规模和准确性

Facebook面临的第一个挑战是其庞大的代码库，以及它们所看到的代码迭代速度。在服务器端，我们有超过1亿行Hack代码，Zoncolan可以在不到30分钟的时间内处理这些代码。此外，我们拥有数百万的移动（Android和Objective C）代码和后端C ++代码。Infer在差异时间部署中快速处理代码修改（平均在15分钟内）。所有代码库每天都会看到成千上万的代码修改，我们的工具会在每次代码更改时都会运行。对于Zoncolan来说，这相当于每天分析一万亿行代码。

扩展程序分析相对简单，只在进程的本地基础上执行简单的检查，最简单的形式是查看linter，它提供语法风格建议（例如，“你调用的方法是弃用的，请考虑重写”）。这种简单的检查提供了价值，并在包括Facebook在内的大公司得到广泛应用，不过我们不会在本文中进一步分析它们。

Infer和Zoncolan都使用类似于研究文献边缘的技术。正如我们将要讨论的那样，推断使用一种基于分离逻辑理论的分析，使用一种新颖的定理证明器来实现猜测假设的推理技术。另一种Infer分析涉及最近发表的关于并发性分析的研究结果。由此，Zoncolan实现了一种新的模块化并行污染分析算法。

但是Infer和Zoncolan如何进行规模化分析？它们共享的核心技术特征是组合性和精心设计的逻辑。对于本文的大部分内容，我们将专注于应用Infer和Zoncolan所获得的内容，而不是其技术属性，但我们稍后将概述它们的基础，并在在线附录中提供了更多技术细节。

与准确性相关的挑战与活动报告和遗漏的漏洞密切相关，我们试图在这些问题之间取得平衡，并根据基于漏洞类别和目标受众的预期提供信息。不过由此而遗漏的漏洞会越来越严重，对遗漏的漏洞的容忍度就越低。因此，对于移动应用程序（如Messenger，WhatsApp，Instagram或Facebook）中潜在崩溃或性能退化的漏洞，容忍度低于 linter的建议。对于可能影响我们的基础设施安全或使用我们产品的人的隐私的漏洞，我们对误报的容忍度仍然较高。

Facebook的软件开发

Facebook的软件更新速度非常快，其中主要代码库（master）被数千名提交代码修改（diffs）的程序员所修改，Master和diffs分别类似于GitHub Master分支和pull请求。开发人员共享对代码库的访问权限，并在通过代码审查后将代码库传递给代码库。持续集成系统（CI系统）用于确保代码继续构建并通过某些测试，分析运行代码修改，并通过直接在代码审查工具中评论他们的发现来参与。

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

虽然他们使用相同的开发模型，但网站和移动产品的部署方式不同。这会影响漏洞的重要性，以及可以修复漏洞的方式。对于该网站，Facebook直接将新代码部署到其自己的数据中心，并且可以将漏洞修复程序直接发送到我们的数据中心，每天数次，并在必要时立即发送。对于移动应用程序，Facebook依赖人们从Android或Apple商店下载新版本，新版本每周发布一次，但我们对手机漏洞的控制较差，因为即使发布了修复程序，也可能无法下载到某些人的手机上。

常见的运行时漏洞，例如，空指针异常，除零等，都在移动设备上难以被修复。另一方面，由于隐私检查是在服务器端执行的，服务器端安全性和隐私漏洞会严重影响Facebook Web版本的用户和移动用户。因此，Facebook目前正在开发的工具使移动应用程序更可靠，服务器端代码更安全。

用Infer快速达到分析目的

Infer是一个应用于Facebook的Java，Objective C和C ++代码的静态分析工具，它报告了与内存安全、并发性、安全性（信息流）以及Facebook开发人员提出的更多专业漏洞相关的漏洞。 Infer在Facebook，Instagram，Messenger和WhatsApp的Android和iOS应用程序内部运行，以及在后端C ++和Java代码上运行。

Infer 是由初创企业 Monoidics开发的，Monoidics于2013年被Facebook收购，Infer于2015年开源（www.fbInfer.com），并在亚马逊、Spotify、Mozilla和其他公司中使用。

差时连续推理（Diff-time continuous reasoning）

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

目标是让Infer平均在差异15分钟到20分钟内运行，这包括检查源存储库、构建diff以及在基础和父提交上运行的时间。它通常是这样做的，但我们会不断监控性能，以检测需要更长时间的回归。在本文中，我们会努力缩短运行时间。在运行diff之后，Infer然后将注释写入代码审查系统。在最常使用的默认模式下，它仅报告回归即diff引入的新漏洞。“新”问题是使用漏洞等效概念计算的，该概念使用涉及漏洞消息的漏洞类型和与位置无关的信息的哈希值，以及敏感文件和行号变化引起的重构移动、删除或添加代码。其目的是避免出现开发人员可能认为已经存在的警告。快速报告对于与开发人员的工作流程保持一致非常重要，相比之下，当Infer在整个程序模式下运行时，它可能需要一个多小时（取决于应用程序），在Facebook上的差异时间很慢。