Symbolic Execution was first described in 1979 in a paper by King. Java path finder uses symbolic execution it to find bugs in Java programs. In recent years, Dawson Engler released a paper on ExE, to fing bugs in the Linux Kernel. Dawn Song’s BitBlaze group also use symbolic Execution to show the capabilities of Windows malware. In binary applications, catchconv can find signedness bugs in Linux executables using a symbolic execution implementation forked from Valgrind.
Symbolic Execution is a promising technology, that appears more capable than either purely static or purely dynamic approaches to binary analysis in a number of applications – including bug checking and intelligent fuzzing.
So what is Symbolic Execution?
Symbolic Execution treats variables as algebraic symbols capable of representing a range of concrete values. As the program executes, a list of formula is built using those symbols. The concret results of execution at any specific time is the set of solutions that satisfy those built up formulas.
We can determine solutions to queries about the formula that we have built. If the expression x divide y is parsed, we can ask if y is ever equal to 0. The answer looks at all the possible values for y, and can tell us if this is the case. This is much more powerful than fuzz testing, which can only ever determine a divide by zero across a single test case. in Symbolic Exectutin, more bugs can be identified than just divide by zeros. Assertions can be resolved at any point in program; assertions such as null pointer dereferences, or even buffer overflows.
When a condition is introduced in a program, a constraint is added to the formula that represents program execution. An example constrain is x being less than 5, or y not being equal to x. there There are two paths for a condition, the constraint being true and the constraint being false. To represent this symbollically, execution splits into two, one set of formula representing the true path, another set of formula representing the false path. The constraint respective to the condition being followed, is added to the formula.
Forking at branches, allows symbolic execution to systematically explore different paths in the program. The Bitblaze project uses this, to determine the capabilities of malware by systematically identifying what the malware does along all identified paths.
Symbolically executing a program introduces an exponential number of paths to be analysed proportional to the number of lines of code. A practical solution to path explosion, is to execute symbolically only the parts of the program we are interested in.
Mixed symbolic execution marks data as either symbolic or concrete. If an expression is purely concrete, it is executed natively. If the expression has symbolic components, it is executed symbolically. BitBlaze, Dawson Engler’s ExE and Catchconv all use mixed symbolic execution and can run on reasonably priced PC’s; you dont need a supercomputer.
The constraint solver used in BitBlaze, Exe and Catchconv is STP (Simple Theorm Prover), written in conjunction with ExE specifically for applications in bug checking. These types of theorem provers are SMT or Satisfiablity Module Theories. It is a generalized version of SAT, or Boolean Satisfiablity theories. Apparently in the past 10 or 15 years much progress has been made in SAT solvers and this is said to account for the recent popularity of it in program verification.
I’m pencilled in to speak at Ruxcon this year. The title of my talk is Code Emulation for Malware Unpacking. Its a summary of the work I’ve done over the past few months in writing an x86 and win32/linux emulator. An application of code emulation is automated unpacking of malware. Code emulation has been a mainstay of commericla AV for the last 15 years. It is used in unpacking, and in identify polymorphic viruses. There are no public unpackers based on code emulation to my knowledge.
My work in emulation is good, but not very exciting.
I’m not promising anything, but I am hoping that by the time Ruxcon comes around, I will have some working results in something more exciting. I’ve started coding only this week, so the clock will be ticking; Symbolic Execution of Cisco IOS.
Dynamips is an opensource Cisco emulator. Perhaps emulator is not the right word, as it also uses dynamic binary translation (just in time compilation) to achieve speed. QEMU uses dynamic binary translation also.
I had to learn MIPS assembly. Its a RISC architecture, and has a really easy to understand instruction set. It’s much easier than x86.
The input in Cisco IOS to be marked as symbolic, is the receiving of network traffic. My code is planned to symbolically explore the network stack.
I have to dynamically instrument each instruction that is emulated in dynamips. Each instruction is executed concretely or symbolically. If all operands are concrete, the instruction is executed conretely (by dynamips). If any operands are symbolic, then the instruction generates a set of formula for use by STP, and the result of the instruction is marked as symbolic. I have written the code for all the general arithmetic and bitwise operations. STP constraints are generated for each respective instruction.
Memory loads and stores are tricky. The problem is getting the theroem prover to work on only the data you are interested in. But for example, when performming a load operation and the address is symbolic, potentially ALL of memory is referenced by the symbolic operation. I solve this by maintaing a table of all of memory identifing each of the memory contents as being symbolic or concrete. At loads and stores with symbolic addresses, I solve the points-to set (where the symbolic addresses can point too) using STP, and update my tables and data accordingly. I hope STP does not take too long when running live. I have only a couple load and store operations implemented. There are quite a handful of operations in MIPS, LB, LBU, LW, LWL, LWR, lWU, lD, lDL, and LDR for the loads (if my memory is right), and an equal amount for the stores.
The only problem I have with this, is that while the number of memory addresses I refer too is probably quite small, the size of the array (which is sparse) handled by STP is 4g – all of the MIPS virtual memory. I am not sure if STP is capable of solving the constraints I generate. I will have to wait until I have a working implementation before I can say that this approach will work.
At branches, execution will need to fork. There will also be a need to select which paths to execute. I haven’t implemented any of this yet.
Booting of IOS takes a couple seconds on my vintage hardware. Executing it symbolically will probably take even longer. I made modifications to dynamips to save and restore running VM’s, much like vmware’s suspend and resume. It’s not perfect, as I dont save state of things like DMA and many other things, but it did work in a test run tonight. This was saving state when IOS was idling. Startup time on restore was almost instaneous.
I will start symbolic execution when IOS is fully booted. But I will need to determine when the run terminates. I imagine I will need to check that the program counter is back to IOS’s idle loop. I haven’t implement this part either.
So that’s my plan and where I’m at. Hopefull this isnt pie in the sky stuff and I’m able to get a working implementation. At best I hope to find real bugs in the cisco network stack. At worse I hope to perform intelligent fuzzing of IOS covering code and paths efficiently. I dare not say worse case is not finishing..
Incidentally, I am thinking of doing a Master’s degree by research next year. I think that symbolic execution seems to be a good project.