SATSMTZ3和符号执行
Posted 白马负金羁
tags:
篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了SATSMTZ3和符号执行相关的知识,希望对你有一定的参考价值。
符号执行(symbolic execution)是一种计算机科学领域的程序分析技术,通过采用抽象的符号代替精确值作为程序输入变量,得出每个路径抽象的输出结果。 这一技术在软件测试中有很重要的应用,能够有效地发现程序中的漏洞。本专栏中前面已经介绍过在angr中使用符号执行来解决CTF题目的例子。本文要更进一步地探讨其背后的一些知识。
一、SAT
SAT在计算理论中是非常重要的一个问题(参见【1】)。我们都知道布尔公式(Boolean formula)是包含布尔变量和运算的表达式。例如就是一个布尔公式。如果对变量的某个0、1赋值使得一个公式的值等于1,则该公式是可满足的(satisfiable)。上面的布尔公式是可满足的,因为当,,时,公式的计算结果就是1
以上是关于SATSMTZ3和符号执行的主要内容,如果未能解决你的问题,请参考以下文章