地狱怪客

如何学习符号执行(Symbolic Execution)

来源:https://www.zhihu.com/question/38727250

ls的答主说得很好,我补充几个项目DART(PLDI 05), EXE(CCS 06), Sketch(ASPLOS 06), SAGE(NDSS 08)。另外有个“微型”项目 GitHub – xiw/mini-mc(作者是谁就不用介绍了..)
两点建议:

从特定应用需求(如果有的话)出发:testing, verification(比如invariant generation), synthesis, repair等等,symbolic execution的设计各有不同。.

从通用的技术问题出发,除了symbolic execution,其他技术也有这些问题。学习某项目时可以重点看它们是如何处理的:

  • Loops and recursion:是unroll/inline还是借助invariant inference
  • Path explosion:各种path selection策略(加入启发式方法?)..
  • Heap modeling: 借助shape analysis/pointer analysis? lazy concretization? 用solver的array theory?
  • Environment modeling: library, os等环境。
  • Solver limitation:从生成到求解的各种优化策略..
github.com/saswatanand/ 这里有一个关于符号执行的文献列表,此外CACM 2013-02 有一篇Symbolic Execution for Software Testing: Three Decades Later的文章可以作为入门。入手项目的话,感觉klee的文档比较全。

首先随便找个开源Symbolic Execution工具,看自带的教学,从自带的例子(如果有)开始试着玩玩各种功能。可选的工具其他人已经说差不多了,再提一个最近才开源的angr:
angr, a binary analysis framework
DARPA CGC胜者组!融合了最近几年的数种优化技术!有能用的Veritesting真令人羡慕;w;

如果想要深入理解,玩的同时可以看看这方面的论文。虽然市面上有多个开源的Symbolic Execution工具,但是基本原理都差不多,所以看个一两篇就够了。嫌整篇论文太长的话也可以找篇最近的Symbolic Execution论文看看Background的部分。

其他一些我所知道的开源Symbolic Execution工具:
KLEE
Overview – S²E: A Platform for In-Vivo Analysis of Software Systems
CREST by jburnim
FuzzBALL: Vine-based Binary Symbolic Execution

码字很辛苦,转载请注明来自人生在世《如何学习符号执行(Symbolic Execution)》

评论