iOS Infer 静态代码分析

杂谈

• Monoidics创建于2009年，专长是分析和核对软件稳定性及安全性。该公司的Infer Static Analyzer产品可帮助检测代码的安全漏洞，以防止类似内存溢出、非法指针引用等错误的出现。此外，另一款名为Infer X-Ray的产品能帮助工程师视觉化检测软件的质量，及识别需要改进的关键区域风险。
• Facebook已经收购英国手机代码验证软件开发商Monoidics。交易完成后，一部分Monoidics工程师将加入Facebook伦敦办事处办公。Facebook将采用Monoidics研发的手机代码验证和Bug分析技术

理论基础（程序验证）

• Hoare Logic(霍尔逻辑)：Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家C. A. R. Hoare开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。
• Separation Logic and Bi-abduction：分离逻辑是霍尔逻辑的一种扩展。
  • facebook infer使用逻辑来推理程序的执行,但是通过这种方式来推理上百万行代码量的应用时会变得非常困难。从理论上讲，需要检查的代码数量会多过预计的数量。这样的规模和速度需要更高级的数学模型，Facebook Infer使用了两种技术: 逻辑分离和bi-abduction。
  • 逻辑分离是使Facebook Infer分析能够推断出应用存储的独立小部分的一种理论，从而不用考虑每一步存储的完整性。因为考虑每一步的存储完整性对当今的大型可寻址虚拟内存处理器来说是一个很蛋疼的事。
  • Bi-abduction是一种逻辑推理技巧，可以使Facebook Infer挖掘到应用代码独立部分的行为特性。在其运行时把这些特性存储下来之后，Facebook只需要分析软件中发生改变的部分，其他的部分可以直接套用先前的分析结果。
  • 结合这几种方法，我们的分析器能够在数分钟之内在上百万行代码中找到被修改的代码中存在的复杂问题。

摘录

• 历史 : 从代码检查理论到为十多亿人服务的蜕变

  • 软件的自动检查在计算机科学社区是一个长期依赖的目标。Facebook Infer在这个领域构建了一个基本实现， 包含霍尔逻辑和抽象解释。在加入facebook之前，我们参与到了其他基础设施的开发工作，“逻辑分离”作为能够实现软件自动检查的结果出现在人们的视野中。

  • 逻辑分离是在计算机科学领域的一个重大突破-一种新的数学逻辑被用于描述计算机内存的变化（类似于布尔逻辑用来描述电路）。我们专注于将这个理论运用和自动化,创建一系列原型工具(例如Smallfoot, Space Invader, Abductor)来支撑这些推理逻辑，最终发现了bi-abduction是模块化分析程序的一种有效形式。

  • 基于上述研究成果,我们2009年创建了一个名为Monoidics的公司。Monoidics在2013年加入Facebook，从那以后我们采用持续开发和部署的风格来开发我们的产品，在我们的分析器团队和facebook移动软件开发工程师的不断努力的迭代开发下我们的分析器得到了很大的提升。我们也展示了当运用到facebook代码库时代码检查技术能够得到快速的发展。

• 展望未来

  • 程序检查是一个有着活跃研究社区和前景光明的领域。在facebook,我们说过这趟旅行我们只完成了1%。在程序检查领域还有很多的工作需要我们去完成。但是，随着我们的不断努力，我们相信这个领域的成果会让软件工程师解放出更多的价值。我们可以展望未来，有你的帮助，程序检查技术能够提供更多、更有用的技术来使得我们的代码更可靠、更高效。

About Infer

• Infer是facebook用OCaml开发的一个用于对Java，C，Objective-C代码进行静态检查、分析的工具。用于在发布移动应用之前对代码进行分析，找出潜在的问题。Facebook 使用该工具来分析 Facebook 的 App，包括 Android 、iOS、Facebook Messenger 和 Instagram 等。目前，它主要来检查以下错误类型：空指针的间接引用、资源和内存泄漏，这几种bug在移动开发中举足重轻且比较致命。
• 任何人都可以使用 Infer 检测应用，这可以将那些严重的 bug 扼杀在发布之前，同时防止应用崩溃和性能低下。
• 工作流中的应用
  • 静态分析工具通常在开发阶段使用。它们的本质是一个测试工具，是作为开发过程或CI/CD工作流中的一个步骤。它们不能代替调试器，因为它们工作的时候代码已经编译完成。它们也不能代替生产环境中的错误追踪器，因为只有当代码在生产环境暴露后，动态输入刚好命中时才会产生。但是在这两个环境之间存在一个空间，在这个地方，像Infer的工具是非常有用的。例如，你可以将Infer做为一个开发环境与生产环境中间的步骤。Infer在这种情景下，能帮助你在上线之前预先发现那些明显的bug。这能给你的用户防止一些问题，至少减少你Takipi面板上的问题，如果你使用Jenkins作为持续开发模型，你可以在每个版本发布的时候运行Infer，然后查看抛出的红色标记。

Limitations,etc

• 你必须清楚的知道：当你run Infer on your project，你可能得到非常好的结果，但也可能不会。
• 尽管facebook根据自己代码仓库的代码很好的修复了Infer的一些问题，但将Infer应用于其它任意的代码库的时候，仍然会碰到很大的错误警告。
• 在将Infer应用到自己的代码上时，即便我们得到的结果是有缺陷的，但仍然可能会有一些参考价值，我们可以根据这些分析结果改进我们的代码；至少我在测试我们项目的代码时发现了多个很难发现的bug：比如strong式的delegate，add可能为nil的object到数组中，以及潜在的内存泄露。
• 目前Infer能report这样的一些bug types，典型的比如：

• null pointers
• memory or resource leaks

• 因为技术或者误报率问题，还没有report的有：
  • Array bounds errors
  • Cast exceptions
  • Leaking of tainted data
  • Concurrency race conditions

安装Infer

• 建议使用brew安装，虽然有墙，源码编译安装相对痛苦

  • brew安装(2016-11-11安装到的是0.9.2版本，在xcode8下测试有问题)：brew install infer

  • 源码安装请参考官方文档

    # Checkout Infer,这一步下载可能略微慢一点，不过肯定可以成功，也可以直接下载https://github.com/facebook/infer/releases/download/v0.9.3/infer-osx-v0.9.3.tar.xz
    git clone https://github.com/facebook/infer.git
    cd infer
    # Compile Infer,这一步会下载一些依赖包，可能会非常慢，且没有提示
    ./build-infer.sh clang
    # Install Infer into your PATH
    export PATH=`pwd`/infer/bin:$PATH
    

基本命令

• 查看Infer的安装路径：where infer

Hello world Objective-C（单个文件）

// Hello.m
#import <Foundation/Foundation.h>

@interface Hello: NSObject
@property NSString* s;
@end

@implementation Hello
NSString* m() {
    Hello* hello = nil;
    return hello->_s;
}
@end

• 执行命令：infer -- clang -c Hello.m #clang前有一个空格，详细分析请参考官方入口文档

Hello world iOS(普通的XCode工程)

• Go to the sample iOS app in infer/examples/ios_hello and run Infer on it: infer -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator

pod式工程

• /Users/test/Downloads/infer-osx-v0.9.3/infer/bin/infer -- xcodebuild -workspace Flight.xcworkspace -scheme FlightApp -configuration Debug -sdk iphonesimulator -arch i386

References

1. Infer中文介绍

• Infer
• AutomatorX
• 霍尔逻辑中文教程