diff --git a/SUMMARY.md b/SUMMARY.md index ac015ed..450b54c 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -78,7 +78,7 @@ GitHub 地址：https://github.com/firmianay/CTF-All-In-One * [3.5 Misc](doc/3.5_misc.md) * [3.6 Mobile](doc/3.6_mobile.md) * [四、技巧篇](doc/4_tips.md) - * 4.1 + * [4.1 Linux 内核调试](doc/4.1_linux_kernel_debug.md) * [4.2 Linux 命令行技巧](doc/4.2_Linux_terminal_tips.md) * [4.3 GCC 编译参数解析](doc/4.3_gcc_arg.md) * [4.4 GCC 堆栈保护技术](doc/4.4_gcc_sec.md) @@ -165,6 +165,7 @@ GitHub 地址：https://github.com/firmianay/CTF-All-In-One * Symbolic Execution * [8.2.1 All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask)](doc/8.2.1_dynamic_taint_analysis.md) * [8.2.2 Symbolic Execution for Software Testing: Three Decades Later](doc/8.2.2_symbolic_execution_for_software_testing.md) + * [8.2.3 AEG: Automatic Exploit Generation](doc/8.2.3_automatic_exploit_generation.md) * [Address Space Layout Randomization](doc/8.3_aslr_review.md) * [8.3.1 Address Space Layout Permutation (ASLP): Towards Fine-Grained Randomization of Commodity Software](doc/8.3.1_aslp.md) * Code Obfuscation diff --git a/doc/4.1_linux_kernel_debug.md b/doc/4.1_linux_kernel_debug.md new file mode 100644 index 0000000..59903be --- /dev/null +++ b/doc/4.1_linux_kernel_debug.md @@ -0,0 +1,104 @@ +# 4.1 Linux 内核调试 + +- [准备工作](#准备工作) + + +## 准备工作 +与用户态程序不同，为了进行内核调试，我们需要两台机器，一台调试，另一台被调试。在调试机上需要安装必要的调试器（如GDB），被调试机上运行着被调试的内核。 + +这里选择用 Ubuntu16.04 来展示，因为该发行版默认已经开启了内核调试支持： +``` +$ cat /boot/config-4.13.0-38-generic | grep GDB +# CONFIG_CFG80211_INTERNAL_REGDB is not set +CONFIG_SERIAL_KGDB_NMI=y +CONFIG_GDB_SCRIPTS=y +CONFIG_HAVE_ARCH_KGDB=y +CONFIG_KGDB=y +CONFIG_KGDB_SERIAL_CONSOLE=y +# CONFIG_KGDB_TESTS is not set +CONFIG_KGDB_LOW_LEVEL_TRAP=y +CONFIG_KGDB_KDB=y +``` + +#### 获取符号文件 +下面我们来准备调试需要的符号文件。看一下该版本的 code name： +``` +$ lsb_release -c +Codename: xenial +``` +然后在下面的目录下新建文件 `ddebs.list`，其内容如下（注意看情况修改Codename）： +``` +$ cat /etc/apt/sources.list.d/ddebs.list +deb http://ddebs.ubuntu.com/ xenial main restricted universe multiverse +deb http://ddebs.ubuntu.com/ xenial-security main restricted universe multiverse +deb http://ddebs.ubuntu.com/ xenial-updates main restricted universe multiverse +deb http://ddebs.ubuntu.com/ xenial-proposed main restricted universe multiverse +``` +`http://ddebs.ubuntu.com` 是 Ubuntu 的符号服务器。执行下面的命令添加密钥： +``` +$ wget -O - http://ddebs.ubuntu.com/dbgsym-release-key.asc | sudo apt-key add - +``` +然后就可以更新并下载符号文件了： +``` +$ sudo apt-get update +$ uname -r +4.13.0-38-generic +$ sudo apt-get install linux-image-4.13.0-38-generic-dbgsym +``` +完成后，符号文件将会放在下面的目录下： +``` +$ file /usr/lib/debug/boot/vmlinux-4.13.0-38-generic +/usr/lib/debug/boot/vmlinux-4.13.0-38-generic: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, BuildID[sha1]=f00f4b7ef0ab8fa738b6a9caee91b2cbe23fef97, not stripped +``` +可以看到这是一个静态链接的可执行文件，使用 gdb 即可进行调试，例如这样： +``` +$ gdb -q /usr/lib/debug/boot/vmlinux-4.13.0-38-generic +Reading symbols from /usr/lib/debug/boot/vmlinux-4.13.0-38-generic...done. +gdb-peda$ p init_uts_ns +$1 = { + kref = { + refcount = { + refs = { + counter = 0x2 + } + } + }, + name = { + sysname = "Linux", '\000' , + nodename = "(none)", '\000' , + release = "4.13.0-38-generic", '\000' , + version = "#43~16.04.1-Ubuntu SMP Wed Mar 14 17:48:43 UTC 2018", '\000' , + machine = "x86_64", '\000' , + domainname = "(none)", '\000' + }, + user_ns = 0xffffffff822517a0 , + ucounts = 0x0 , + ns = { + stashed = { + counter = 0x0 + }, + ops = 0xffffffff81e2cc80 , + inum = 0xeffffffe + } +} +``` + +#### 获取源文件 +将 `/etc/apt/sources.list` 里的 `deb-src` 行都取消掉注释： +``` +$ sed -i '/^#\sdeb-src /s/^#//' "/etc/apt/sources.list" +``` +然后就可以更新并获取 Linux 内核源文件了： +``` +$ sudo apt-get update +$ mkdir -p ~/kernel/source +$ cd ~/kernel/source +$ apt-get source $(dpkg-query '--showformat=${source:Package}=${source:Version}' --show linux-image-$(uname -r)) +``` +``` +$ ls linux-hwe-4.13.0/ +arch CREDITS debian.master firmware ipc lib net security tools zfs +block crypto Documentation fs Kbuild MAINTAINERS README snapcraft.yaml ubuntu +certs debian drivers include Kconfig Makefile samples sound usr +COPYING debian.hwe dropped.txt init kernel mm scripts spl +``` diff --git a/doc/4_tips.md b/doc/4_tips.md index 621a4e5..9c3e38a 100644 --- a/doc/4_tips.md +++ b/doc/4_tips.md @@ -1,6 +1,6 @@ # 第四章 技巧篇 -- 4.1 +- [4.1 Linux 内核调试](4.1_linux_kernel_debug.md) - [4.2 Linux 命令行技巧](4.2_Linux_terminal_tips.md) - [4.3 GCC 编译参数解析](4.3_gcc_arg.md) - [4.4 GCC 堆栈保护技术](4.4_gcc_sec.md) diff --git a/doc/5.2.1_pin.md b/doc/5.2.1_pin.md index 05bb86c..c3648cc 100644 --- a/doc/5.2.1_pin.md +++ b/doc/5.2.1_pin.md @@ -116,7 +116,7 @@ sci: ## Pin 简介 Pin 是 Intel 公司研发的一个动态二进制插桩框架，可以在二进制程序运行过程中插入各种函数，以监控程序每一步的执行。[官网](https://software.intel.com/en-us/articles/pin-a-dynamic-binary-instrumentation-tool)（目前有 2.x 和 3.x 两个版本，2.x 不能在 Linux 内核 4.x 及以上版本上运行，这里我们选择 3.x） -Pin 具有一下优点： +Pin 具有以下优点： - 易用 - 使用动态插桩，不需要源代码、不需要重新编译和链接。 - 可扩展 diff --git a/doc/5.3_symbolic_execution.md b/doc/5.3_symbolic_execution.md index 166aff5..85eaacf 100644 --- a/doc/5.3_symbolic_execution.md +++ b/doc/5.3_symbolic_execution.md @@ -1,22 +1,76 @@ # 5.3 符号执行 -- [符号执行的历史](#符号执行的历史) -- [什么是符号执行](#什么是符号执行) +- [基本原理](#基本原理) +- [参考资料](#参考资料) -## 符号执行的历史 - -![history-of-se](https://raw.githubusercontent.com/enzet/symbolic-execution/master/diagram/symbolic-execution.svg) - -或者进入[https://github.com/enzet/symbolic-execution](https://github.com/enzet/symbolic-execution)查看SVG大图。 - - -## 什么是符号执行 +## 基本原理 符号执行起初应用于基于源代码的安全检测中，它通过符号表达式来模拟程序的执行，将程序的输出表示成包含这些符号的逻辑或数学表达式，从而进行语义分析。 符号执行可分为过程内分析和过程间分析（或全局分析）。过程内分析是指只对单个函数的代码进行分析，过程间分析是指在当前函数入口点要考虑当前函数的调用信息和环境信息等。当符号执行用于代码漏洞静态检测时，更多的是进行程序全局的分析且更侧重代码的安全性相关的检测。将符号执行与约束求解器结合使用来产生测试用例是一个比较热门的研究方向。（关于约束求解我们会在另外的章节中详细讲解） 符号执行具有代价小、效率高的有点，但缺点也是很明显的。比如路径状态空间的爆炸问题，由于每一个条件分支语句都可能会使当前路径再分出一条新的路径，特别是遇到循环分支时，每增加一次循环都将增加一条新路径，因此这种增长是指数级的。在实践中，通常采用一些这种的办法来解决路径爆炸问题，比如规定每个过程内的分析路径的数目上限，或者设置时间上限和内存上限等来进行缓解。 -#### 动态符号执行 -动态符号执行将符号执行和具体执行结合起来，并交替使用静态分析和动态分析，在具体执行的同时堆执行到的指令进行符号化执行。 +**动态符号执行**将符号执行和具体执行结合起来，并交替使用静态分析和动态分析，在具体执行的同时堆执行到的指令进行符号化执行。 + +每一个符号执行的路径都是一个 true 和 false 组成的序列，其中第 i 个 true（或false）表示在该路径的执行中遇到的第 i 个条件语句。一个程序所有的执行路径可以用执行树（Execution Tree）表示。举一个例子： +```c +int twice(int v) { + return 2*v; +} + +void testme(int x, int y) { + z = twice(y); + if (z == x) { + if (x > y+10) { + ERROR; + } + } +} + +int main() { + x = sym_input(); + y = sym_input(); + testme(x, y); + return 0; +} +``` +这段代码的执行树如下图所示，图中的三条路径分别可以被输入 {x = 0, y = 1}、{x = 2, y = 1} 和 {x = 30, y = 15} 触发： + +![](../pic/5.3_tree.png) + +符号执行中维护了符号状态 σ 和符号路径约束 PC，其中 σ 表示变量到符号表达式的映射，PC 是符号表示的不含量词的一阶表达式。在符号执行的初始化阶段，σ 被初始化为空映射，而 PC 被初始化为 true，并随着符号执行的过程不断变化。在对程序的某一路径分支进行符号执行的终点，把 PC 输入约束求解器以获得求解。如果程序把生成的具体值作为输入执行，它将会和符号执行运行在同一路径，并且以同一种方式结束。 + +例如上面的程序中 σ 和 PC 变化过程如下： +``` +开始： σ = NULL PC = true +第6行： σ = x->x0, y->y0, z->2y0 PC = true +遇到if(e)then{}else{}：σ = x->x0, y->y0 then分支：PC = PC∧σ(e) else分支：PC' = PC∧¬σ(e) +``` + +于是我们发现，在符号执行中，对于分析过程所遇到的程序中带有条件的控制转移语句，可以利用变量的符号表达式将控制转移语句中的条件转化为对符号取值的约束，通过分析约束是否满足来判断程序的某条路径是否可行。这样的过程也叫作路径的可行性分析，它是符号执行的关键部分，我们常常将符号取值约束的求解问题转化为一阶逻辑的可满足性问题，从而使用可满足性模理论（SMT）求解器对约束进行求解。 + +#### 检测程序漏洞 +程序中变量的取值可以被表示为符号值和常量组成的计算表达式，而一些程序漏洞可以表现为某些相关变量的取值不满足相应的约束，这时通过判断表示变量取值的表达式是否可以满足相应的约束，就可以判断程序是否存在相应的漏洞。 + +使用符号执行检测程序漏洞的原理如下图所示： + +![](../pic/5.3_overview.png) + +举个数组越界的例子： +```c +int a[10]; +scanf("%d", &i); +if (i > 0) { + if (i > 10) + i = i % 10; + a[i] = 1; +} +``` +首先，将表示程序输入的变量 i 用符号 x 表示其取值，通过分别对 if 条件语句的两条分支进行分析，可以发现在赋值语句 a[i] = 1 处，当 x 的取值大于 0、小于 10 时，变量 i 的取值为 x，当 x 的取值大于 10 时，变量 i 的取值为 x % 10。通过分析约束 `(x>10∨x<10)∧(010∨x%10<10)∧x>10` 的可满足性，可以发现漏洞的约束是不可满足的，于是认为漏洞不存在。 + +#### 构造测试用例 + + +## 参考资料 +- [History of symbolic execution](https://github.com/enzet/symbolic-execution) diff --git a/doc/8.2.2_symbolic_execution_for_software_testing.md b/doc/8.2.2_symbolic_execution_for_software_testing.md index c34da8e..eaf8b16 100644 --- a/doc/8.2.2_symbolic_execution_for_software_testing.md +++ b/doc/8.2.2_symbolic_execution_for_software_testing.md @@ -1 +1,72 @@ # 8.2.2 Symbolic Execution for Software Testing: Three Decades Later + + +## 简介 +近几年符号执行因其在生成高覆盖率的测试用例和发现复杂软件漏洞的有效性再次受人关注。这篇文章对现代符号执行技术进行了概述，讨论了这些技术在路径探索，约束求解和内存建模方面面临的主要挑战，并讨论了几个主要从作者自己的工作中获得的解决方案。 + +这算是一篇很经典很重要的论文了。 + + +## 传统符号执行 +符号执行的关键是使用符号值替代具体的值作为输入，并将程序变量的值表示为符号输入值的符号表达式。其结果是程序计算的输出值被表示为符号输入值的函数。一个符号执行的路径就是一个 true 和 false 组成的序列，其中第 i 个 true（或false）表示在该路径的执行中遇到的第 i 个条件语句，并且走的是 then（或else） 这个分支。一个程序所有的执行路径可以用执行树（Execution Tree）来表示。举一个例子： + +![](../pic/8.2.2_tree.png) + +函数 testme() 有 3 条执行路径，组成右边的执行树。只需要针对路径给出输入，即可遍历这 3 条路径，例如：{x = 0, y = 1}、{x = 2, y = 1} 和 {x = 30, y = 15}。符号执行的目标就是去生成这样的输入集合，在给定的时间内遍历所有的路径。 + +符号执行维护了符号状态 σ 和符号路径约束 PC，其中 σ 表示变量到符号表达式的映射，PC 是符号表示的不含量词的一阶表达式。在符号执行的初始化阶段，σ 被初始化为空映射，而 PC 被初始化为 true，并随着符号执行的过程不断变化。在对程序的某一路径分支进行符号执行的终点，把 PC 输入约束求解器以获得求解。如果程序把生成的具体值作为输入执行，它将会和符号执行运行在同一路径，并且以同一种方式结束。 + +例如上面的例子。符号执行开始时，符号状态 σ 为空，符号路径约束 PC 为 true。每当遇到输入语句 var = sym_input() 时，符号执行就会在符号状态 σ 中加入一个映射 var->s，这里的 s 是一个新的未约束的符号值，于是程序的前两行得到结果 σ = {x->x0, y->y0}。当遇到一个赋值语句 v = e 时，符号执行就会在符号状态 σ 中加入一个 v 到 σ(e) 的映射，于是程序执行完第 6 行后得到 σ = {x->x0, y->y0, z->2y0}。 + +当每次遇到条件语句 if(e) S1 else S2 时，PC 会被更新为 PC∧σ(e)，表示 then 分支，同时生成一个新的路径约束 PC'，初始化为 PC∧¬σ(e)，表示 else 分支。如果 PC 是可满足的，那么程序会走 then 分支（σ 和 PC），否则如果 PC' 是可满足的，那么程序会走 else 分支（σ 和 PC'）。值得注意的是，符号执行不同于实际执行，其实两条路都是可以走的，分别维护它们的状态就好了。如果 PC 和 PC' 都不能满足，那么符号执行就在对应的路径终止。例如，第 7 行建立了符号执行实例，路径约束分别是 x0 = 2y0 和 x0 ≠ 2y0，在第 8 行又建立了两个实例，分别是 (x0 = 2y0)∧(x0 > y0 + 10) 和 (x0 = 2y0)∧(x0 ≤ y0 + 10)。 + +如果符号执行遇到了 exit 语句或者 error，当前实例会终止，并利用约束求解器对当前路径约束求出一个可满足的值，这个值就构成了测试输入：如果程序输入了这些实际的值，就会在同样的路径结束。例如上图中三个绿色块里的值。 + +如果符号执行的代码包含循环或递归，且它们的终止条件是符号化的，那么可能就会导致产生无数条路径。举个例子： + +![](../pic/8.2.2_loop.png) + +这段程序的执行路径有两种：一种是无数的 true 加上一个 false，另一种是无数的 false。第一种的符号路径约束如下： + +![](../pic/8.2.2_constraint.png) + +其中每个 Ni 都是一个新的符号值，执行结束的符号状态为 {N->Nn+1, sum->Σi∈[1,n]Ni}。在实践中我们需要通过一些方法限制这样的搜索。 + +传统符号执行的一个关键的缺点是，当符号路径约束包含了不能由约束求解器求解的公式时，就不能生成输入值。例如把上面的 twice 函数替换成下面的： + +![](../pic/8.2.2_twice.png) + +那么符号执行会得到路径约束 x0 ≠ (y0y0)mod50 和 x0 = (y0y0)mod50。更严格一点，如果我们不知道 twice 的源码，符号执行将得到路径约束 x0 ≠ twice(y0) 和 x0 = twice(y0)。在这两种情况下，符号执行都不能生成输入值。 + + +## 现代符号执行 +现代符号执行的标志和最大的优势是将实际执行和符号执行结合了起来。 + +#### Concolic Testing +Directed Automated Random Testing(DART) 在程序执行中使用了具体值，动态地执行符号执行。Concolic 执行维护一个实际状态和一个符号状态：实际状态将所有变量映射到实际值，符号状态只映射那些有非实际值的变量。Concolic 执行首先使用一些给定的或者随机的输入作为开始，收集执行过程中的条件语句对输入的符号约束，然后使用约束求解器推测输入的变化，从而引导下一次的程序执行到另一条路径。这个过程会不断地重复，直至探索完所有的执行路径，或者满足了用户定义的覆盖范围，又或者超出了预计的时间开销。 + +还是上面那个例子。Concolic 执行会生成一些随机输入，例如 {x = 22, y = 7}，然后对程序同时进行实际执行和符号执行。这个实际执行会到达第 7 行的 else 分支，同时符号执行会为该实际执行路径生成路径约束 x ≠ 2y0。然后 Concolic 执行会将路径约束的连接词取反，求解 x0 = 2y0 得到测试输入 {x = 2, y = 1}，这个新的输入将会让程序沿着另一条执行路径运行。然后 Concolic 执行在这个新的测试输入上，重复实际执行和符号执行的过程，此时将到达第 7 行的 then 分支和第 8 行的 else 分支，生成路径约束 (x0 = 2y0)∧(x0 ≤ y0 + 10)，从而生成新的测试输入让程序执行没有被执行过的路径。通过对将结合项 (x0 ≤ y0 + 10) 取反得到的约束 (x0 = 2y0)∧(x0 > y0 + 10) 进行求解，得到测试输入 {x = 30, y = 15}，然后程序到达了 ERROR 语句。这样程序的所有 3 条路径就都探索完了，其使用的策略是深度优先搜索。 + +#### Execution-Generated Testing(EGT) +EGT 是由 EXE 和 KLEE 实现和扩展的现代符号执行方法，它将程序的实际状态和符号状态进行了区分。EGT 在每次执行前会动态地检查所涉及的值是不是都是实际的值，如果是，则程序按照原样执行，否则，如果至少有一个值是符号值，程序会通过更新当前路径的条件符号化地执行。例如上面的例子，把 17 行的 y = sym_input() 改成 y = 10，那么第 6 行就会用实参 20 去调用 twice 函数，就像原程序那样执行。然后第 7 行将变成 if(20 == x)，符号执行会通过添加约束 x = 20，走 then 分支，同时添加约束 x ≠ 20，走 else 分支。而在 then 分支上，第 8 行变成了 if(x > 20)，不会到达 ERROR。 + +于是，传统符号执行中，因为外部函数或者无法进行约束求解造成的问题通过使用实际值得到了解决。但同时因为在执行中使用了实际值，固定了某些执行路径，由此将造成路径完成性的缺失。 + + +## 关键的挑战和解决方案 +#### 路径爆炸 +在时间和资源有限的情况下，符号执行应该对最相关的路径进行探索，主要有两种方法：启发式地优先探索最值得探索的路径，并使用合理的程序分析技术来降低路径探索的复杂性。 + +启发式搜索是用于确定路径搜索优先级的关键机制。大多数的启发式方法都专注于获得较高的语句和分支的覆盖率。一种有限的方法是使用静态控制流图来知道探索，尽量选择与未覆盖指令最接近的路径。另一种启发式方法是随机探索，即在两边都可行的符号化分支处随机选择一边。最近提出的一种方法是将符号执行与进化搜索相结合，其 fitness function 用于指导输入空间的搜索。 + +利用程序分析和软件验证的思想，以合理的方式减少路径探索的复杂性。一种简单的方法是使用 selelct 表达式进行静态融合，然后将其直接传递给约束求解器。这种方法在很多情况下都很管用，但实际上是将路径选择的复杂性传递给了约束求解器。还有一种方法是通过缓存和重用底层函数的计算结果，减小分析的复杂性。 + +#### 约束求解 +虽然近几年约束求解器的能力有明显提升，但依然是符号执行的关键瓶颈之一。因此，实现约束求解器的优化十分重要，这里讲两种方法：不相关约束消除和增量求解。 + +通常一个程序分支只依赖于一小部分的程序变量，因此一种有效的优化是从当前路径条件中移除与识别当前分支不相关的约束。例如，当前路径的条件是：(x + y > 10)∧(z > 0)∧(y < 12)∧(z - x = 0)，我们想通过求解 (x + y > 10)∧(z > 0)∧¬(y < 12)，其中 ¬(y < 12) 是取反的条件分支，那么我们就可以去掉对 z 的约束，因为其对 ¬(y < 12) 分支不会造成影响。减小后的约束会产生新的 x 和 y，我们用当前执行产生的 z 就可以产生新的输入了。 + +符号执行生成的约束集有一个重要的特征，就是它们被表示为程序源代码中的静态分支的固定集合。所以，多个路径可能会产生相似的约束集，所以可以使用相似的解决方案。通过重用以前相似请求得到的结果，可以提升约束求解的速度，这种方法被运用到了 CUTE 和 KLEE 中。在 KLEE 中，所有的请求结果都保存在缓存里，该缓存将约束集映射到实际的变量赋值。例如，在缓存中有这样一个映射：(x + y < 10)∧(x > 5) => {x = 6, y = 3}。利用这些映射，KLEE 可以迅速地解决一些相似的请求，例如请求 (x + y < 10)∧(x > 5)∧(y ≥ 0)，KLEE 可以迅速检查得到 {x = 6, y = 3} 是可行的。 + +#### 内存建模 +程序语句翻译为符号约束的精确性对符号执行的覆盖率有很大的影响。 diff --git a/doc/8.2.3_automatic_exploit_generation.md b/doc/8.2.3_automatic_exploit_generation.md new file mode 100644 index 0000000..9899901 --- /dev/null +++ b/doc/8.2.3_automatic_exploit_generation.md @@ -0,0 +1 @@ +# 8.2.3 AEG: Automatic Exploit Generation diff --git a/doc/8_academic.md b/doc/8_academic.md index d243381..7a73f19 100644 --- a/doc/8_academic.md +++ b/doc/8_academic.md @@ -13,6 +13,7 @@ * Symbolic Execution * [8.2.1 All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask)](8.2.1_dynamic_taint_analysis.md) * [8.2.2 Symbolic Execution for Software Testing: Three Decades Later](8.2.2_symbolic_execution_for_software_testing.md) + * [8.2.3 AEG: Automatic Exploit Generation](8.2.3_automatic_exploit_generation.md) * [Address Space Layout Randomization](8.3_aslr_review.md) * [8.3.1 Address Space Layout Permutation (ASLP): Towards Fine-Grained Randomization of Commodity Software](8.3.1_aslp.md) * Code Obfuscation diff --git a/pic/5.3_overview.png b/pic/5.3_overview.png new file mode 100644 index 0000000..07e696c Binary files /dev/null and b/pic/5.3_overview.png differ diff --git a/pic/5.3_tree.png b/pic/5.3_tree.png new file mode 100644 index 0000000..e5d7a9a Binary files /dev/null and b/pic/5.3_tree.png differ diff --git a/pic/8.2.2_constraint.png b/pic/8.2.2_constraint.png new file mode 100644 index 0000000..c1dcd54 Binary files /dev/null and b/pic/8.2.2_constraint.png differ diff --git a/pic/8.2.2_loop.png b/pic/8.2.2_loop.png new file mode 100644 index 0000000..7b7b67a Binary files /dev/null and b/pic/8.2.2_loop.png differ diff --git a/pic/8.2.2_tree.png b/pic/8.2.2_tree.png new file mode 100644 index 0000000..dd3452e Binary files /dev/null and b/pic/8.2.2_tree.png differ diff --git a/pic/8.2.2_twice.png b/pic/8.2.2_twice.png new file mode 100644 index 0000000..6adc216 Binary files /dev/null and b/pic/8.2.2_twice.png differ diff --git a/src/Others/5.3_symbolic_execution/tree.gv b/src/Others/5.3_symbolic_execution/tree.gv new file mode 100644 index 0000000..4329a72 --- /dev/null +++ b/src/Others/5.3_symbolic_execution/tree.gv @@ -0,0 +1,16 @@ +digraph { + 0 [shape="none", label=""]; + 1 [shape="diamond", label="2*y == x"]; + 2 [shape="box", label="x = 0\ny = 1"]; + 3 [shape="diamond", label="x > y+10"]; + 4 [shape="box", label="x = 2\ny = 1"]; + 5 [shape="box", label="x = 30\ny = 15"]; + 6 [shape="plaintext", label="ERROR"]; + + 0 -> 1; + 1 -> 2 [label="false"]; + 1 -> 3 [label="true"]; + 3 -> 4 [label="false"]; + 3 -> 5 [label="true"]; + 5 -> 6; +} \ No newline at end of file