1
$\begingroup$

I am an undergraduate CS student and currently reading on software security, particularly on static analysis of programs. I am particularly interested in understanding Symbolic Execution - an implementation technique under static analysis.

So far, I am unable to understand some of the research papers on the same, because of the lack of deep understanding of Symbolic Execution and its applications and uses.

There aren't many resources on the web, and the ones that are, assume a considerable formal knowledge on this domain from the reader beforehand.

I would appreciate if somebody can explain in depth the concept of Symbolic Execution and how it can be possibly used in program analysis - identifying bugs/vulnerabilities in softwares. Any links to some helpful resources on the same that would enable a security enthusiast to get started would be highly appreciated.

$\endgroup$
  • 1
    $\begingroup$ So you are looking for an accessible survey/lecture note/book on the topic of "Symbolic Execution"? $\endgroup$ – Kaveh Jul 6 '13 at 6:46
  • $\begingroup$ @Kaveh: yes, that would be really helpful, especially if it is at a beginner-level, yet sophisticated enough for research paper survey. $\endgroup$ – dmkathayat Jul 6 '13 at 6:54
  • $\begingroup$ Why do you say there are few resources? I have listed below only a few of those available and I wouldn't consider most of them heavy in formal details. $\endgroup$ – Vijay D Jul 6 '13 at 7:53
  • $\begingroup$ @VijayD: Thanks for the links. Should help me get started. $\endgroup$ – dmkathayat Jul 6 '13 at 7:55
  • 1
    $\begingroup$ @guerrero, I would recommend you to read the CACM 2013 article by Cadar and Sen to get an explanation of classic symbolic execution and the more modern counterpart and why it evolved in that direction. $\endgroup$ – Vijay D Jul 7 '13 at 9:06
5
$\begingroup$

Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding.

If you are looking to develop your understanding by starting from a security context, I recommend this excellent summary of pointers to program analysis material from the Reverse Engineering reddit.

$\endgroup$
1
$\begingroup$

Being a beginner to Symbolic Execution (SE) myself, I would suggest:

  • Symbolic execution and program testing: this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation.
  • All you ever wanted to know...: this paper surveys SE and its applications to Security.
  • The third step may be to learn an SE engine. I would suggest Symbolic Pathfinder, it is open source and is actively maintained by NASA.
  • Vijay mentioned CUTE, DART, SAGE but they are not traditional SE, they are concolic testing tools, and are slightly different from SE described above. For example, for bounded programs, SE can be used as a verification tool, but concolic testing tools can not.

I hope this helps.

$\endgroup$
  • $\begingroup$ Thanks. I just finished reading the paper authored by J.King - Symbolic execution and program testing. I spent a few hours on it and it truly was a remarkable way to get started. I am looking forward to exploring other works. Also, I did realize that concolic execution differs from symbolic execution, but wasn't sure. Thank you for pointing out the difference. $\endgroup$ – dmkathayat Jul 6 '13 at 17:13
  • $\begingroup$ The original King paper is very readable. Good suggestion! In current usage though, "symbolic execution" almost always refers to some derivative of symbolic execution and not strictly to King's original formulation. SE cannot be used even for bounded verification if there is no theorem prover support (for example, if expressions combine addition and multiplication, or arbitrary string or heap operations). This is one motivation for concolic methods. $\endgroup$ – Vijay D Jul 7 '13 at 0:47
  • $\begingroup$ I agree with you. I do not mean SE is better than concolic testing, I just mean they are different. From Verification point of view: Verification > Symbolic Execution > Concolic Testing > Testing. $\endgroup$ – qsp Jul 7 '13 at 4:40
  • $\begingroup$ I think you should clarify what the ">" means. Also, this is an old view going back to Dijkstra and Hoare. I don't think people in the field hold that view anymore because there are tradeoffs on both side. $\endgroup$ – Vijay D Jul 7 '13 at 20:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.