dynaroars/dig
GitHub: dynaroars/dig
DIG 是一款数值型程序不变量自动生成工具，能从执行 trace 或 C 源码中推断非线性等式、不等式、同余关系等多种数值性质，用于程序验证与分析研究。
Stars: 55 | Forks: 7
# DIG
**DIG** 是一个 _不变量生成_ 工具，用于发现 _任意_ 程序位置的程序属性（例如，循环不变量、后置条件）。DIG 专注于 _数值型_ 不变量，目前支持以下数值关系：
- 任意变量之间的 *非线性/线性等式*，例如 `x+y=5`, `x*y=z`, `x*3y^3 + 2*zw + pq + q^3 = 3`
- *线性不等式*（例如，区间和八边形不变量），例如 `-4 <= x <= 7, -2 <= - x - y <= 10`
- *析取*：*min/max* 形式下的某些特定类型的析取，例如 `max(x,y) <= z + 2`，以及非线性形式，例如 `x^2 −xy −xz +yz =0` 即为 `(x −y)=0 v (x − z)=0`
- *同余*关系，例如 `x == 0 (mod 4), x+y == 1 (mod 5)`
- 数组间的 *嵌套关系*，例如 `A[i] = B[C[3*i+2]]`
- 用户还可以使用 *项* 来表示所需信息，例如 `t1 = 2^x, t2 = log(n)`，并让 DIG 推断这些项上的不变量。
DIG 的数值关系（特别是非线性关系）已被用于许多[研究项目](#page_with_curl-publications)，包括
- *程序理解和正确性/安全性检查* (`TSE21`, `ICSE12`, `ICSE14`, `ASE17`, `FSE17`, `TOSEM13`)
- 通过提供程序运行时间复杂度（如 `O(N^2)` 或 `O(NM)`）进行 *复杂度分析* (`ASE17`, `FSE17`)
- 用于复杂度分析的 *递归关系*（例如，为递归程序寻找递归关系，如 `T(n)=3*T(n/2) + f(n)`, (`SEAD20`, `OOPSLA21`)
- *终止和非终止分析*（使用非线性不变量来推断和推导用于终止的秩函数以及用于非终止的递归集，`OOPSLA20`）
- *数组分析*，在数组数据结构上寻找不变关系，如 `A[i] = B[C[2i + 3]]`, (`ICSE12`, `TOSEM13`)
- **基准测试**：DIG 项目还生成了一组大型的 **NLA** [基准测试程序](https://github.com/dynaroars/dig/tree/dev/benchmark)，其中包含非线性不变量。其中许多程序被用于一年一度的 SV-COMP（软件验证竞赛），例如 [`dig-nla`](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main/c/nla-digbench) 和 [`dig-nla-scaling`](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/tree/main/c/nla-digbench-scaling)。
### :exclamation: 快速信息
## 设置和使用 DIG
### 使用 Docker 进行设置（手动安装的详细信息，请参阅 [Dockerfile](./Dockerfile)）
### 用法
DIG 可以从[trace 文件](#generating-invariants-from-traces)（一个由分号分隔的纯文本 `csv` 文件，包含变量的具体值）或[程序](#generating-invariants-from-a-program)（C 语言文件 `.c`）生成不变量。
#### 从 Trace 生成不变量
#### 从程序生成不变量
#include
void vassume(int b){}
void vtrace1(int q, int r, int a, int b, int x, int y){}
void vtrace2(int q, int r, int a, int b, int x, int y){}
void vtrace3(int q, int r, int x, int y){}
int mainQ(int x, int y){
vassume(x >= 1 && y >= 1);
int q=0;
int r=x;
int a=0;
int b=0;
while(1) {
vtrace1(q, r, a, b, x, y);
if(!(r>=y))
break;
a=1;
b=y;
while (1){
vtrace2(q, r, a, b, x, y);
if(!(r >= 2*b))
break;
a = 2*a;
b = 2*b;
}
r=r-b;
q=q+a;
}
vtrace3(q, r,x, y);
return q;
}
void main(int argc, char **argv){
mainQ(atoi(argv[1]), atoi(argv[2]));
}
```
* 要在某个任意位置查找不变量，我们声明一个函数 `vtraceX`，其中 `X` 是某个不同的数字，并在该位置调用该函数。
* 例如，在 `cohendiv.c` 中，我们在外层和内层 while 循环的头部调用 `vtrace0`, `vtrace1` 来寻找循环不变量，并在函数退出前调用 `vtrace2` 来寻找后置条件。
* `vtraceX` 接受一个参数列表，这些参数是所需位置作用域内的变量。这告诉 DIG 在这些变量上寻找不变量。
* 我们现在对 `cohendiv.c` 运行 DIG，并在 `vtracesX` 位置发现以下不变量：
```
$ time ~/miniconda3/bin/python3 -O dig.py ../tests/cohendiv.c -log 3
settings:INFO:2021-10-29 13:51:11.038391: dig.py ../tests/cohendiv.c -log 3
alg:INFO:analyzing '../tests/cohendiv.c'
alg:INFO:got symbolic states at 4 locs in 4.21s
alg:INFO:got 69 ieqs in 1.11s
alg:INFO:got 377 minmax in 1.69s
alg:INFO:got 6 eqts in 5.50s
alg:INFO:check 452 invs using 680 traces (0.33s)
alg:INFO:simplify 452 invs (1.40s)
* prog cohendiv locs 4; invs 29 (Eqt: 5, MMP: 1, Oct: 23) V 6 T 3 D 2; NL 5 (2) ;
-> time eqts 5.5s, ieqs 1.1s, minmax 1.7s, simplify 1.8s, symbolic_states 4.2s, total 11.5s
rand seed 1635533471.04, test 62
tmpdir: /var/tmp/dig_92233634043151007_2nugp63w
vtrace0(2 invs):
1. -y <= -1
2. -x <= -1
vtrace1(12 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. -r <= 0
4. -a <= 0
5. -y <= -1
6. q - x <= 0
7. a - q <= 0
8. b - x <= 0
9. r - x <= 0
10. a - b <= 0
11. -q - r <= -1
12. min(q, y) - b <= 0
vtrace2(8 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. -q <= 0
4. -y <= -1
5. r - x <= 0
6. b - r <= 0
7. a - b <= 0
8. -b + y <= 0
vtrace3(7 invs):
1. q*y + r - x == 0
2. -q <= 0
3. -r <= 0
4. q - x <= 0
5. r - x <= 0
6. r - y <= -1
7. -r - x <= -1
```
`-noss` 选项禁用符号状态，从而使 DIG 表现为纯 *动态* 不变量生成工具。在这里，DIG 对随机输入运行程序，收集 trace，并推断不变量。它不使用符号状态，因此不需要符号执行工具，但可能会产生虚假结果。
```
$ time ~/miniconda3/bin/python3 -O dig.py ../tests/cohendiv.c -log 3 -noss -nrandinps 10
settings:INFO:2021-10-23 12:37:15.965808: dig.py ../tests/cohendiv.c -log 3 -noss -nrandinps 10
alg:INFO:analyzing '../tests/cohendiv.c'
alg:INFO:analyzing '../tests/cohendiv.c'
infer.eqt:WARNING:18 traces < 35 uks, reducing to deg 2
infer.eqt:WARNING:38 traces < 84 uks, reducing to deg 2
infer.eqt:WARNING:50 traces < 84 uks, reducing to deg 2
alg:INFO:testing 678 invs using 106 traces (0.30s)
alg:INFO:simplify 670 invs (3.26s)
vtrace1 (17 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. -a <= 0
4. -r <= 0
5. -y <= -9
6. a - b <= 0
7. a - q <= 0
8. r - x <= 0
9. q - x <= -6
10. b - x <= -2
11. -a - r <= -2
12. -x - y <= -16
13. min(q, r, x) - b <= 0
14. a + q === 0 (mod 2)
15. a - q === 0 (mod 2)
16. -a - q === 0 (mod 2)
17. -a + q === 0 (mod 2)
vtrace2 (17 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. -q <= 0
4. -y <= -9
5. r - x <= 0
6. b - r <= 0
7. -b + y <= 0
8. -r + y <= -2
9. -q - x <= -12
10. min(a, b, q) - y - 1 <= 0
11. b + 2 - max(a, q, r, y) <= 0
12. q === 0 (mod 2)
13. -q === 0 (mod 2)
14. r - x === 0 (mod 4)
15. r + x === 0 (mod 2)
16. -r + x === 0 (mod 4)
17. -r - x === 0 (mod 2)
vtrace3 (9 invs):
1. q*y + r - x == 0
2. -r <= 0
3. -q <= 0
4. -y <= -9
5. r - x <= 0
6. r - y <= -1
7. -q - x <= -6
8. -q - r <= -3
9. -x - y <= -16
```
#### 其他程序
* 目录 [`benchmark/c/nla`](./benchmark/c/nla) 包含许多具有非线性不变量的程序。
### :wrench: 调整 DIG
## :question: 常见问题解答
## :page_with_curl: 出版物
有关 DIG 及基于 DIG 构建的项目的技术信息可以从这些论文中找到。`tool` 论文 (`ICSE22`) 和 `Symbolic States` 论文 (`TSE21`) 可能是一个很好的起点。
1. ThanhVu Nguyen, KimHao Nguyen, and Hai Duong. [**SymInfer: Inferring Numerical Invariants using Symbolic States**](https://dynaroars.github.io/pubs/nguyen2022syminfer.pdf). International Conference on Software Engineering-Tool Demo (ICSE-Demo), pages 197--201, 2022
2. ThanhVu Nguyen, KimHao Nguyen, Matthew Dwyer. [**Using Symbolic States to Infer Numerical Invariants**](https://dynaroars.github.io/pubs/nguyen2021using.pdf). Transactions on Software Engineering (TSE), 2021
3. Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen. Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations, Proc. ACM Program. Lang. (OOPSLA), pages 1--23, 2021
4. Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, ThanhVu Nguyen. **DynamiTe: Dynamic Termination and Non-termination** Proofs. Proc. ACM Program. Lang. (OOPSLA), 2020
5. ThanhVu Nguyen, Didier Ishimwe, Alexey Malyshev, Timos Antonopoulos, and Quoc-Sang Phan. **Using Dynamically Inferred Invariants to Analyze Program Runtime Complexity**. Workshop on Software Security from Design to Deployment, 2020
6. ThanhVu Nguyen, Matthew Dwyer, and William Visser. **SymInfer: Inferring Program Invariants using Symbolic States**. In Automated Software Engineering (ASE). IEEE, 2017.
7. ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks. **A Counterexample-guided Approach to Finding Numerical Invariants**. In 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE), pages 605--615. ACM, 2017.
8. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. **DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants**. Transactions on Software Engineering Methodology (TOSEM), 23(4):30:1--3030, 2014.
9. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. **Using Dynamic Analysis to Generate Disjunctive Invariants**. In 36th International Conference on Software Engineering (ICSE), pages 608--619. IEEE, 2014.
10. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. **Using Dynamic Analysis to Discover Polynomial and Array Invariants**. In 34th International Conference on Software Engineering (ICSE), pages 683--693. IEEE, 2012. `Distinguish Paper Award`
## 致谢
* 本项目部分由 NSF 基金 CCF 1948536、CCF 2200621 和 ARO 基金 W911NF-19-1-0054 支持。同时也得到了来自 Facebook 和 Amazon Research Awards 的赞助支持。
详情
``` # 克隆 DIG $ git clone --depth 1 https://github.com/dynaroars/dig.git # 然后进入 DIG 的目录 $ cd dig # in DIG's directory # 构建 docker image，安装和构建所有内容需要一些时间 $ docker build . -t='dig' ... ... # 然后运行 dig $ docker run -it dig # docker 会将你带入如下所示的 Linux 提示符 $ root@b53e0bd86c11:/dig/src# # 现在你可以运行 DIG —— 你的机器的 CPUs/CORES 越多，DIG 运行得越快。 # 在 trace 文件上运行 DIG root@931ac8632c7f:/dig/src# time ~/miniconda3/bin/python3 -O dig.py ../examples/traces/cohendiv.csv -log 4 ... ... # 或者在 C 程序上运行 # 更快：将非线性 eqts 限制为 degree 2，但不生成 inequalities 或 minmax invariants，并且 root@931ac8632c7f:/dig/src# time ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4 # 如果你遇到 SARL expected version X but found Y 的错误，请编辑 ~/.sarl 并将 X 更改为 Y # 更慢：但提供所有内容 root@931ac8632c7f:/dig/src# time ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/cohendiv.c -log 4 ... # 要将 DIG 更新到来自 github 的最新版本，请在 Docker 中的主 DIG 目录中执行 git pull root@931ac8632c7f:/dig/src# git pull ... ... ```详情
DIG 可以直接从包含具体程序执行 trace 的 `csv` 文件中推断不变量，如下所示。 ``` # 在 DIG 的 src 目录中 $ less ../test/traces/cohendiv.csv vtrace1; I q; I r; I a; I b; I x; I y vtrace1; 4; 8; 1; 4; 24; 4 vtrace1; 16; 89; 1; 13; 297; 13 vtrace1; 8; 138; 4; 76; 290; 19 vtrace1; 0; 294; 8; 192; 294; 24 vtrace1; 64; 36; 4; 16; 292; 4 ... vtrace2; I x; I y; I q; I r vtrace2; 280; 24; 11; 16 vtrace2; 352; 11; 32; 0 vtrace2; 22; 298; 0; 22 vtrace2; 274; 275; 0; 274 vtrace2; 2; 287; 0; 2 ... ``` ``` # 在 DIG 的 src 目录中 tnguyen@origin ~/d/src (dev)> time ~/miniconda3/bin/python3 -O dig.py ../tests/traces/cohendiv.csv -log 3 (base) settings:INFO:2021-10-29 13:51:40.966898: dig.py ../tests/traces/cohendiv.csv -log 3 alg:INFO:analyzing '../tests/traces/cohendiv.csv' alg:INFO:check 546 invs using 181 traces (0.26s) alg:INFO:simplify 544 invs (2.35s) vtrace1(17 invs): 1. a*y - b == 0 2. q*y + r - x == 0 3. -q <= 0 4. -y <= -1 5. a - b <= 0 6. r - x <= 0 7. b - r <= 0 8. a - x <= -5 9. -b + y <= 0 10. -x + y <= -6 11. -q - r <= -8 12. -r - x <= -16 13. -x - y <= -10 14. a + 2 - max(q, r, y) <= 0 15. y + 2 - max(b, q, r, 0) <= 0 16. -q === 0 (mod 2) 17. -r - x === 0 (mod 2) vtrace2(8 invs): 1. q*y + r - x == 0 2. -q <= 0 3. -r <= 0 4. q - x <= 0 5. r - x <= 0 6. r - y <= -1 7. -q - r <= -1 8. -x - y <= -10 ``` *注意*：如果我们仅在 trace 上运行 Dig，那么我们可能会得到伪不等式，也就是说，它们在给定的 trace 下是正确的，但并不是真正的不变量。如果如下所示给出了程序的源代码，DIG 可以检查源代码并去除虚假结果。详情
考虑以下 `cohendiv.c` 程序 ``` // in DIG's src directory // $ less ../test/cohendiv.c #include详情
DIG 旨在实现完全自动化。然而，它也允许用户控制其行为（`src/settings.py` 列出了所有默认参数）。使用 `-h` 或 `--help` 查看可以传递给 DIG 的选项。下面我们展示几个有用的选项。 #### 指定等式的最大次数 默认情况下，DIG 会自动寻找具有较高次数（例如 `x^7`）的等式。这可能需要一些时间，因此我们可以使用选项 `-maxdeg X` 指定 DIG 搜索不超过最大次数 `X` 的等式。这将使 DIG 运行得更快（代价是无法找到次数高于 `X` 的等式）。 #### 禁用不变量 默认情况下，DIG 会搜索所有支持形式的不变量。然而，我们可以使用 `-noeqts`, `-noieqs` , `-nominmax`, `nocongruences` 关闭它们 ``` $ ~/miniconda3/bin/python3 -O dig.py ../tests/cohendiv.c -log 3 -maxdeg 2 -noieqs #find equalities up to degree 2 and do not infer inequalities ... ``` #### 自定义不等式 默认情况下，DIG 推断八边形不等式（即，系数在 `{-1,0,1}` 集合中的 `2` 个变量之间的线性不等式）。我们可以自定义 DIG 以寻找更具表达式的不等式（当然，代价是需要更多时间来生成更具表达力的不变量）。 下面我们用不同的示例 `Sqrt1.java` 来演示 ``` $ ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/sqrt1.c -nominmax -nocongruences # find default, octagonal, ieq's. ... 1. 2*a - t + 1 == 0 2. 4*s - t**2 - 2*t - 1 == 0 3. -a <= 0 4. a - n <= 0 5. -n + t <= 2 6. -s + t <= 0 $ ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/sqrt1.c -nominmax -nocongruences -ideg 2 # find nonlinear octagonal inequalities ... 1. 2*a - t + 1 == 0 2. 4*s - t**2 - 2*t - 1 == 0 3. -a <= 0 4. a - n <= 0 5. -s + t <= 0 6. -n + t <= 2 7. -s**2 + t**2 <= 0 $ ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/sqrt1.c -nominmax -nocongruences -icoefs 2 # find linear inequalities with coefs in {2,-1,0,1,2} ... 1. 2*a - t + 1 == 0 2. 4*s - t**2 - 2*t - 1 == 0 3. -a <= 0 4. a - n <= 0 5. -n + 2*t <= 6 6. -2*n + s <= 2 7. -2*s + 2*t <= 0 ```对研究有用的信息（例如，是什么让 DIG 与众不同？）
- DIG 将一个 C 程序作为输入。该程序必须是可编译的（即语法正确），并且标注了感兴趣的位置（你希望推断不变量的位置）。 - DIG 还可以将包含程序 trace 的 `csv` 文件作为输入，并且仅根据这些 trace 推断不变量（即纯动态）。 - Python、Sympy 和 Z3 SMT solver 用于推断不变量，以及符号执行工具 CIVL 用于从源代码检查不变量。Python、Sympy 和 Z3 可以使用 Miniconda 发行版的 Python 进行安装。CIVL 已随 DIG 发行版附带。 - 不，DIG 开箱即用，不需要用户输入。但是，如果你想调整 DIG 的行为，可以像[这里](#wrench-tweaking-dig)展示的那样操作。 - 此 DIG 工具支持 **数值型不变量**。这包括非线性和线性（仿射）属性。请参阅[这里](./EXAMPLES.md)的程序和示例。 - 请注意，许多[研究项目](#page_with_curl-publications)基于 DIG 支持其他种类的不变量（例如，用于终止和非终止分析的秩函数和递归集，或用于复杂度分析的递归关系）。这些项目有各自独立的研究原型工具。 - 了解 DIG 技术细节的一个好起点是我们的 [TSE'21](https://dynaroars.github.io/pubs/nguyen2021using.pdf) 论文。 - DIG 的主要目的是在所需位置发现尽可能强的不变量，*而不是*证明断言或后置条件，这是许多不变量工具的目标。 - 当然，如果发现的不变量比断言或后置条件更强，那么这些就被证明了。 - DIG 在任意位置推断不变量，因此不局限于例如归纳循环不变量。 - DIG 的输入是 _程序_，而不是像许多不变量工具那样表示状态转换的 SMT 公式。 - 检查是通过使用 _符号执行_ 提取 _符号状态_ ，并应用 Z3 SMT solver 对状态和候选不变量进行推理来完成的。 - DIG 的推算是动态的（大部分情况下），也就是说，DIG *是*一种数据驱动的方法。 - 某些部分，例如不等式，使用静态分析来分析符号状态。 - 不使用 ML（机器学习）进行推算（不是神经网络、分类器等）。 - DIG 遵循一种 _迭代猜测与检查方法_，即从 trace 推断候选不变量，检查并获取反例 trace 以改进推断，并重复此过程。 - 默认情况下，DIG 执行多种算法来寻找不同的不变量，其非线性等式不变量可能具有非常高的次数，所有这些都导致了巨大的搜索空间。要加速 DIG，你有几个选项。 - 使用多核计算机。DIG 利用多处理技术，在具有现代多核计算机上运行速度会显著提高。举个例子，我们的[实验室机器](https://github.com/dynaroars/dynaroars.github.io/wiki/Servers)有 64 核。当然你不需要那么多，但越多越好。 - 请注意，DIG 不利用 GPU 处理。 - 像[这里](#wrench-tweaking-dig)展示的那样调整其参数。例如，将次数减少到 `d` (`-maxdeg d`) 将告诉 DIG 不要搜索次数超过 `d` 的非线性不变量，或者如果你不感兴趣，可以禁用某些特定类型的不变量（例如，使用 `-nominmax` 来禁用 min/max 属性的计算）。引用 DIG 的 BibTeX 条目
- 关于符号状态和 DIG 的最新论文 (TSE'21) ``` @article{nguyen2021using, title={Using symbolic states to infer numerical invariants}, author={Nguyen, Thanhvu and Nguyen, KimHao and Dwyer, Matthew B}, journal={IEEE Transactions on Software Engineering}, volume={48}, number={10}, pages={3877--3899}, year={2021}, publisher={IEEE} } ``` - 关于推断非线性数值不变量的 DIG 最初论文 (ICSE'12) ``` @inproceedings{nguyen2012using, title={Using dynamic analysis to discover polynomial and array invariants}, author={Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie}, booktitle={2012 34th International Conference on Software Engineering (ICSE)}, pages={683--693}, year={2012}, organization={IEEE} } ```标签：不变量生成, 云安全监控, 可配置连接, 形式化验证, 程序分析, 请求拦截, 逆向工具, 静态分析