Automated Key Generator Generation

Originally published on March 6th, 2012 on OpenRCE, under the overly-academic title "[video] Semi-Automated Input Crafting by Symbolic Execution, with an Application to Automatic Key Generator Generation"

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

We take as our example program a crackme called Kao's Toy Project, which recently attracted the scrutiny of Dcoder and andrewl, two clever computer-hacking mathematician types.  Note:  I would have used a vulnerability analysis example since it might be more compelling to a general audience, however, the notion of producing a reverse engineering video involving commercial software is not a palatable one for legal reasons, and therefore I chose a program that was deliberately designed to be reverse engineered.

The crackme implements the following scheme.  When presented with a 32-byte activation code, the user enters a hexadecimal string such as "01234567-76543210", which is then decomposed into two dwords, one of which is XORed with the other, and the following compact loop is executed:

.text:004010F7 mov     esi, offset a_ActivationCode
.text:004010FC lea     edi, [ebp+Output]
.text:004010FF mov     edx, [ebp+arg_0__SerialDwLow]
.text:00401102 mov     ebx, [ebp+arg_4__SerialDwHigh]
.text:00401105
.text:00401105 compute_output:
.text:00401105 lodsb
.text:00401106 sub     al, bl
.text:00401108 xor     al, dl
.text:0040110A stosb
.text:0040110B rol     edx, 1
.text:0040110D rol     ebx, 1
.text:0040110F loop    compute_output
.text:00401111 mov     byte ptr [edi], 0
.text:00401114 push    offset String2                  ; "0how4zdy81jpe5xfu92kar6cgiq3lst7"
.text:00401119 lea     eax, [ebp+Output]
.text:0040111C push    eax                             ; lpString1
.text:0040111D call    lstrcmpA

Given that the user's input consists of two dwords, the key space is 2^64.  Dcoder and andrewl offer an observation that halves the exponent to 2^32.  Dcoder further offers an algebraic cryptanalysis of the scheme that obliterates it.  andrewl chose to explore the route of modelling the scheme in terms of the Boolean Satisfiability (SAT) problem, and then feeding the result into a SAT solver.  The resulting SAT instance is solved more or less immediately.

We followed andrewl's line of reasoning and manually constructed a representative Satisfiability Modulo Theories (SMT) formula.  (To be technical, the formula is a sentence in a quantifier-free fragment of first-order logic restricted to the theories of equality, bitvectors, and extensional arrays.)  The formula does not explicitly take advantage of any aforementioned, known flaw in the cryptosystem, and instead encodes the algorithm literally.  We believe that the reader will find the resulting SMT formula very clear and easy to understand.  This is an advantage over a SAT instance, which is virtually incomprehensible and harder to debug.  The SMT instance is a bona-fide key generator, and furthermore the theorem prover is able to solve the formula in milliseconds (considerably faster than a brute-force search over a 64-bit keyspace).

We outline the SMT instance:  Line 1 sets the theory. Lines 3-7 declare the variables of interest, as well as the array sort. Lines 9-40 encode the serial algorithm. Lines 42-73 state that the output array must equal the fixed value given in the crackme. Lines 75-106 encode the activation code that was given by a given instance of running the crackme. You can replace these lines with whatever your own activation code was, thereby creating a key generator. Lines 108-110 encode the additional constraints where one of the serial dwords was XORed with the other. Lines 112-113 query the decision procedure and output the results.  After installing Z3 (other theorem provers such as Yices are also suitable), one solves the formula as follows:  C:\Program Files (x86)\Microsoft Research\Z3-3.2\bin>z3 /m /smt2 \temp\kao.smt.

Generating the constraint system automatically, directly from the binary

This is all well and good, but manually encoding algorithms as SMT instances is tedious business.  Instead, we seek a solution that can automatically generate the relevant constraint system directly from the x86 binary.  The current solution is a static analysis (i.e. it does not alter or observe the execution of the program).

The algorithm proceeds in three main phases:

