SATSMTZ3和符号执行

Posted 白马负金羁

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了SATSMTZ3和符号执行相关的知识,希望对你有一定的参考价值。

符号执行(symbolic execution)是一种计算机科学领域的程序分析技术,通过采用抽象的符号代替精确值作为程序输入变量,得出每个路径抽象的输出结果。 这一技术在软件测试中有很重要的应用,能够有效地发现程序中的漏洞。本专栏中前面已经介绍过在angr中使用符号执行来解决CTF题目的例子。本文要更进一步地探讨其背后的一些知识。

 

一、SAT

SAT在计算理论中是非常重要的一个问题(参见【1】)。我们都知道布尔公式(Boolean formula)是包含布尔变量和运算的表达式。例如就是一个布尔公式。如果对变量的某个0、1赋值使得一个公式的值等于1,则该公式是可满足的(satisfiable)。上面的布尔公式是可满足的,因为当时,公式的计算结果就是1

以上是关于SATSMTZ3和符号执行的主要内容,如果未能解决你的问题,请参考以下文章

SATSMTZ3和符号执行

SATSMTZ3和符号执行

符号执行-基于python的二进制分析框架angr

[符号执行-入门1]软件测试中的符号执行

TFVC api:如何获取文件属性(“可执行文件”和“符号链接”)

Linux文件权限符号含义