OpenRCE

About Articles Book Store Distributed RCE Downloads Event Calendar Forums Live Discussion Reference Library RSS Feeds Search Store Users What's New

Customize Theme

Flag: Tornado! Hurricane!

Created: Thursday, June 10 2010 15:17.00 CDT

Direct Link, View / Make / Edit Comments

PatchDiff2 Analysis and Decompilation

Author:

RolfRolles

# Views: 2039

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.

Created: Monday, March 8 2010 15:45.22 CST

Direct Link, View / Make / Edit Comments

Compiler Optimizations for Reverse Engineers

Author:

RolfRolles

# Views: 7869

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.

Created: Friday, December 25 2009 13:45.13 CST

Direct Link, View / Make / Edit Comments

Code release: C-subset compiler in Objective Caml

Author:

RolfRolles

# Views: 3721

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.

Created: Friday, December 4 2009 01:41.32 CST Modified: Friday, December 4 2009 01:57.35 CST

Direct Link, View / Make / Edit Comments

VinE's OCaml Programming Tricks: Explicit Continuation-Passing Style

Author:

RolfRolles

# Views: 4446

There are many books devoted to languages like C++ or Python, and technical blogs are teeming with further information on these subjects.  Languages like OCaml have much smaller communities, with very few dedicated books and technical blogs.  As far as I've put together, we OCaml programmers mainly learn from reading one anothers' code.  Functional programmers must stick together.

VinE is the static analysis component of the BitBlaze binary analysis project, it is written in OCaml, and it contains some tricks that I haven't seen elsewhere.  For the sake of contributing to their dissemination throughout the community, I would like to detail some of them here.  These might be obvious to everyone already, or maybe no one cares.  Feedback is welcome.

The following discussion concerns /ocaml/wp.ml, the weakest precondition calculator.  A weakest precondition (hereinafter WP) is the most general condition under which execution reaches some given point with some desired post-condition (i.e. an execution trace plus some arbitrary condition that must hold at the end of the trace, e.g. "this array write at this location goes out of bounds").  WPs compare favorably to forward symbolic execution in terms of formula size, and comprise an attractive choice for enacting the primitive "cause execution to reach a particular line in a particular state", if loop unrolling is palatable.  This entry concerns an OCaml programming technique found in VinE's WP calculator, and does not seek to discuss WPs themselves.  For further reading, read a book on formal semantics (the section on axiomatic semantics) or Dijkstra's original work in the area from the early 1970s.

One issue with functional programming is that, if recursive functions are not written in a tail-recursive style, they have the potential to overflow the stack, thereby causing the program to abort.  One learns to be judicious about writing tail-recursive functions, but alas, it is impossible to naively convert some functions into such a form; care is needed.  For example, if the recursive function needs to call itself to produce a value, and then perform some operation on the result before returning it, then the recursive invocation is not in the tail position and cannot be optimized into a jump by the compiler.  Therefore, the function will consume stack space for each recursive invocation, leading to an upper bound on the size of the data that can be processed before a stack overflow exception is thrown.

Consider the following snippet, which is the aforementioned weakest precondition calculator written as a straightforward recursive pattern match:

  let rec wp q = function

    | Skip           -> q

    | Assume e       -> exp_implies e q

    | Choice(s1, s2) -> let r1 = wp q s2 in

                        let r2 = wp q s1 in

                        exp_and r1 r2

    | Seq(s1, s2)    -> let r1 = wp q s2 in

                        wp r1 s1

    | Assign(t, e)   -> Let(t, e, q)

    | Assert e       -> exp_and e q

In the case of the Choice statement, the weakest precondition for both choices (variables r1 and r2) must be calculated before they can be conjoined, and therefore these calls can not be made tail-recursive. Seq is similar. How do we write this function so it does not crash in the presence of large data sets?

One answer is "explicit continuation-passing style", as seen in the following snippet:

let calculate_wp (simp:Gcl.exp->Gcl.exp) (post:Gcl.exp) (stmt:Gcl.t)  =

  let rec wp q s k =

    match s with

    | Skip           -> k q

    | Assume e       -> k (simp(exp_implies e q))

    | Choice(s1, s2) -> wp q s1 (fun x -> wp q s2 (fun y -> k(simp(exp_and x y ))))

    | Seq(s1, s2)    -> wp q s2 (fun x -> wp x s1 k)

    | Assign(t, e)   -> k(simp(Let(t, e, q)))

    | Assert e       -> k (simp(exp_and e q))

  in

    wp post stmt (fun x->x)

