SATSMTZ3和符号执行

Posted 2021-08-24 白马负金羁

符号执行（symbolic execution）是一种计算机科学领域的程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。 这一技术在软件测试中有很重要的应用，能够有效地发现程序中的漏洞。本专栏中前面已经介绍过在angr中使用符号执行来解决CTF题目的例子。本文将通过几个例子来演示一下symbolic execution（或者SMT solver）在软件分析领域的应用。

一、程序等价性检验（Program Equivalence Checking）

这是《深入理解计算机系统》（参见【1】）中给出的一个问题。有一段计算机程序，在使用之前定义好的宏变量M和N后被编译成了二进制代码。由于编译器对程序中的乘法和除法运算做了一些优化，当把二进制代码反编译回C代码之后，对比两份源码，其实很难看出来它们是等价的（尽管它们确实是等价的）。现在的问题是，想求出：M和N的值到底是多少？

注意我们这里不会使用《深入理解计算机系统》中的分析方法（那个相当于是手工分析）。现在我们希望使用SMT solver来解决这个问题。

#!/usr/bin/env python3
from z3