SynFuzz：通过分支条件合成实现高效混合符号执行
密码学与安全
2019-05-24 v1
摘要
混合符号执行（concolic execution）是一种以系统化方式探索执行路径的强大程序分析技术。与基于随机变异的模糊测试相比，混合符号执行尤其擅长探索由复杂且严苛的分支谓词（如 (a*b) == 0xdeadbeef）所守护的路径。然而其缺点是，混合符号执行引擎比原生执行慢得多。造成缓慢的一个主要根源是，混合符号执行引擎必须解释指令以维护程序变量的符号表达式。在本工作中，我们提出 SynFuzz，一种执行可扩展混合符号执行的新方法。SynFuzz 通过用动态污点分析和程序合成替代解释来实现这一目标。具体而言，为翻转一个条件分支，SynFuzz 首先使用操作感知的污点分析记录其分支谓词的部分表达式（即草图），然后利用预言引导的程序合成基于输入输出对重建符号表达式。最后一步与传统混合符号执行相同——SynFuzz 咨询 SMT 求解器以生成能够翻转目标分支的输入。通过这样做，SynFuzz 可以达到接近模糊执行的执行速度，同时保留混合符号执行翻转复杂分支谓词的能力。我们实现了 SynFuzz 的原型，并使用三组程序对其进行了评估：真实世界应用、LAVA-M 基准和 Google Fuzzer Test Suite (FTS)。评估结果表明，SynFuzz 比传统混合符号执行引擎可扩展性强得多，能在 LAVA-M 中发现比大多数最先进的混合符号执行引擎（QSYM）更多的漏洞，并在真实世界应用和 FTS 上取得更好的代码覆盖率。
引用
@article{arxiv.1905.09532,
title = {SynFuzz: Efficient Concolic Execution via Branch Condition Synthesis},
author = {Wookhyun Han and Md Lutfor Rahman and Yuxuan Chen and Chengyu Song and Byoungyoung Lee and Insik Shin},
journal= {arXiv preprint arXiv:1905.09532},
year = {2019}
}