前言

这篇文章主要是体验各种程序分析的工具，对于网上已经写的很好的文章，采取了直接引用的方式。读者应该多了解引用的链接，感兴趣的话可以跟着其他人的文章做一做。

如果需要精通使用，程序分析框架的学习成本还是比较高的。但是强烈建议有时间的读者，可以玩一玩。

Tai-e

首推Tai-e，学习资料中文的看着真是舒服。

首先可以看设计者的演讲视频【静态程序分析框架“太阿”的设计之道_李樾老师】，下面是通用性的程序分析框架的架构图，个人觉得参考意义很大。建议尝试去完成课程的作业，

软文介绍：https://zhuanlan.zhihu.com/p/547780818

发布说明：https://zhuanlan.zhihu.com/p/488957195

论文：https://arxiv.org/abs/2208.00337

代码实现：https://github.com/pascal-lab/Tai-e

Doop

学习资源：http://plast-lab.github.io/feb16-seminar/

项目地址：https://bitbucket.org/yanniss/doop/src/master/

视频讲解：https://www.bilibili.com/video/BV1yz411B7MS

资料和文档都较少，建议多去 Discord 提问。

介绍

Doop 是一个以 指针分析 算法为中心的 Java 静态分析框架，使用 Datalog 规则形式表达的各种分析的集合。维护两套规则：

• LogicBlox：使用 LogiQL，Datalog 程序的构建块以 谓词 的形式出现，例如 Person("John")、Parent("John", "Johnny jr")，利用 规则（IDB 逻辑）从已知的事实中推断出新的信息，例如 Ancestor(x, y) <- Parent(x, y)
• souffle-lang/souffle (Systematic, Ontological, Undiscovered Fact Finding Logic Engine)：由 Datalog 启发的一种编程语言，可用于静态分析、网络分析和数据分析。默认使用该引擎。

安装

首先按照项目 README 的建议，自己构建 souffle 而不是直接安装二进制包，记得添加环境变量。

The currently maintained version targets Soufflé, an open-source Datalog engine for program analysis (which is the default engine used). In order to install an up-to-date version of Soufflé, the best practice is to clone the development Github repo and follow the instructions found on this page. Doop is currently tested with Souffle versions 1.5.1, 2.0.2, and 2.1.

基本命令

./doop --help all 全部命令如下：

可以跑一下项目里 docs/doop-101-examples/Example.java 的例子，先把这个打包成 Example.java，然后开始分析

之后的内容就不介绍了，建议阅读这篇[博客](https://jckling.github.io/2021/12/17/Security/指针分析工具 Doop 使用指南/)，还有这篇，自己跑几个例子。因为真的要弄清楚各种规则，很花时间的。了解最重要的原理即可：

Doop 执行流程大致可以分为三步：

1. 使用 soot 生成 jimple 文件，使用 –generate-jimple 参数可以输出 jimple 文件，在 output//database/jimple 文件夹下
2. 将 jimple 文件转换为 datalog 引擎的输入事实（.facts）
3. 使用 souffle 引擎执行选定的分析，将关系输出为 .csv，即分析结果

Doop 分析字节码，被转换为名为 Jimple 的中间表示（Intermediate Representation, IR），实际分析的就是 jimple；因为字节码是基于堆栈的，但指针分析中需要变量/局部变量来分析指向，所以使用 Soot 将基于堆栈的字节码转换为具有局部变量的中间表示。下一步将 Jimple 中间表示转换为 .facts 文件（数据库表），然后由 Datalog 逻辑加载这些文件作为输入。Datalog 从输入开始推导事实，填充关系；一些关系使用 .output 标记输出，保存为 .csv 文件；当 Datalog 执行终止时，保存的 .csv 文件就是分析输出。

Z3

Z3 是微软研究领域最先进的定理证明器。它可以用来检查逻辑公式在一个或多个理论上的可满足性。Z3为软件分析及验证工具提供了一个引人注目的匹配, 因为几个常见的软件构造直接映射到支持的理论中。

• 安装教程和 GitHub：https://github.com/Z3Prover/z3

• 非常棒的 wiki：https://github.com/Z3Prover/z3/wiki

• 教程：https://github.com/Z3Prover/z3/tree/master/examples/python/tutorial/jupyter

• python binding 教程：https://github.com/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb

STP

GitHub：https://github.com/stp/stp

Doc：https://stp.readthedocs.io/en/latest/

一个把问题编码成 SAT 的求解器。安装之后遇到坑，请看 Issue，基本能够解决。python binding 的用法直接看 build 里 python 的源码即可，内容很少。

KLEE

C 语言的符号执行工具

GitHub：https://github.com/klee/klee/tree/master

主页和教程：http://klee.github.io/getting-started/

建议手动编译安装，多踩踩坑，熟悉工具链，这样才能熟悉基本流程。安装完之后按照官方的教程跑一跑就可以了。利用好主页的资源，邮件列表里别人的讨论和问题很实用。

总结

静态基本流程都是生成中间表示(IR)，简化源码或者操作码，中间还可能有静态单赋值或者 def-use 的优化。然后就分成两种方式了。

一种是直接是一些软件分析的算法，写死了，事先提供的。这样的算法会提供控制流、指针分析这些信息。另外一种是基于 Datalog，首先用 C++或者 python 等语言生成 facts，这些 facts 是程序的各种信息。然后再根据预定的 Datalog 逻辑还有选项，生成这个程序需要的 Datalog 代码，然后由 Datalog 引擎编译 Datalog 代码，生成 C++ 代码，然后开始执行各种程序分析算法。

前者的方式就像 slither 的 detector 规则，一般简单的情况就够用了，拓展性不好。后者的方式，是往往基于前者提取的信息，比如 slither 就只完成了第一步。后者可以具备可拓展性，可以自己添加额外的 datalog 代码，自定义一些分析。为什么用 datalog 呢，因为代码量会小很多，而且自己写 C++ 不一定有引擎生成的高效。

提高分析精度的方式，我看到有采用多种中间表示（IR）的，不同IR有一些侧重点，然后综合起来进行分析。