SANER 2020上的一篇Poster
简介
符号执行是软件测试和程序分析里一个很重要的技术。路径爆炸是符号执行里一个很严重的问题。为了缓解这个问题，文章提出了一种基于Q-learning的算法来指导符号执行。
方法
Q-learning算法是一种model-free off-policy的算法。给定一个状态，算法能够估计一个动作的长期expected return。这个expected return 也叫做Q-value。Q-value越高，意味着动作 A t A_{t} At?在状态 S t S_{t} St?上产生更好的长期结果。
在符号执行例子里，Q-learning里的状态表示程序执行到的语句。动作表示符号执行在遇到分支语句时，选择true分支还是false分支。当语句运行到关键点时，奖励值为正的。
具体实现上，首先在源码中设定目标语句，并且用静态分析获取路径上的关键点。然后，当符号执行遇到分支语句时，会将当前状态的信息发送给Q-learning，并且获取到action的建议（true or false）。基于 ε ? g r e e d y \varepsilon-greedy ε?greedy规则，klee有 ε \varepsilon ε的概率选择Q表的值，也有 1 ? ε 1-\varepsilon 1?ε的概率随机选择一个action。然后在每个分支结束后，再返回给Q-learning reward，来更新Q表。只有程序运行到关键点的时候，reward才为正的，其余情况都为负的。
如果程序被中止了，并且没有到达目标语句，程序就会重启执行。这种情况下，klee会发送fail信号给Q-learning，Q-learning会选择一个新的执行状态给KLEE。选择需要以下三个步骤：
- 列举出上个执行过程中所有可能的候选状态
- 计算每个候选状态的概率
- 选择最大概率的作为新的状态
举个例子，假如在第一轮执行过程中没有到达目标就中止了，他的分支选择序列是101（true false true），由于每次fork都会生成两个状态，所以候选状态有（0，11，100）当前状态的概率是所有前面状态的的累乘得到的。比如：
P ( 100 ) = P ( 1 ) ? P ( 1 ∣ 0 ) ? P ( 10 ∣ 0 ) P(100) = P(1) * P(1|0) * P(10|0) P(100)=P(1)?P(1∣0)?P(10∣0)
一直持续这个过程，直到到达目标点，或者超时。
评估
在sv-benchmark上测试了60个程序，结果在筛选路径上确实是过滤了很多路径。但是花费的时间也更多。因为需要计算Q-learning的value值。
