前言

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

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

Java

java 基本语法与 C++ 类似，不熟悉的读者可以参考教程学习：https://www.liaoxuefeng.com/wiki/1252599548343744 ，如果有编程基础，入门很快的。

Soot

以下引用内容来自 星雪亭的《Soot 使用笔记》，我对里面不太准确的内容进行了调整和改正。

1、soot 简介

Soot 是 McGill 大学的 Sable 研究小组自 1996 年开始开发的 Java 字节码分析工具，它提供了多种字节码分析和变换功能，通过它可以进行过程内和过程间的分析优化，以及程序流图的生成，还能通过图形化的方式输出，让用户对程序有个直观的了解。尤其是做单元测试的时候，可以很方便的通过这个生成控制流图然后进行测试用例的覆盖，显著提高效率。

soot 项目在 github 上的地址为：https://github.com/Sable/soot

soot 是 java 优化框架，提供 4 种中间代码来分析和转换字节码。

• Baf：精简的字节码表示，操作简单
• Jimple：适用于优化的 3-address 中间表示
• Shimple：Jimple 的 SSA 变体
• Grimple：适用于反编译和代码检查的 Jimple 汇总版本。

soot 提供的输入和输出格式

输入格式

• java
• android 字节码
• Jasmin，低级中间表示
• soot 提供的分析功能
• class(Java8 以后)

输出格式

• Java 字节码
• android 字节码
• Jimple
• Jasmin
• shimple
• baf
• grimple
• xml
• class
• dava
• template
• jar 文件

soot 提供的分析功能

• 调用图构造
• 指针分析
• Def/use chains
• 模块驱动的程序内数据流分析
• 结合 FlowDroid 的污染分析

2.soot 的安装

目前来说，要使用 soot 有三种途径，分别是命令行、程序内以及 Eclipse 插件（不推荐）

2.1、命令行

可以在这里下载最新的 soot jar 包，我下载的是 4.1.0 版本中的 sootclasses-trunk-jar-with-dependencies.jar 包，这个包应该自带了 soot 所需要的所有依赖。下载：

1	curl -O https://soot-build.cs.uni-paderborn.de/public/origin/master/soot/soot-master/4.1.0/build/sootclasses-trunk-jar-with-dependencies.jar

输入以下命令：

1	java -cp sootclasses-trunk-jar-with-dependencies.jar soot.Main

可以看到：

再输入

1	java -cp sootclasses-trunk-jar-with-dependencies.jar soot.Main -h

可以看到有关 soot 的各种帮助信息。

2.2、程序内使用 soot

从 github 上 soot 项目的简介可知，soot 一般配合 maven 来进行部署,相关的依赖添加语句如下：

1 2 3 4 5 6 7

<dependencies> <dependency> <groupId>ca.mcgill.sable</groupId> <artifactId>soot</artifactId> <version>4.1.0</version> </dependency> </dependencies>

因为目前我的目的只是简单的使用 soot，所以对于程序中 soot 的使用在后面学习了相关 api 再来更新。

3.命令行中 soot 的使用

我的目标是将 java 转化为 Jimple 以发现程序编译中的问题和规律。因此本文的重点就在这里，我先在 soot.jar 所在的文件夹下新建了一个 java 文件 HelloWorld.java 如下图所示：

1 2 3 4 5 6

//HelloWorld.java public class HelloWorld { public static void main(String[] args) { System.out.println("hello"); } }

因为我使用的 Java 版本是 JDK1.8，根据 soot 提示，默认输入是 class 文件，所以我先用 javac 命令将 HelloWorld.java 编译为 HelloWorld.class。

1	javac HelloWorld.java

下面我们尝试将上面得到的 class 文件作为输入传给 soot.

1	java -cp sootclasses-trunk-jar-with-dependencies.jar soot.Main -pp -cp . HelloWorld

