Infer试用以及扫描原理分析

Infer作为facebook 开源的使用 ocaml 开发静态代码检测工具，作为公司的产品调研对象，本文就其使用和原理两方面进行分析。

GitHub：https://github.com/facebook/infer

教程：https://infer.liaohuqiu.net/

Usage

# Gradle
infer -- gradle <gradle task, e.g. "build">
infer -- ./gradlew <gradle task, e.g. "build">
# Maven
infer -- mvn <maven target>

检测能力

Common：

• Divide By Zero
• Null dereference
• Resource leak
• Integer Overflow
• Unreachable Code

Java：

• Injection（SQL，Shell，XSS，JS）
• Deadlock
• Untrusted Deserialization、File、URL、…
• Inconsistent Subclass Parameter Annotation(重载方法@NotNull不一致等)

C/C++ and Objective-C：

• Memory leak
• Parameter not null checked
• Ivar not null checked
• Premature nil termination argument
• Uninitialized Value

Bugs reported only in Objective-C：

• Retain cycle
• Ivar Not Null Checked

Android：

• Create Intent From URI

更详细的列表在 https://fbinfer.com/docs/next/all-issue-types

但是定位到源代码：https://github.com/facebook/whitebox-infer/blob/master/whitebox-infer/src/base/IssueType.ml后，发现其还能检测其存在注入类型的漏洞，不知为何没有扫描到。

规则编写

• Infer AI
  自定义过程内分析和过程间分析实现，https://fbinfer.com/docs/next/absint-framework：

  module Analyzer =
    AbstractInterpreter.Make
      (ProcCfg.Backward(ProcCfg.Exceptional))
      (TransferFunctions)
  module Summary = Summary.Make (struct
      type summary = SiofDomain.astate
      let update_payload astate payload =
        { payload with Specs.siof = Some astate }
      let read_from_payload payload =
        payload.Specs.siof
    end)

• Infer AL

  DEFINE-CHECKER STRONG_DELEGATE_WARNING = {
          // 一个属性若包含“delegate”且不包含“queue”，那么它不应该定义为string
      LET name_contains_delegate =
          declaration_has_name(REGEXP("[dD]elegate"));
      LET name_does_not_contain_queue =
          NOT declaration_has_name(REGEXP("[qQ]ueue"));
      SET report_when =
          WHEN
             name_contains_delegate
             AND name_does_not_contain_queue
             AND is_strong_property()
          HOLDS-IN-NODE ObjCPropertyDecl;
      SET message = "Property or ivar %decl_name% declared strong";
      SET suggestion = "In general delegates should be declared weak or assign";
      SET severity = "WARNING"
    };

