Symbolic Execution Optimization
Symbolic Execution Optimization
符号执行过程:
获取字节码和源文件
反汇编
控制流图
符号执行
z3 求解器求解
检测漏洞符号执行包括两个重要模块, 分别是测试用例选择和路径约束条件求解, 前者关系到能否发现漏洞、测试覆盖率和测试代码深度, 后者用于产生测试用例, 大量的约束条件求解极大影响了符号执行性能
符号执行面临的三大难点：路径爆炸问题、符号执行精确性问题和复杂符号约束求解优化问题
Solutions
两种思路:
思路一: 通过某些方法或技术直接对符号执行本身、某个步骤进行改进
思路二: 通过和其他技术结合，相互弥补缺点，最终达到比较好的结果
思路三: 结合要检测的东西(即：智能合约)的特点，对符号执行进行特定的改进
思路一
路径爆炸(Path Explosion)/路径搜索(覆盖)
描述
所谓路径爆炸问题是指符号执行很难遍历程序的所有执行路径(特别是遇到循环分支时)，产生这个问题主要有两个方面的原因：
- 随着程序规模的增大，程序的可行路径呈现指数级增长；
- 符号执行在遍历每条路径的时候都需要大量的计算资源。
在有限的测试时间和金钱的条件下，符号执行不可能完成对所有的可行路径进行遍历。而在有效的计算资源条件下，如何设计一个有效的路径搜索策略就成了减轻路径爆炸问题的关键。
解决
主要有 2 个方面研究:
搜索约束
搜索约束即对程序的输入进行建模，或以目标位置为导向排除无关路径。这类方法是通过约束对搜索路径进行裁剪，从而达到降低复杂度的目的。
搜索约束面向特定类型/结构时，例如：对循环可达上界进行约束等
搜索约束面向特定类型的程序或者目标时，能够大幅地裁剪路径，例如基于文档辅助对输入建模，该方法从帮助文档、代码注释及文件格式中提取更多的搜索约束，帮助手册格式（manual）的参数约束以及特殊的文件格式，如可执行和可链接格式（ELF, executable and linking format）。
然而该方法也很有局限性，比如需要程序带有帮助手册，同时符合解析的规范。如果一个程序缺少必要信息，比如缺少帮助文档，则无法使用该方法。所以该方法很难适用于所有的开源程序，尤其是一些缺乏维护的开源程序。
-
本文提出了一种新的基于输入约束的符号执行（ICBSE，input constraint basedsymbolic execution）优化框架 通过提取代码中有效的命令行约束参数（比如 rm 命令中的-r 选项），从而实现对搜索路径的裁剪。
见论文第二页
-
这个比较基础看看题目就好 提出特定目标制导与循环可达上界制导相结合的符号执行制导技术
搜索策略
符号执行中的通用搜索策略希望在有限资源内覆盖更多的程序语句或路径，包括深度优先搜索（depth-first search，DFS）、随机状态搜索（random state search，RSS）、随机路径搜索（random path search，RPS）以及覆盖率优化搜索（coverage-optimized search，COS）等； 也有一些工作针对某个具体目标研究高效的路径空间搜索策略，包括提高程序语句覆盖率、面向可达性的搜索策略[、面向程序不同版本差异的搜索策略等.
搜索策略的改进和一些剪枝与优化
规定每个过程内的分析路径的数目上限、设置时间上限和内存上限等来进行缓解。 各种路径制导技术、路径剪枝、循环优化等方面的工作. 现有的制导技术以及路径剪枝分别关注于提出新的路径分支选择策略或者修剪探索过的路径
-
本文首先优化了动态执行引擎 Angr 的路径搜索算法。通过对 Angr 源码的深入分析,提出了优化其路径选择策略的思想 提出了两种并行分段式路径搜索算法:分割式并行化算法和基于 pipeline 的并行化算法。 见论文摘要
下面的 2, 3 条是启发式搜索
Path Exploration Based on Monte Carlo Tree Search for Symbolic Execution
We therefore propose novel strategies that only require limited resources to give priority to more valuable paths. We utilize a method based on the Monte Carlo tree search(MCTS) strategy to resolve the problem. We then compare the proposed MCTS-based strategy with other methodsthen such as depth-first search (DFS) and breadth-first search(BFS). MCTS is a heuristic search algorithm 这个和下面那个都是
Chopped symbolic execution_2018
allows users to specify uninteresting parts of the code to exclude during the analysis, thus only targeting the exploration to paths of importance.
However, the excluded parts are not summarily ignored, as this may lead to both false positives and false negatives. Instead, they are executed lazily, when their effect may be observable by code under analysis.
Chopped symbolic execution leverages various on-demandstatic analyses at runtime to automatically exclude code fragmentswhile resolving their side effects, thus avoiding expensive manualannotations and imprecision.
基于求解开销预测的符号执行搜索策略_来源: 计算机研究与发展
这个论文不是解决 Path Explosion 问题，而是基于约束求解预测的一种搜索策略。 符号执行中现有搜索策略在约束求解方面的考虑不够，而符号执行中很大一部分时间开销花在约束求解上.
现有的符号执行搜索策略在进行路径选择时都没有考虑到这一点，导致符号执行在分析复杂运算程序时无法在有限的时间内探索更多的程序路径，从而制约了符号执行探索路径空间的能力.
针对这个问题，本文提出了一种基于求解开销预测的符号执行搜索（solving cost predication based search，SCPS）策略，通过对符号执行中的求解开销进行经验预测，在兼顾程序语句覆盖率的前提下，优先选择求解开销小的路径进行探索，从而可在有限时间内提高探索路径的数量. 本文在开源符号执行器 KLEE 上实现了 SCPS，并在开源程序上开展了实验
基于实验总结出了度量约束复杂度的经验公式，并结合约束的历史求解开销来预测当前的求解开销，从而在符号执行过程中优先探索求解开销较小的路径. 在 KLEE 中实现了上述搜索策略，
Enhancing Dynamic Symbolic Execution by Automatically Learning Search Heuristics
A key challenge indynamic symbolic execution is how to effectively explore the program’s execution paths to achieve high code coverage in a limited timebudget. Dynamic symbolic execution employs a search heuristic to address this challenge.
However，manually designing a good search heuristic is nontrivial and typically ends up with suboptimal and unstable outcomes
The goal of this paper is to overcome this shortcoming of dynamic symbolic execution by automatically learning search heuristics. We define a class of search heuristics, namely a parametric search heuristic, and present an algorithm that efficiently finds an optimal heuristic for each subject program.
测试用例精确覆盖路径问题
上述关于符号执行的优化方法在一定程度上都能够减少路径分支并提高代码覆盖率。但是，上述各方法注重符号执行过程中的路径发现问题，而非测试用例精确覆盖路径问题，故对于特殊参数情况下的测试用例精确生成存在不足。
同时，程序中因调用大量外部环境函数且自身参数存在特殊性，故符号执行生成的测试用例导致某些路径尽管被发现了却无法被执行，进而降低了符号执行的准确性和路径覆盖率。
-
该算法通过搜索收集程序代码中函数的特殊参数， 然后利用这些特殊参数作为约束条件，最后将约束条件添加到路径的约束集中。 该算法使符号执行生成的测试用例更加精确， 从而实现覆盖特殊约束条件下的路径分支，以提高符号执行的精确性和路径覆盖率
约束求解(Constraint Solving)
以 SMT 求解器为代表的约束求解技术就是其中的典型。Z3 是由微软开发并主要用于软件验证和分析的一种 SMT 求解器。
Z3 对包含非线性计算和库函数调用的路径约束支持效果很有限。
对包含非线性计算和库函数调用的路径约束的解决策略是基于约束简化。
混合执行（Concolic execution） 就是其中的典型代表。它直接使用具体值来简化复杂路径约束 SPF-Mixed 针对复杂路径约束，优先计算路径的简单的部分，然后将解出的值代入复杂部分作为其解。除了使用具体值简化复杂路径约束，
约束重用
Constraint Solving with Deep Learning for Symbolic Executio 2020 年 3 月
Techniques like Green and GreenTrie reuse constraint solutions to speed up constraint solving for symbolic execution; however, these reuse techniques require syntactic/semantic equivalence or implication relationship between constraints. DeepSolver, a novel approach to constraint solving with deep learning for symbolic execution. Our key insight is to utilize the collective knowledge of a set of constraint solutions to train a deep neural network, which is then used to classify path conditions for their satisfiability during symbolic execution.约束简化
-
本文着眼于动态符号执行的约束求解优化问题，提出一种针对约束集合的基于线性规划技术的优化方法，通过此优化方法可以降低约束集合中约束条件的复杂性，降低后续求解生成测试用例过程的计算复杂度，从一定程度上提升了约束求解过程的效率， 本文将线性规划技术应用于约束求解过程，以此对约束求解过程中冗余的约束条件进行消除，以此达到优化的目的
通过线性拟合的技术来简化非线性约束。尽管基于简化约束求解技术的符号执行工具能够提供针对非线性路径约束的支持，但是因为该技术缩小了求解空间，所以也只能针对有限的案例适用。
基于启发式搜索的约束求解技术
这类工作的核心思想就是将复杂约束的可满足问题转化为一个搜索问题，约束的符号化变量就是搜索空间，同时设定一个目标函数用于指导整个搜索过程。 它们的性能对参数比较敏感，而这些参数比较难提前设定。
Optimization Based on domain and contextual information
Optimizing Constraint Solving to Better Support Symbolic Execution Constraint solvers are mostly used in a black-box fashion within symbolic execution, without leveraging any of the contextual and domain information available.
Because constraint solvers are optimized for specific kinds of constraints and heavily based on on heuristics，this leaves on the table many opportunities for optimizing the solvers performance
-
Most solver implementations are designed to be used as a black box, and due to their aim as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge. We present optimization techniques incorporated as a lightweight semi-decision procedure (LDP) that provides up to an order of magnitude faster analysis time when analyzing realistic programs and well-known algorithms
semantics-preserving transformations
Accelerating array constraints in symbolic execution 这个不是启发式搜索，而且他主要针对 符号执行中的 Array ，主要是它也用了保留上下文语义的方式优化，所以放在这儿。 One of the main scalability challenges is related to constraint solving: large applications and long exploration paths lead to complex constraints, often involving big arrays indexed by symbolic expressions. We propose a set of semantics-preserving transformations for array operations that take advantage of contextual information collected during symbolic execution. Our transformations lead to simpler encodings and hence better performance in constraint solving.
复杂约束的可满足问题转换为优化问题
通过设定合理的目标函数，复杂约束的可满足问题同样可以转化为优化问题。
见开头摘要
见书签 Problem&Answer 基于机器学习的优化算法 RACOS 基于一个模型对优化空间进行采样，然后通过采样点的评估反馈进行学习并优化模型，接着使用优化后的模型指导下一轮的采样。通过以上采样和反馈学习的不断迭代，RACOS 最终完成对优化问题的求解。 见书签 RACOS 的特点
将所有包含复杂数值计算的约束进行编码，将包含复杂函数调用约束编码成了未解释的路径约束。通过设定合理的目标函数，将复杂路径约束的满足性问题转化成了优化问题，然后利用底层的优化算法 RACOS 完成对复杂路径约束的求解。
预测并选择的最佳的 solver
Enhancing Symbolic Execution by Machine Learning Based Solver Selection_2019
Path Constraint Classifier (PCC), a machine learning based meta-solver that aims to reduce overall constraint solving latency by dynamically selecting a solver per query.
未分类
Neuro-Symbolic Execution: The Feasibility of an Inductive Approach to Symbolic Execution_2018
Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints_2019
symbolic execution limitations: the path explosion problem encumbers scalability,the need for language-specific implementation, the inability to handle complex dependencies, and the limited expressiveness of theories supported by underlying satisfiability checkers.
Relationships between variables of interest are not expressible directly as purely symbolic constraints.
neuro-symbolic execution—which learns an approximation of the relationship between program values of interest, as a neural network. We develop a procedure for checking satisfiability of mixed constraints, involving both symbolic expressions and neural representations.
看一下摘要里面的效果 很厉害的样子
思路二
-
虽然采用模糊测试和符号执行交替探索程序执行路径，一方面符号执行解决模糊测试陷入代码覆盖率增长慢的情况，这样能引导模糊测试探索到程序更深层次的节点，另一方面，模糊测试也能直接避免符号执行可能带来的路径爆炸问题。 但是一些实验结构表明，基于符号执行增强的模糊测试技术仍然会受限于符号执行中的约束求解问题，符号执行的引入可能会弱化模糊测试本身的可扩展性。 --- 来源 自动化到智能化: 软件漏洞挖掘技术进展
- 符号执行与污点分析结合
思路三
这只是一个想法，因为我看有些论文为了解决他们的问题，而特意改进符号执行。
对智能合约的符号执行，不知道智能合约有什么特点，要是有的话，可以针对它去改进符号执行。虽然这样不是解耦合的结构，但是应该能改善智能合约的检测结果。
下面是一些改进符号执行以适应他们要解决的问题的论文，看一下题目啥的，没准有启发？
Verifying systems rules using rule-directed symbolic execution
existing symbolic execution systems often blindly explore many redundant program paths while missing relevant ones that may contain bugs. Our key insight is that only a small portion of paths are relevant to rules, and the rest (majority) of paths are irrelevant and do not need to be verified.