1)  Trace generation.  Since the algorithm is static, the analyst manually specifies some parameters to the system:  namely, an address from which to start the analysis, a model of the initial values of the registers and memory, and some condition that dictates when the analysis should stop.  (Note that, if we were to reformulate our analysis in a dynamic setting, many of these considerations would be superfluous.)  The tool then statically emulates the program, generates a list of instructions encountered during the emulation, and converts them into an intermediate representation.

2)  Trace simplification.  We apply other static analyses against the trace to simplify it, which could potentially speed up the solving.  Analyses could include constant propagation, dead statement elimination, or the abstract interpretation that I published last year.  This step is actually optional in the sense that the simplifications preserve satisfiability.

3)  Constraint generation and solving.  With our trace in hand, we transform it into an SMT instance and feed the resulting equations into a theorem prover.  Additionally, the user supplies some postcondition that corresponds to the state that he or she wishes for the program to enter.  We then check satisfiability, and if the formula is indeed satisfiable, the theorem prover can furnish a model of the inputs that cause the desired state to be reached.

With all of that out of the way, here is a link to the actual video depicting the process.  I apologize if the video is tedious (I am tedious) and for the stupid manner in which I sound (I am stupid, and also I am from the American south).  The files referenced in the video, kao-1.ml through kao-3.ml, are linked to above in the description of the algorithm.

Key-generator generation

​Given the construction laid out in the video referenced above, generation of a key generator is now trivial.  Instead of asserting in the postcondition that the activation code is fixed to whatever value was observed in the construction of the constraint system, we allow the user to enter his or her own activation code, which we then assert as the initial values of the activation code array.  We then solve the system as described in the video and part 3 of the code linked above, and provide the user with the proper registration code (EBX and EDX values).

Postscript

An astute proofreader wondered why, during the video, when I solved the manually-constructed instance with Z3, it reported an error about a model not being available.  In fact, the formula solved correctly (as evidenced by the output saying "sat"), but I did not specify the "/m" flag on the command line due to it skewing the time statistics, which resulted in that message being produced.  The reader can manually verify that the formula is correct with the command line given previously.

Finding Bugs in VMs with a Theorem Prover

Originally published January 22nd, 2012 on OpenRCE.

Equivalence checking is a popular technique in the academic literature and in industrial practice, used to verify that two "things" are equivalent.  Commonly, it involves translating those things into some logic that is supported by a theorem prover, and asking the decision procedure to prove whether the two things must always be equal.  Equivalently, we ask whether there exists any circumstances where the two things might not be equal.  If the two things must always be equal under all circumstances, then a complete decision procedure will eventually report that the formula is unsatisfiable.  If they can ever deviate, then it will return a "counterexample" illustrating a scenario in which the things differ.  The decision procedure may not terminate in a reasonable amount of time, or do so at all if the logic is undecidable or the decision procedure is incomplete.


Equivalence checking is commonly found in the hardware world (particularly, in a field known as Electronic Design Automation, or EDA), but it has been applied to software as well, for tasks such as verification that compiler optimizations have been implemented correctly, verification of cryptographic implementations, and other forms of specification-conformance.  In this blog, we'll take a look at an application of equivalence checking in deobfuscation.

Equivalence Checking

We begin by giving an example proving the equivalence between an x86 sequence and a machine instruction.

Bit-level hackers -- those who study the works of the original MIT "hackers", whose work bequeathed the term "hacker" -- will know the following example regarding taking the population count of a 32-bit integer.  The "population count" of a given integer is the number of one-bits set in the integer.  This operation is known as "popcnt", and the x86 instruction set features an instruction of the same name, whose syntax is "popcnt r32, r/m32" and whose semantics dictate that the population count of the right-hand side (32- or 16-bit, depending upon encoding) be deposited into the location specified by the left-hand side.  We can easily imagine implementing this functionality with a loop:

int popcnt = 0;
for(int mask = 1; mask; popcnt += !!(mask & value_to_compute_popcnt_of), mask <<= 1);

A hoary MIT HAKMEM gem shows how to compute the same value via a series of arithmetic manipulations and no explicit loop.  We summarize the procedure below.

