0%

Infer试用以及扫描原理分析

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

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

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

Usage

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

检测能力

官网上看到能够检测到的问题有:

Java:

  • Resource Leak
  • Null dereference

C and Objective-C

  • Resource leak
  • Memory leak
  • Null dereference
  • Parameter not null checked
  • Ivar not null checked
  • Premature nil termination argument

Bugs reported only in Objective-C

  • Retain cycle

参见:https://infer.liaohuqiu.net/docs/infer-bug-types.html

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

试用

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

1566373102585

扫描InsecureBankv2:

1566370930925

优势

  • 增量分析

  • 能够分析大规模程序

原理

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

分离逻辑

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

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

static/images/SepSplit.jpg

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

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

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

这里使用了一个小规范(spec)去更新了一个大规范(use),更一般的,我们有:

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

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

双向假说推理

A推出B表示为:

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

  • 给定假设A和目标G

  • 找到一个M,使如下公式成立:

应用到分离逻辑问题,即:

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

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

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

为了说明问题,例如我们有如下函数:

1
2
3
4
5
6
7
8
9
10
11
12
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有没有空指针,有

如果开始分析q到第5行,我们有:

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

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

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

总结

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