We have introduced a new argument to wp called "k", the "continuation", which means "the rest of the computation". We can see that the calls to wp in the Choice and Seq cases are now in the tail position, and hence can be optimized directly into jumps, resulting in constant stack depth and no more crashes. The cases other than Choice and Seq have been modified to apply the continuation to the result of their portion of the weakest precondition calculation.

But what exactly is going on here? The compact representation yields little insight into how the WP is actually calculated step-by-step. Thus, let's take a look at an example GCL statement and the computation of its WP:

wp q Seq(Skip,Seq(Assume expr1,Assert expr2)) (fun x -> x) (* Initial call to wp with arbitrary post-condition q *)



wp q (Seq(Assume expr1,Assert expr2)) (fun x -> wp x Skip (fun x->x)) (* Grow the continuation because of the Seq *)



wp q (Assert expr2) (fun x -> wp x (Assume expr1) (fun x -> wp x Skip (fun x->x))) (* Grow the continuation because of the Seq *)



(fun x -> wp x (Assume expr1) (fun x -> wp x Skip (fun x->x))) (exp_and expr2 q) (* Shrink the continuation to process the assert *)



wp (exp_and expr2 q) (Assume expr1) (fun x -> wp x Skip (fun x->x)) (* Process the assume *)



(fun x -> wp x Skip (fun x->x)) (exp_implies expr1 (exp_and expr2 q)) (* Shrink the continuation to because of the assume *)



wp (exp_implies expr1 (exp_and expr2 q)) Skip (fun x->x) (* Process the skip *)



(fun x -> x) (exp_implies expr1 (exp_and expr2 q)) (* Shrink the continuation because of the skip *)



(exp_implies expr1 (exp_and expr2 q)) (* Final WP *)

The first three steps show the expansion of the continuation due to the Seq statements in the input; the rest of the steps show the gradual shrinkining of the continuation by processing the statements inside of the Seq statements. Essentially, we have traded stack space for the activation records of wp for heap space for the continuation, and in the process have produced a tail-recursive function that does not consume stack space.

From here, we pass the propositional formula (a VinE expression) off to a theorem prover and receive an input that causes execution to reach the specified state with the specified condition. However, this is once again beyond the scope of this entry.

Created: Friday, October 9 2009 22:28.46 CDT

Modified: Saturday, October 10 2009 05:24.10 CDT

Direct Link, View / Make / Edit Comments

Structure Recovery as Counter-Example Guided Abstraction Refinement

Author:

RolfRolles

# Views: 5049

Counter-Example Guided Abstraction Refinement (C.E.G.A.R. for short) is one of those brilliant techniques, like abstract interpretation, that is simple to state, and that in principle applies beyond its original application domain (in this case, model checking).  As this blog entry is meant to be an informal exposition of an idea I had, I feel that it is not warranted to set up the necessary formalism to discuss C.E.G.A.R. in precise mathematical terms, but it would be wrong to convey the notion that it is anything other than a mathematical endeavor.

When you're trying to figure something out in a black-box fashion, you probably do something like the following.  You begin by inspecting the data at hand and constructing some sort of model (an "abstraction") that fits it.  Then you acquire more data, and test your model against it.  If new data causes the model to be falsified (that particular data is called a "counterexample"), you must "refine" your model so as to account for it.  This process is iterated until no more counterexamples are found.  Basically, this is C.E.G.A.R. -- you can see that the idea enjoys widespread genericity and more or less applies to any scientific endeavor.  Notice I didn't talk about software or anything in particular in this paragraph; I'm just talking about thinking.

To be more specific, C.E.G.A.R. is an idea in model checking that is very similar to the preceeding paragraph.  Basically, a model (abstraction) is constructed automatically, and standard model-checking techniques are used to verify that the model satifies the specification which has been provided.  If it does not, a counterexample is generated.  You then analyze the original hardware or software system to see if the counterexample falsifies the specification.  If it does, the counterexample is a genuine witness to the fact that the system does not adhere to the specification.  If it does not, then we have a "spurious" counterexample (an indication that our abstraction is deficient), which we use to refine our model accordingly, and then we repeat the process.

Once I learned about C.E.G.A.R., I realized that I already adopted a very similar technique while manually reverse engineering object-oriented applications.  I begin by assuming that there are not any structures in the program at all.  When I encounter an instruction of the form mov reg, [reg+offset], I define a new structure consisting solely of that member, with any bytes below or above that member being considered as undefined.  I then track the structure pointer and repeatedly add members every time I encounter a reference of that form.