Consider some 8-bit integer, whose bits we shall represent symbolically with letters as in the following:

abcdefgh

Let's demonstrate how the method computes the population count of this integer.  First, we separate out all of the even bits and the odd bits:

x = ((x & 0xAA) >> 1) + (x 0x55);
abcdefgh AND
10101010
--------
a0c0e0g0 SHR 1
--------
0a0c0e0g


abcdefgh AND
01010101
--------
0b0d0f0h


Adding these two quantities together, we obtain the following result:

wwxxyyzz

Where ww, xx, yy, and zz are each two-bit quantities such that ww = a + b, xx = c + d, yy = e + f, and zz = g + h.  By adding these masked-and-shifted quantities together, we thereby compute the sum of two adjacent bits, and store the sum in that location within the integer that corresponds to those two bits.  Given that 0+0 = 0, 0+1 = 1, 1+0 = 1, and 1+1 = 10, the sum can never overflow, and is hence neatly contained in those two bits.

Next, we perform the same kind of trick to compute the sum of each two-bit quantity.  We use a similar shift-and-add tableau:

x = ((x & 0xCC) >> 2) + (x & 0x33);
wwxxyyzz AND
11001100
--------
ww00yy00 SHR 2
--------
00ww00yy

wwxxyyzz AND
00110011
--------
00xx00zz

Adding these two quantities together, we get:

iiiijjjj

Where iiii and jjjj are the 4-bit results such that iiii = ww + xx and jjjj = yy + zz.  Once again, this sum is safe from overflow because ww and xx are at most 2-bits, whereas iiii and jjjj are 4-bits.

We pull the same trick again to sum the quantities iiii and jjjj:

x = ((x & 0xF0) >> 4) + (x & 0x0F);
iiiijjjj AND
11110000
--------
iiii0000 SHR 4
--------
0000iiii

iiiijjjj AND
00001111
--------
0000jjjj

Adding these two quantifies together, we get kkkkkkkk, where kkkkkkkk = iiii + jjjj = ww + xx + yy + zz = a + b + c + d + e + f + g + h.  This corresponds to the definition of the population count of an 8-bit integer.  We can easily imagine extending the same procedure for 16-, 32-bit, 64-bit, and generally 2^n-bit quantities.  Below we display a fragment of x86 assembly language that computes the population count for a 32-bit integer

Sequence (1) -- messy bit hack for eax = popcnt(ebx)

mov eax, ebx
and eax, 55555555h
shr ebx, 1
and ebx, 55555555h
add ebx, eax
mov eax, ebx
and eax, 33333333h
shr ebx, 2
and ebx, 33333333h
add ebx, eax
mov eax, ebx
and eax, 0F0F0F0Fh
shr ebx, 4
and ebx, 0F0F0F0Fh
add ebx, eax
mov eax, ebx
and eax, 00FF00FFh
shr ebx, 8
and ebx, 00FF00FFh
add ebx, eax
mov eax, ebx
and eax, 0000FFFFh
shr ebx, 16 
and ebx, 0000FFFFh
add ebx, eax
mov eax, ebx

This is equivalent to the x86 instruction

Sequence (2) -- direct ISA computation of eax = popcnt(ebx)
popcnt eax, ebx

Except that the former example also modifies the flags in some certain way, and modifies the ebx register, whereas the popcnt instruction modifies the flags in a different way and does not modify ebx.

We would like to prove the equivalence of sequences (1) and (2) with respect to the relationship of the resulting eax register with the original ebx register.  We must not consider the resulting value of the ebx register or the flags, for in that case, the sequences will not be equivalent in general.  The code for performing this task in Pandemic follows.

(* Define the x86 sequences *)
let hack_sequence_x86   = (* declaration of sequence (1) as X86.x86instrpref variant types *)
let popcnt_sequence_x86 = (* declaration of sequence (2) as X86.x86instrpref variant types *)

(* This function converts each sequence to IR *)
let make_ir_sequence x86l = List.concat (List.map (X86ToIR.translate_instr 0l) x86l)

