Symbolic execution 符号执行 Symbolic execution (King 1976) is another vulnerability discovery technique that is considered to be very promising. By symbolizing the program inputs, the symbolic execution

0x10 符号执行的定义 符号执行是软件测试行业新型的一个方向，当下较为火热，也给安全测试提供了新的思路，衍生出了诸多安全测试工具。维基百科中定义的符号执行如下 在计算机科学中，符号执行技术指的是通过程序分析的方法，确定哪些输入向量会对应导致程序的执行结果向量的方法。 抛开专业术语的表层，拨云见日，符号执行就是使用符号值代替真实值执行。在计算机程序中，尤其是C语言，符号是指函数名和变量

传统针对MT19937的逆向往往需要得到连续且完整的624个随机数，从而逆向出所有内部状态。但在实际场景中，想得到连续且完整的624个随机数是比较困难的，大部分情况下得到的是一些截断的数（例如得到连续的624个数，每个数是原始随机输出中的前16比特）。这种情况下，我们可以利用z3的符号执行推导部分内部状态，甚至可以推导一个“部分等价”的初始种子。本文针对python的random底层c库实现做了

1. 引言 程序静态分析（Program Static Analysis）是指在不运行代码的方式下，通过词法分析、语法分析、控制流、数据流分析等技术对程序代码进行扫描，验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术[8]。 程序静态分析的历史几乎与程序的历史一样长, 自从有了程序就有了程序分析。特别是随着编译技术的发展，大大带动了程序的自动分析技术。目前静态分析技术向模

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