Implement general dynamic symbolic execution

[zimmski]

http://research.microsoft.com/en-us/projects/pex/ shows clearly that dynamic symbolic execution is a key changer for simple unit tests. Pex is only for .NET languages especially only for C# and there are other DSE projects e.g. for Java but there is no general DSE tool. Tavor could fill this gap easily by implementing a general symbolic execution which is fed by different source code parsers for different languages. DSE could then be also implemented in general by implementing agents for different langauges.

E.g.

• Language code parser -> Tavor SE AST
• The Tavor SE AST should then be Handled by the Tavor SE implementation which generates path constraintes and so on
• Tavor SE should then talk to the Language Agent to exectue code with given parameter values which makes it DSE

Allow different strategies for branch selection:

• DFS, BFS -> which are according to the Pex papers not very efficient
• Copycat Pex's implementation which is nothing but excellent

[mstone]

FWIW, in the field of symbolic (& concolic) execution, klee and s2e both have friendly licenses, are well worth studying, and have very friendly development+research teams backing them. (Also, in the same vein, FuzzBALL/VINE/BitBlaze may also be worth a look though I have no personal experience using their work.)

(NB: by contrast, several years ago, I wrote up a small example to demonstrate Klee's usage here: http://mstone.info/posts/klee_quickcheck/ and have used both klee and s2e more privately over the last few years to find some interesting bugs in, e.g., open source image-parsers and network protocol parsers.)

[zimmski]

Cool, thanks! I took a look at klee and s2e. They both look very interesting. The fuzzball website is currently down http://bitblaze.cs.berkeley.edu/ I will check on it tomorrow.

Symbolic execution is unfortunately not at the top of my TODO for Tavor. After I announce the project and fix the remaining bugs, I will focus at first on file format fuzzing and model-based testing so I can use it on more test projects at work. Since I am not working full time on the project (it is my master thesis but I am done with the coding part) I am hoping to get some help from the community. My personal milestone is to reach functionality equality with https://github.com/OpenRCE/sulley but with easier and shorter definitions for the fuzzers.

[zimmski]

I am currently working on this in another project. This can then be later integrated with Tavor.