DART and CUTE: Concolic Testing

[skyleaworlder]

https://www.cs.cmu.edu/~aldrich/courses/17-355-17sp/notes/lec-concolic-sen.pdf

Koushik Sen
University of California, Berkeley
Joint work with Gul Agha, Patrice Godefroid, Nils Klarlund,
Rupak Majumdar, Darko Marinov

[skyleaworlder]

[skyleaworlder]

给出了 p50-83 给出了 CUTE 的机制：

• 同时维护 concolic state 和 symbolic state，利用 symbolic state 表示 constraint，每一步都同时使用 concolic state 和 symbolic state；
• 每次为 symbolic state 中的 variable 生成一套具体值，这套具体值希望能够走与先前不同的路径；
  • 具体值方便程序执行，符号值表示的 constraint 又指导了下一次具体值向其他路径的生成；
  • Concolic testing 是动态的，不必执行一些静态分析无法排除的 block；
  • 具体值自带内存表示，可以解决 alias / array / pointer 的问题，而这本来是纯 symbolic 不方便的；
  • 我猜测这样也能更好地利用缓存机制。

[skyleaworlder]