得到的结果没有报错，但是也无事发生，这是因为 soot 需要通过-f 属性指定输出的类型，这里我们将输出类型指定为 Jimple，查询文档之后得知要添加-f J 以确定输出格式，最终的语句如下：

1	java -cp sootclasses-trunk-jar-with-dependencies.jar soot.Main -f J -pp -cp . HelloWorld

该命令在 jar 文件所在目录下生成了一个 sootOutput 文件夹，里面有一个 HelloWorld.jimple 文件，使用 Idea 编辑器打开这个文件，得到的内容如下，这就是一个最基本的 HelloWorld.java 文件所形成的 jimple 码。

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

public class HelloWorld extends java.lang.Object { public void <init>() { HelloWorld r0; r0 := @this; specialinvoke r0.<init>(); return; } public static void main(java.lang.String[]) { java.io.PrintStream $r0; java.lang.String[] r1; r1 := @parameter0; $r0 = java.lang.System.out; $r0.println("hello"); return; } }

3.soot 命令行相关参数设置

soot/wiki里的命令表格写的十分清楚和明确，这里我就直接搬运过来，方便以后查阅。

二、Soot 生成控制流图

如果是将 Soot 当作简单工具来分析的人，可以直接使用 Soot 自带的工具 soot.tools.CFGViewer 分析类中的每个方法的控制流并生成 DOT 语言描述的控制流图，然后用 graphviz 中的 dot 命令来转换成可视化图形格式如.PNG

1、使用 soot.tools.CFGViewer 来生成 Triangle.class 的控制流图

新建文件 Test.java

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20

public class Test { private double num = 5.0; public double cal(int num, String type){ double temp=0; if(type == "sum"){ for(int i = 0; i <= num; i++){ temp =temp + i; } } else if(type == "average"){ for(int i = 0; i <= num; i++){ temp = temp + i; } temp = temp / (num -1); }else{ System.out.println("Please enter the right type(sum or average)"); } return temp; } }

然后编译和运行

1	javac Test.java && java -cp sootclasses-trunk-jar-with-dependencies.jar soot.tools.CFGViewer -pp -cp . Test

生成了 Test.dot 文件

1	dot -Tpng -o Test.png sootOutput/Test\ double\ cal\(int,java.lang.String\).dot

生成了 png 文件。

关于 Soot 的详细说明，可以看Jckling’s Blog 的《Soot 使用记录》和《利用 Soot 对 APK 插桩实践》

Doop

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

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

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

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

介绍

Doop is a declarative framework for static analysis of Java programs, centered on pointer analysis algorithms. Doop provides a large variety of analyses and also the surrounding scaffolding to run an analysis end-to-end (fact generation, processing, statistics, etc.).

The declarative nature of Doop stems from its use of Datalog (more specifically, LogiQL, a Datalog dialect developed by LogicBlox) to specify an analysis.

The building blocks of Datalog programs come in the form of predicates. Our input facts (a.k.a. EDB logic) are represented as predicate values, e.g., Person("John") or Parent("John", "Johnny jr").

Then we have rules (a.k.a. IDB logic) to infer new information from facts already known to be true. This continues until no new information can be extracted.

如果读者不熟悉以上概念，可以翻之前的 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，然后开始分析，分析的时间非常长，WSL 虚拟机 Ubuntu 跑了 40 分钟，都没有结果。

之后的内容就不介绍了，建议阅读这篇博客，还有这篇，自己跑几个例子。因为真的要弄清楚各种规则，很花时间的。了解最重要的原理即可：

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

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

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

来自：博客

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 API (also available in pydoc format)
• python binding 教程：https://github.com/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb

由于时间限制，就不详细介绍 API 了，读者有需求或者感兴趣，可以自己读文档。以后有需要我在学习如何应用到实际科研场景。

STP

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

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

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

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

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

后续有时间会基于它，完成一些作业。

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 有一些侧重点，然后综合起来。

读者如果感兴趣，不妨自己学习理论知识，然后折腾玩一玩。如果遇到困难，不妨在博客下方留言。