In terms of C.E.G.A.R.:

1:  Begin with an empty structure as the model.
2:  Assert that the structure is a valid model of the program's memory accesses with respect to the structure pointer.  Model-check the program under this assumption.
3:  If a reference to an as-yet undefined structure member is found, this is a counter-example which is a witness to the falsity of the notion that the model accurately depicts the structure under consideration.  Therefore, refine the model to incorporate the new structure member, and go to 2.
4:  Output the structure.

I don't mean to imply that this is the way that an automated structure recovery tool should be constructed; I think that an interprocedural version of what Hex-Rays does with global dataflow analysis ought to be sufficient for most purposes.  I'm merely suggesting a mathematically precise way to look at the problem of structure recovery.

Perhaps I'll post an entry about viewing the same problem in terms of the Knaster-Tarski theorem in order theory.

Archived Entries for RolfRolles

Subject	# Views	Created On
InfoSec Institute's RE Course	4332	Sunday, March 15 2009
Switch as Binary Search, Part 1	4196	Friday, November 28 2008
Switch as Binary Search, Part 0	3652	Friday, November 28 2008
Bagle.W IDB	3596	Wednesday, November 5 2008
Part 3: Optimizing and Compiling	6654	Wednesday, August 6 2008
Part 2: Introduction to Optimization	4796	Wednesday, August 6 2008
Part 1: Bytecode and IR	4501	Wednesday, August 6 2008
VMProtect, Part 0: Basics	6396	Wednesday, August 6 2008
Compiler 1, X86 Virtualizer 0	11615	Friday, April 4 2008
Industrial-Grade Binary-Only Profiling and Coverage	3831	Saturday, February 16 2008
Array Indexing Qurik	2089	Wednesday, February 13 2008
SpyShredder Malware Spammed on OpenRCE	2826	Tuesday, February 5 2008
Compiler Optimizations Regarding Structures	2513	Tuesday, January 22 2008
Binary Search in Large-Scale Structure Recovery	1739	Monday, January 21 2008
CommWarrior.B Thorough IDB (ARM/C++)	3011	Thursday, January 3 2008
Weird Code: CCs on the Stack	1709	Tuesday, January 1 2008
T2 2006 VM Analysis	3320	Wednesday, October 10 2007
My Training Class	2558	Monday, August 13 2007
ProcDump Thorough IDB	4477	Friday, June 15 2007
IDA's .IDS Files Part II	3830	Thursday, June 7 2007
IDA's .IDS Files Part I	3992	Thursday, June 7 2007
Ten Years of Reverse Engineering	2668	Wednesday, June 6 2007
Shellcode Analysis	4288	Tuesday, April 3 2007

There are 20,335 total registered users.

Recently Created Topics
Career: Threat Inte...	Jul/30
Career: Security Res...	Jul/30
Library Debugging Pr...	Jul/29
Pydbg attach Vs load?	Jul/29
IDA and MIPS (emulat...	Jul/27
UK Cyber Security ch...	Jul/26
System Service Descr...	Jul/26
LD_PRELOAD Question	Jul/23
Patching Application...	Jul/22
Contract: Research E...	Jul/19

Recent Forum Posts
Pydbg attach Vs load?	aMIr
LD_PRELOAD Question	monarch
LD_PRELOAD Question	justano...
LD_PRELOAD Question	monarch
Patching Application...	hughhan
Patching Application...	jduck
immunity debugger pl...	Malware...
paimei installation ...	wishi
IDA Pro customization	wishi
how to chnage an ins...	ConsoleFx

Recent Blog Entries
	ResearchAviator	Jul/28
Installation procedure for ...
	artemblagodarenko	Jul/27
Common function prototype
	dennis	Jul/24
Dr. Gadget IDAPython plugin
	trufae	Jul/23
radare2 0.5 released
	AmrThabet	Jul/21
Pokas x86 Emulator for Gene...
More ...

Recent Blog Comments
	omeg on:	Jul/29
Windows 7 syscall list
	renzosilv on:	Jul/26
Windows 7 syscall list
	renzosilv on:	Jul/26
Windows 7 syscall list
	Dreg on:	Jul/21
HiperDrop 0.0.1
	djnemo on:	Jul/20
HiperDrop 0.0.1
More ...

Imagery

SoySauce Blueprint
Jun 6, 2008

[+] expand

View Gallery (11) / Submit