• Infer
  Quandary(https://github.com/facebook/infer/blob/master/infer/tests/codetoanalyze/java/quandary/.inferconfig)

  {
    "force-delete-results-dir": true,
    "quandary-sources": [
      {
        "procedure": "codetoanalyze.java.quandary.ExternalSpecs.privateData*",
        "kind": "PrivateData"
      },
      {
        "procedure": "codetoanalyze.java.quandary.InterfaceSpec.source",
        "kinds": ["PrivateData", "Other"]
      }
    ],
    "quandary-sinks": [
      {
        "procedure": "codetoanalyze.java.quandary.ExternalSpecs.loggingSink1",
        "kind": "Logging",
        "index": "1"
      },
      {
        "procedure": "codetoanalyze.java.quandary.ConstructorSink.<init>",
        "kind": "Other",
        "index": "0"
      }
    ],
    "quandary-sanitizers": [
      {
        "procedure": "codetoanalyze.java.quandary.ExternalSpecs.sanitizer"
      }
    ],
    "quandary-endpoints": [
      "codetoanalyze.java.quandary.MyService"
    ]
  }

试用

Webgoat检测到16个问题，14个空引用和2个资源泄露：

扫描InsecureBankv2:

优势

• 增量分析

• 能够分析大规模程序

特色

分离逻辑（separation logic）和双向假说推理（bi-abduction），霍尔逻辑和抽象解释，分离逻辑用来检测bug，双向假说推理用来做增量分析。

分离逻辑

一开始用于内存管理的逻辑

$$x\mapsto y * y\mapsto x$$

$x \mapsto y$ 指指针x指向值y（x points to y），$A*B$指A和B处于分离的两块内存中（and separately），因此以上公式被叫做（x 指向y，同时y指向x），可以用下图表示：

接着使用Hoare三元组$\{pre\}prog\{post\}$，表示程序行为，$pre$指前置条件，$prog$指程序片段$post$为后置条件。例如使用Hoare三元组描述一个关闭资源的函数：

$$\{r\mapsto open\}closeResource(r)\{r\mapsto closed\}(spec)$$

它说明，一个正确的关闭资源的函数运行前，r资源应该是打开的，运行后r资源应该是关闭的，如果不符合则代码有问题。

那么若有两个资源$r_1$和$r_2$仅关闭$r_1$可以表示成：

$$\{r_1\mapsto open * r_2\mapsto open\}closeResource(r_1)\{r_1\mapsto closed * r_2\mapsto open\}(use)$$

这里使用了一个小规范（spec）去更新了一个大规范（use），更一般的，我们有：

$$\{pre\}prog\{post\}\rightarrow\{pre*frame\}prog\{post*frame\}$$

这一规则也被称为逻辑分离中的frame规则，$frame$描述了不变的状态，属于来自于就像动画场景中背景（frame）——动画场景中背景不会变。

这一规则用于数学推理，它揭示了逻辑推理应该聚焦于程序访问资源的那一块逻辑，并且分离的两块可以独立分析。

双向假说推理

A推出B表示为：

$$A \vdash B$$

在传统逻辑推理中，一个推理问题被定义为：

• 给定假设A和目标G

• 找到一个M，使如下公式成立：

  $$A \land M \vdash G$$

应用到分离逻辑问题，即：

$$A * M \vdash G$$

双向假说推理将问题拓展成：

$$A*?antiframe \vdash G*?frame$$

即infer需要找到一对$antiframe$和$frame$让上式成立。

这在做增量扫描是很重要。

为了说明问题，例如我们有如下函数：

lst_nd* q(lst_nd *y) { // Inferred Pre: list(y) 
    lst_nd *x, *z;
    x=malloc(sizeof(lst_nd)); x->tail=0;
    z=malloc(sizeof(lst_nd)); z->tail=0; // Abducted: list(y), Framed: z|->0 
    merge(x,y); // Obtained Post: list(x)*z|->0 
    merge(x,z); // Obtained Post: list(x) 
    return(x);
} // Inferred Post: list(ret)
void merge(lst_nd *x,lst_nd *y){//SUMMARY ONLY 
    // Given Pre: list(x) * list(y)
    // x=x+y
} // Given Post: list(x)

要分析merge有没有空指针，有

$$\{x\mapsto list * y\mapsto list\}merge(x,y)\{x\mapsto list\}$$

如果开始分析q到第5行，我们有：

$$A=x\mapsto 0 *z \mapsto 0$$

但是我们的前提条件是$G=x\mapsto list * y\mapsto list$那么开始推导：

$$x\mapsto0 *z \mapsto 0 * ?antiframe \vdash x\mapsto list * y \mapsto list * ?frame$$

因此 $antiframe=y\mapsto list$且$frame=z\mapsto 0$，这说明，如果想要分析q()函数有没有空指针，那么我们现在只需要分析$y\mapsto list$是成立就行了。

这意味着，如果将来发新版本，若q()函数不变，则不需要再分析该函数，只需要分析改变的那些函数有没有改变$y \mapsto list$即可。

总结

Infer目前的检测能力只局限于空指针和数据泄露问题，然而在检测项中发现了更多，怀疑是开源的是缩水的版本，而其增量分析的思想值得扫描器借鉴，其可用来完成commit级别的SAST和Serveless的安全检测。