In this final video in the series we go over how to generate new inputs for a program once we detect a user-influenced conditional branch. At the end there is also an example of the type of condition/resulting formula that we get from working on a real file parser, in this case libwebp.
(You probably want to click the “Watch on YouTube” option on the bottom right of the video and set the quality to 720p)
Conclusion
This type of emulation, input generation and formula checking does not need to be limited to conditional jumps. As I discussed in a previous post you can use a similar approach to discover variable ranges, check for variable relationships and assist in figuring out complex algorithms. For example, one could generate a query to the solver every time an argument to malloc is found to be influenced by the user, or export a list of all functions that operate on user-influenced data to IDA for manual review. (In fact, a light-weight version of this approach in combination with fuzzing and an IDA importer is possibly more generally useful to an individual auditor than going down the route of full on whitebox fuzzing. More on that later =))
Anyway, I hope these videos provide some insight into how a whitebox fuzzer might work as well as one approach to building a symbolic emulator. To give an idea of the effort involved – the combined whitebox fuzzing, trace parsing and emulation code (along with supporting libraries) comes to around 10,000 lines of Python. Of this, the emulator itself is only 3000 lines or so. The PIN tracer is just under 1000 lines of C++.
Tracing is currently fairly unoptimised and parsing something like a video or image while tracing can result in a factor of 10-100 increase in running time. This usually means a wait of 30 seconds, which isn’t too bad for whitebox fuzzing as tracing is not performed too often but for other uses of a symbolic emulator (like tracing while fuzzing normally) this will require some work. The emulator itself is Python based and as such is not lightning fast. In the default run-mode it emulates ~5000 instructions per second. What this translates to is about 30-40 minutes per trace of an average file parser. This isn’t as bad as you might think however as the tests cases generated tend to be much more effective at hitting new code than what you would get from dumb fuzzing. Despite this we still need performance gains and I’m working on a few different solutions for that. Somewhere around 30,000+ instructions per second would be what I would consider approaching acceptable =)
To preempt the inevitable questions – for now JESTER is not publicly available but that may change in the future. It’s very much a research prototype at the moment where we’re testing out several approaches to improving performance and general usefulness. However, if you are interested in working on this type of research post a comment with a contact address (it won’t appear publicly) as I’m fairly sure we are currently hiring.
Sean Heelan's Blog 
Hi Sean,
I enjoyed watching the videos. It looks like a nice tool.
In the interpreter, did you write the code for the individual
instructions by hand or did you auto generate it from a specification?
How complete is the emulator?
Checking the results of the interpretation against the concrete values
from the trace is a good idea. I’ve written some similar tools but
never thought to do that. Do you need those concrete values for
anything else? If not, I guess you can shrink the trace-size
considerably.
Hey, I hand-coded the handler for each instruction. This is not ideal of course but at the time I figured it would be just as much effort to draw up a spec detailing instruction semantics then have a generator for that. In January I was at an academic conference where there seemed to be an interest in having a formal semantic specification for x86, ARM etc so hopefully something will come of that and we can all stop re-coding these things from the ground up.
The emulator is complete enough that I have yet to see any divergences between the semantics of generated formulae and the semantics of the code it refers to. I am missing plenty of instructions but the vast majority of common ones are handled. When I started I ran a bunch of sample programs on Windows and Linux and made a list of every instruction that occured more than a certain number of times, then started with those.
It currently does not handle most floating point instructions but it does handle some MMX/XMM ones. For now I’m not really focused on writing handlers any more as, like I said, I’m not seeing many cases where things I care about are influenced by instructions I don’t have (except for bt and cmpxchg which I just noticed appear to have gone missing! I could have sworn I implemented those two before….)
The concrete values are not used for anything else. I only run the tracer in debug mode when I’ve got some bug showing up during emulation and I want to track down what instruction handler is broken. Normally that is disabled so the traces are half the size as otherwise.
Do you remember who / what conference? Having such a specification would simplify a lot of my work.
I know you don’t want to do a public release, but would you consider sharing the tool privately? Feel free to email me if you want to discuss outside of the comment system.
Yea, it was the Dagstuhl seminar on analysis of executables in January of this year. From that there were too initiatives that people expressed interest in. The first was a common format for generating disassemblers and the second was for a common format and specification of semantics. The first task has seen some work but the second hasn’t really got off the ground yet from what I can tell.
Just wanted to say thanks for taking the time to make these videos. This is an interesting area of study that is just now finding its way out of academia and into public security research.
Great videos, thanks for posting these! In the beginning of this video (as well as in your second video) you mention that you create symbolic flags. Do you create symbolic flags for all flags that affect conditional jumps, or just the most common ones? For instance, something like a Parity flag could get very difficult to represent to a solver… how do you represent something like that as a bitvector?
I create symbolic versions of all the flags, including the parity. It’s not used that often but every now and then you hit a JP. Representing it isn’t as straightforward as the zero flag, for example, but it’s not complex either.
Starting with the 0th bit, XOR that with 1st bit and then then result with the 2nd bit and so on, up to the 7th bit. Negate the result and you have your parity bit. On an abstract value you end up with an expression tree a few layers deep with XOR, shifts etc. but still quite simple and easily converted to SMT-LIB format.
Sean,
First of all, great videos! I’m very interested in this field of research and I am really struggling to find tools in the wild that actually utilize symbolic execution. In my thesis work, I built my own symbolic emulator, but it will need some serious tweaking before it is anything more than a research project. While I know you said in this post that JESTER is not publicly available, but I would love to see your code in order to better understand how to build a whitebox fuzzer and continue my research. If you don’t want to share it, I completely understand, but in the event you would like another pair of eyes looking at it and maybe even continuing work on it, please let me know.
Hi Seth,
Thanks for your comments. I no longer work for Immunity and as JESTER was developed during my employment there I am not at liberty to share it. I’m working on a similar engine at Persistence Labs now however, and once it is done I expect I’ll make it easily available for academic research. Have you looked at S2E, TEMU, BAP and KLEE btw? All of those provide some form symbolic emulation support.
Once it’s ready I’ll drop you a mail (presuming you left one when you commented =)) If you have any specific design questions however, feel free to drop me an email to sean [at] persistence labs.com
Cheers,
Sean