CyberGlossary

应用安全

符号执行

别称: 符号分析, concolic 执行

定义

一种程序分析技术,使用符号输入而非具体值执行代码,通过 SMT 求解器求解路径约束以发现缺陷。

符号执行引擎将程序输入视为数学变量,并在每个条件分支处分裂路径进行探索。每条路径累积一组以一阶逻辑表达的约束,Z3 等 SMT 求解器据此判断约束是否可满足,如可满足,则产生一组能将程序导向该路径的具体输入。这使符号执行非常擅长证明缺陷条件(溢出、除零、污点到达汇点)的可达性,但容易遭遇路径爆炸与约束求解复杂度问题。KLEE、angr、Manticore 等工具常用于辅助 fuzzer、发现深层漏洞,以及验证二进制程序的安全属性。

示例

  • 对 C 语言库使用 KLEE,生成覆盖每个分支并触发 assert 的输入。
  • 将 angr 与 AFL++ 结合,解决单纯 fuzz 无法绕过的约束。

相关术语