(* These bindings are the IR translations *)
let hack_sequence_ir   = make_ir_sequence   hack_sequence_x86
let popcnt_sequence_ir = make_ir_sequence popcnt_sequence_x86

(* These bindings are the results of converting the IR sequences to SSA form *)
let   hack_tbl,  hack_sequence_ir_ssa = IRSSA.bb_to_ssa_state_out X86ToIRUtil.num_reserved_vars   hack_sequence_ir
let popcnt_tbl,popcnt_sequence_ir_ssa = IRSSA.bb_to_ssa_state_out X86ToIRUtil.num_reserved_vars popcnt_sequence_ir

(* The postcondition says that sequence(1).eax != sequence(2).eax *)
let hack_popcnt_postcondition = 
  IRUtil.mk_not 
   (IRUtil.mk_eq 
     (IRUtil.mk_evar (Hashtbl.find   hack_tbl X86ToIRUtil.vEax))
     (IRUtil.mk_evar (Hashtbl.find popcnt_tbl X86ToIRUtil.vEax)))

(* We query the theorem prover as to whether eax from the ends of the respective 
   sequences are equal.  We do this by asking the theorem prover to generate an
   example where they are not equal, which it is unable to do (the formula is
   unsatisfiable), and therefore they are equal on all inputs. *)
let _ = IDA.msg "%s\n" (Z3SymbolicExecute.symbolic_execute (Z3SymbolicExecute.mk_context ()) (hack_sequence_ir_ssa@popcnt_sequence_ir_ssa) hack_popcnt_postcondition)

The theorem prover cranks for 10 seconds and returns that the formula is unsatisfiable, in other words, that it was not able to generate a counterexample where sequence(1).eax != sequence(2).eax.  Assuming the soundness of Z3 with respect to propositional logic over the bitvector and array theories of finite domain, we have just generated a mathematical proof that the sequences have the same effect on the eax register.  Z3 can be configured to output the proof explicitly so that it may be checked by other tools.

Equivalence checking for verification of deobfuscation results

​I had written a deobfuscation procedure (e.g., a program of the type described here) for a commercial VM ("VM" meaning virtualization obfuscator in this context), and I wanted to know whether my deobfuscation was correct, since I felt like I might've taken some shortcuts along the way.  Given access to some obfuscating transformation O, and access to a deobfuscating transformation D, we want to know if D(O(p)) is a semantics-preserving translation for all programs p.  We'll settle for random testing:  generating a "random" executable according to some guidelines, obfuscating it, deobfuscating it, and comparing (by equivalence checking) the deobfuscated program against the original, pre-obfuscated version.  As it turns out, the translation D(O(p)) is not semantics-preserving because VM itself has many bugs that could affect the translation of the original x86 into the VM bytecode. 

The procedure in the last paragraph can provide us with straight-line sequences of code (or control flow graphs) such that one is the original, and the other is the obfuscated version with deobfuscation applied.  We can then apply equivalence checking to determine whether these sequences are semantically equivalent.

It turns out that they often are not.  For example, consider this obfuscated sequence (which has been mostly deobfuscated for the sake of easy illustration):

mov cx, word ptr [esp]
add esp, 2
ror dword ptr ss:[esp], cl
pushfd

And the corresponding deobfuscated sequence:

pop cx
ror dword ptr ss:[esp], cl
pushfd

The former example has a similar effect as the latter one, but it modifies the flags before the rol instruction executes.  The rol instruction does not change the flags if cl is zero, therefore, the two sequences are not semantically equivalent if cl = 0.  The theorem prover finds this bug, the same bug for ror word ptr and ror byte ptr, and the equivalent bugs for rcr, rcl, rol, shl, shr, and sar.  This is a total of 21 buggy VM handlers.

Similarly, obfuscation can also affect the value of the flags register prior to the execution of the inc and dec instructions.  Consider this deobfuscated sequence:

pop eax
dec dword ptr ss:[esp]
pushfd

