The problem of input crafting can be stated as follows: given the ability to influence some aspect of a program's execution (say, by supplying it with a hand-crafted file, network input, sequence of keystrokes, etc), we want to know whether it is possible to cause the program to reach some state, for example, a condition where the integer argument to some memory allocation function is zero, a specific sequence of branches being taken causing EIP to obtain a certain value, an array dereference whose index is not within its bounds, etc. Much work in reverse engineering for vulnerability analysis and software cracking reduces to this problem; some malware analysis problems can also be stated in such terms.
It is well-known in the formal verification literature that symbolic execution, a method for reasoning about program executions based upon formal semantics and theorem proving, may be applied towards this problem. However, actual tools that can be used in a friendly fashion have not yet materialized in the hands of the common, working reverse engineer. This blog entry demonstrates a prototype of a tool of this nature.
Crafting inputs with manually-generated SMT instances
Bookmarks