Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

Boosting Concolic Testing via Interpolation

论文下载:https://www.comp.nus.edu.sg/~joxan/papers/testing.pdf

ABSTRACT && INTRODUCTION

  • 优化concolic execution的工作
  • 当前的优化方法:启发式搜索策略、简易功能缓存、动静结合
  • 作者提出搜索剪枝的方法:如果一个test遍历了一条路径,当下次另一test遇到相同情况的时候就可实现剪枝
  • concolic execution(我是传送门)

RUNNING EXAMPLE

Fig

  1. 假设两个read()都非0,程序执行到l_8,路径可达,没有bug
  2. 反转l_6的条件,发现不可达,所以l_6这个subtree搜索完成,条件是s <=3(这个例子有点违和,在符号执行里面放bug不可达)
  3. 回溯,到l_4,发现分支l’_6,但条件是s < = 1,满足刚才l_6的条件,所以不用再搜索
  4. l_4搜索完全,条件是s < = 1

ALGORITHM

Fig

  • 每当产生一条新的路径,就检查是否被搜索过
  • 如果没有被搜索过,就执行concolic execution,但会记录每个分支的搜索条件和情况,即SymExec这个过程
  • SymExec包括回溯的过程,对于回溯的搜索作了限定:每个program point只被搜索至多一次,当再次经过的时候,检查是否可以被剪枝,如果不行,放弃回溯
  • 保证回溯是O(n)

Evaluation

  • 4 programs from the ntdrivers-simplified category of SV-COMP’12
  • 1000 – 2000 LOC
  • 控制流复杂,有大量路径

Performance

Fig

  • b明显说明回溯的作用

Subsumption

  • 剪掉的路径数量百分比

Fig

Extra path-coverage

  • 隐含福利,回溯的时候存在额外搜索,作为主搜索的补充
  • (作者没有说明数据获取细节,但这个福利未免太大了)
  • Fig