inc and dec do not change the value of the carry flag, but add and sub do.  Therefore, obfuscation applied upon the vicinity of the pop eax instruction can destroy the value of the carry flag in these circumstances.  As there are three sizes that these instructions might be applied to, there are 6 bugs of this variety.

The theorem prover also found more subtle bugs.  Consider the following deobfuscated instruction sequence, where esi points to the VM bytecode.

lodsd dword ptr ds:[esi]
sub eax, ebx
xor eax, 7134B21Ah
add eax, 2564E385h
xor ebx, eax
movzx ax, byte ptr ds:[eax]
push ax
 

The program's obfuscator would alter the behavior of this snippet by introducing writes to the stack that were not present in the original version, therefore the state of the stack after execution of the obfuscated and non-obfuscated sequences would differ.  The memory read on the second-to-last line might therefore target the area below the stack pointer, which would cause it to read a different value in the obfuscated and deobfuscated world.  This bug is unlikely to manifest itself in the obfuscation of a real-world program, although it demonstrates the ruthless efficacy of theorem proving towards this problem:  the ability to discover tricky situations like this one by considering all possible concrete behaviors of the individual snippets, and generate countermodels for inequal scenarios, no matter how far-fetched.

When taking these factors into consideration, I am able to say that my deobfuscator is correct modulo the bugs in the original obfuscator, which demonstrably number at least 33 (or about 20% of the total handlers).

Control Flow Deobfuscation via Abstract Interpretation

Work done May 30th, 2010.  Originally published on July 9th, 2011 on OpenRCE.

I present some work that I did involving automatic deobfuscation of obfuscated control flow constructs with abstract interpretation.  Considering the image below, this project is responsible for taking graphs like the one on the left (where most of the "conditional" branches actually only go in one direction and are only present to thwart static analysis) and converting them into graphs like the one on the right.

Much work on deobfuscation relies on pattern-matching at least to some extent; I have coded such tools myself.  I have some distaste for such methods, since they stop working when the patterns change (they are "syntactic").  I prefer to code my deobfuscation tools as generically ("semantically") as possible, such that they capture innate properties of the obfuscation method in question, rather than hard-coding individual instances of the obfuscation.

The slides present a technique based on abstract interpretation, a form of static program analysis, for deobfuscating control flow transfers.  I translate the x86 code into a different ("intermediate") language, and then perform an analysis based on three-valued logic over the translated code.  The end result is that certain classes of opaque predicates (conditional jumps that are either always taken or always not taken) are detected and resolved.  I have successfully used this technique to break several protections making use of similar obfuscation techniques.  

Although I invented and implemented these techniques independently, given the wealth of work in program analysis, it wouldn't surprise me to learn that the particular technique has been previously invented.  Proper references are appreciated.

Code is also included.  The source relies upon my Pandemic program analysis framework, which is not publicly available.  Hence, the code is for educational purposes only.  Nonetheless, I believe it is one of very few examples of publicly-available source code involving abstract interpretation on binaries.

PPTX presentation, OCaml source code (for educational purposes only -- does not include my framework.)

PatchDiff2 Analysis and Decompilation

Originally published June 10th, 2010 on OpenRCE

Now that PatchDiff2 is open-source, I release my IDB and the initial decompilation that I did.  You can find it here.

I met the author, Nicolas Pouvesle, at RECon 2008, who told me of his upcoming plans to release this plugin.  He mentioned that the license would be friendly towards reverse engineering, so I asked him if I could decompile the plugin and release the source code.  We must have miscommunicated, because I could have sworn he gave me the green light.  

When it was released, I spent about three days reverse engineering and decompiling it, resulting in the workproduct linked above.  I had intended to spend an extra couple of days on the decompilation to make sure it was functionally equivalent, if not byte-perfect (which is always the ultimate goal).

After I finished the initial phase of the decompilation, I sent it over to Nicolas to solicit his feedback.  He informed me that releasing the source code would violate PatchDiff2's EULA.  Therefore, I abandoned the project.  As it stands, I never even tried to compile the source code, so I'm afraid it's not worth much beyond the mere curiosity.  Still, I'm releasing this hoping that somebody might find it interesting.  The IDB itself is very thorough, e.g. all structures are recovered.

