[oss] Using symbolic execution for reverse engineering

[Lucian Mogosanu]

Hi everyone,

ctfhacker.com has a post on combining radare2 and symbolic execution to
reverse engineer a CTF binary [1]. You might remember radare2 from the
first labs. Although its interface is a bit clunky, the post shows a few
interesting uses in the preliminary stages of reversing.

For those of you who are not familiar with it, symbolic execution is an
analysis technique that involves looking at programs, extracting
execution path constraints (based on branch conditions) and determining
for example if a point in the program is reachable, what inputs
(including "anomalous" inputs such as buffer overflows) can reach it,
and much, much more.

Symbolic execution engines are now emerging as state-of-the-art tools in
both offensive and defensive security (e.g. as alternatives or
complements to fuzzing tools), so do take a look at them if you're
interested in the subject.

[1]: http://ctfhacker.com/ctf/python/symbolic/execution/reverse/radare/2015/11/28/cmu-binary-bomb-flag2.html

Lucian