Enjoy.

Compiler Optimizations for Reverse Engineers

Originally written Q1 2007 as part of my Static Reverse Engineering Training Class, first published March 8th, 2010 on OpenRCE.

I've decided to release the part of my training material relating to compiler optimizations.  I created this back in January of 2007; for a while I was teaching classes very often, and so it made sense to keep it private.  Nowadays I only teach a few classes a year, and so this presentation is sort of languishing away on my hard drive, which is a shame since it's my favorite part.  I think people will enjoy reading it, so I have decided to make it public.


Since I made this in early 2007, it lacks some of GCC 4's optimizations, and from time to time I realize that I forgot an optimization or two.  But for the most part, it's fairly complete.  If you have any specific suggestions for optimizations that I missed, please either email me or respond via comment with a link to a binary exhibiting said optimization and the address at which I can find it.  Proper compiler-theoretic names for the optimizations, if applicable, are also appreciated.

Here it is.  Enjoy.

C-subset Compiler in OCaml

Originally published on December 25th, 2009 on OpenRCE

Here is the source code for a compiler that I wrote in Objective Caml this semester, for a subset of the C language.  It requires a standalone C->IR translator which is not included in this release, as the school owns the copyright on that particular piece of code.  Hence one cannot immediately use this compiler to compile C programs without writing a C front end; anyway, an existing compiler such as MSVC or GCC would be a better choice.

The portion of the code that I wrote (everything except bitv.ml and .mli) totals roughly 3200 lines of code.  It includes two optimizations based on classical data-flow analysis, constant propagation and dead-statement elimination.  It also supports translation into and out of static single assignment form, as well as two optimizations based on SSA:  constant propagation and loop-invariant code motion.  The code for the graph-coloring register allocator is not included.  As a back-end, the compiler produces C code that can be compiled by any other C compiler.

The code is a pretty good example of how to structure medium-sized programs in functional programming languages.  I tried to adopt a pure functional style throughout most of the codebase.  Sometimes this failed:  cfg_ir.ml is unnecessarily ugly, and should have been re-written in an imperative style with mutability; also, I made the mistake of using a mutable array to describe Phi values in static single assignment whereas pure functional style would have dictated a list.  But those are my only complaints with the code; overall, I'm pretty pleased with how it all turned out.

This code is substantially more sophisticated than the compiler that I wrote to break VMProtect, so if you can read and understand this release, you should be in good shape for breaking virtualization obfuscators.

Switch as Binary Search, Part 1

Originally published on November 28th, 2008 on OpenRCE

(Continued from part 0)

We have seen how a compiler-generated binary search partitions the range of integers into successively smaller intervals and ultimately converging upon either a single value or one contiguous range of values.  We will now develop a tool to deal with this construct in a friendly fashion for the working reverse engineer.  

The tool has the following high-level specification:

Given the first address of a compiled binary switch construct:

  • Determine the register used and whether the comparisons are signed (trivial)
  • Determine all terminal labels, at which cases reside, and all values that lead to these cases.

A discussion of the problem and its solution follows.

Upon entering the switch, the register value is entirely unconstrained:  the range of values that it might have are contained in the interval [0, MAX_INT] (or [-(MAX_INT+1)/2, MAX_INT/2] for signed integers).  The following example uses an unsigned integer.

Suppose that the first comparison is of the form

@loc0:
cmp eax, val1
jbe @loc1
@loc2:

If the jump is taken, the value must be below or equal to 'val1'.  In other words, it lies in the range [0, val1].  If the jump is not taken, the value must be above 'val1', so it lies in the range [val1+1, MAX_INT].  Therefore, each comparison in the tree partitions the range of possible values into two disjoint ranges:  one for those values where the jump is taken, and one for those where it is not.

At the second level of the tree, there will be two comparisons:  one for the case where the jump for the first was not taken, and one for the case where it was.  Consider the second set of such instructions:

@loc1:
cmp eax, val2
jbe @loc3
@loc4:

@loc2:
cmp eax, val3
jbe @loc5
@loc6:

Each of these cases further constrains the input:

  • The range of values leading to loc3 is [0,         val2]
  • The range of values leading to loc4 is [val2+1,    val1]
  • The range of values leading to loc5 is [val1+1,    val3]
  • The range of values leading to loc6 is [val3+1, MAX_INT]

This table has a very regular structure, and it should not be too hard to imagine what it would look like for three levels into the tree, or four, or...  The following image summarizes the process.  The unique path to a given vertex specifies the constraints required for input to reach it.

As we walk the comparisons in the tree in this fashion, the binary tree will eventually stop and give way to the code for the cases in the switch.  At this point, our constraints will be terminal cases of either single values (most commonly) or of simple ranges.  For each terminal address, we maintain a dictionary associating it with the corresponding ranges that lead there.

The following pseudocode codifies the discussion above.

// The first range returned is that for which the jump is taken;
// the second is for non-jump-taking values
partition(ea, low, high, compared)
{
  if(comparison at ea is ">")
    return [compared+1, high], [low, compared]

  if(comparison at ea is ">=")
    return [compared, high], [low, compared+1]

  if(comparison at ea is "<")
    return [low, compared-1], [compared, high]

  if(comparison at ea is "<=")
    return [low, compared], [compared+1, high]

  if(comparison at ea is "==")
    return [compared, compared], [low, high]

  if(comparison at ea is "!=")
    return [low, high], [compared, compared]
}

The following recursive algorithm solves the general problem.

analyze_bswitch(ea_t ea, int low, int high, int compared)
{
  if(ea is cmp reg, constant)
    compared = instruction's immediate value 
    ea = address of next instruction

  if(ea is a conditional jump)
    [low1,high2], [low2,high2] = partition(ea, low, high, compared)
    analyze_bswitch(jump taken ea, low1, high1, compared)
    analyze_bswitch(jump not taken ea, low2, high2, compared)

  // Instruction is a leaf in the binary tree
  else
    associate(ea, low, high)
}

IDAPython-1.0 compatible source code is available here.

The resulting disassembly is properly annotated with case labels, as IDA does normally:

AUTO:0046348E   jbe     loc_463D16      ; case 0A0h
AUTO:00463494   cmp     eax, 0A2h
AUTO:00463499   jb      loc_462FA0      ; case 0837F81BAh, 0837F81D8h, 0A1h, 091h
AUTO:0046349F   ja      loc_463D21      ; case 0837F90BAh, 0A3h
AUTO:004634A5 loc_4634A5:               ; CODE XREF: sub_462120:loc_462EDAj
AUTO:004634A5                           ; sub_462120+DDDj ...
AUTO:004634A5   push    ebx             ; case 0837F8106h, 0837F8124h, 0A2h, 031h
AUTO:004634A6   call    sub_45C630
AUTO:004634AB   jmp     loc_462217

Switch as Binary Search, Part 0

Originally posted on OpenRCE on November 28th, 2008

For a standard switch with a contiguous region of cases, as in the below, compilers generate constant-time lookups by treating the cases as indexes into an array of pointers.

switch(x)
{
  case 10: /* case 10 code */ break;
  // No case 11 (default)
  case 12: /* case 12 code */ break;
  case 13: /* case 13 code */ break;
  case 14: /* case 14 code */ break;
  // No case 15 (default)
  case 16: /* case 16 code */ break;
  default: /* default code */ break;
}

This might compile into the following:

sub eax, 10 
cmp eax, 6 
ja @default 
jmp dword ptr switch_table[eax*4] 

switch_table dd offset loc_case0
             dd offset default
             dd offset loc_case2
             dd offset loc_case3
             dd offset loc_case4
             dd offset default
             dd offset loc_case6
             ...

For switches with multiple labels pointing to the same code, some compilers save space by generating doubly-indexed, tabular code.

switch(x)
{
  case 0x00..0x20: /* 0x00 <= x < 0x20 code */ break;
  case 0x21..0x40: /* 0x21 <= x < 0x40 code */ break;
}

This might compile to:

cmp eax, 40h 
ja @over 
movzx eax, byte ptr index_table[eax*4] 
jmp dword ptr switch_table[eax*4] ; 
72 bytes instead of 256 
index_table  db 32 DUP(0)
             db 32 DUP(1) 
switch_table dd offset loc_case_00_00
             dd offset loc_case_20_40

For switches with non-contiguous, sparsely-distributed cases like the below, the table-based approaches from above are unsuitable, and yet cases like this do appear in practice, so the compiler must have a strategy for dealing with them.

switch(x)
{
  case 0x0:
  case 0x16:
  case 0x326:
  case 0x9821:
  case 0x90826:
  case 0x278946:
  case 0x4578939:
  case 0x12372826:
  default:
}

One obvious solution to this problem would be to generate a sequence of comparisons, one for each case, starting from the lowest case and ending with the highest.  This would work, but the lookup would be O(N) in the number of case labels.  An equally obvious solution, and one that was mentioned in the book "Reversing", is to generate a binary search construct in the generated code to perform lookups in O(log(N)) time.


To briefly review binary searching, consider the (necessarily) sorted sequence [1;2;3;4;5;6;7;8;9], and consider finding the value 2.  We begin by comparing against the middle element, 5. Since 2 is lesser, we discard all values 5 and above and consider those below it.  Now we have a smaller range of values upon which we can perform the same procedure.

[1;2;3;4]

As before, we compare against the middle element, 3.  Since it is lesser, we can discard anything above 3, leaving [1;2] as the remaining search space.

[1;2]

The middle element is 2, which is our search key, so we stop.  This process took three steps (log(9)) to complete, compared with N=9 steps for searching the whole array.

The compiler is responsible for generating code that implements these comparisons.  The first comparison will be against the middle element in the collection; whether the case value is above or below determines whether to repeat the process for the integers above or below the middle one.  At each comparison there is a corresponding equality test to see whether the search key is the same as the comparator.

Below is an example of this construct in the wild.

AUTO:00462141  cmp  eax, 0E3h 
AUTO:00462146  jnb  loc_46220F ; see below 
AUTO:0046214C  cmp  eax, 73h 
AUTO:0046214F  jnb  loc_463131 
AUTO:00462155  cmp  eax, 3Bh 
AUTO:00462158  jnb  loc_463606 
AUTO:0046215E  cmp  eax, 1Fh 
AUTO:00462161  jnb  loc_463835 
AUTO:00462167  cmp  eax, 10h 
AUTO:0046216A  jnb  loc_463948 
AUTO:00462170  cmp  eax, 8 
AUTO:00462173  jnb  loc_4639D1 
AUTO:00462179  cmp  eax, 4 
AUTO:0046217C  jnb  loc_463A1A 
AUTO:00462182  cmp  eax, 2 
AUTO:00462185  jnb  loc_463A2E  
AUTO:0046220F  ja   loc_462257 
AUTO:00462211  push ebx             ; case 0E3h 
AUTO:00462212  call sub_460920

Hex-Rays does a nice job of illustrating the time-consuming ugly confusingness of dealing with code like this:

if ( v7 <= 0x837FDF02 )
  goto LABEL_755;
if ( v7 >= 0x837FE22C )
{
  if ( v7 <= 0x837FE22C )
    return sub_45EA80(v4);
  if ( v7 < 0x837FE358 )
  {
    if ( 2088770818 != v5 )
      goto LABEL_10;
    goto LABEL_97;
  }
  if ( v7 <= 0x837FE358 )
    goto LABEL_750;
  if ( 2088770608 != v5 )
    goto LABEL_10;
  goto LABEL_100;
}
if ( v7 < 0x837FE0E2 )
  goto LABEL_10;
if ( v7 <= 0x837FE0E2 )
  goto LABEL_535;
if ( 2088771118 == v5 )
{
  sub_460880(v4);
  goto LABEL_23;
}

This entry is continued in part 1.