Flag: Tornado! Hurricane!

Blogs >> RolfRolles's Blog

Created: Friday, October 9 2009 22:28.46 CDT Modified: Saturday, October 10 2009 05:24.10 CDT
Printer Friendly ...
Structure Recovery as Counter-Example Guided Abstraction Refinement
Author: RolfRolles # Views: 7644

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.


Blog Comments
lallous Posted: Saturday, October 10 2009 05:29.07 CDT
Thanks for sharing Rolf.

This technique is really intuitive, and as you said I also found myself doing the same while reconstructing structures.

fileoffset Posted: Sunday, October 11 2009 04:48.07 CDT
I generally just take a glance at the disassembly and write the structure out in full but this will work too...

melajara Posted: Sunday, October 11 2009 05:22.34 CDT
This reminds me of Popper "Conjectures and refutations", a seminal work in the philosophy of science.

Popper elaborated this 90 years ago ;-)

See e.g. http://www.leonardbeeghley.com/docs/SYG%206125/Popper,%20Science-conjectures%20&%20refutations.pdf

As he said "the criterion of the scientific status of a theory is its falsifiability, or refutability, or testability".

Sounds familiar?

Cheers



Add New Comment
Comment:









There are 30,779 total registered users.


Recently Created Topics
Intel pin in loaded ...
Jun/27
Going to do today wi...
Jun/27
how to create delphi...
Jun/27
enabling menu in a s...
Jun/18
How to get the Image...
Jun/17
OllyDBG Process Term...
Apr/28
Reversing opcode
Apr/24
Question about debbu...
Apr/16
IDA PRO Struct Point...
Apr/15
Problem with ollydbg
Mar/22


Recent Forum Posts
Intel pin in loaded ...
djnemo
OOP_RE tool available?
Bl4ckm4n
OOP_RE tool available?
van7hu
Should binaries be n...
Kolisar
Problem with ollydbg
nullx42
!findtrampoline Immu...
skycrack
looking for a softwa...
raxen
Documenting reversed...
raxen
.orpc section what's...
mbin
Pydbg load() issue
phreak


Recent Blog Entries
oleavr
Jun/25
Build a debugger in 5 minutes

oleavr
Apr/17
frida.re 1.2.0 is out, with...

gareebnavas
Jan/21
Android Malware Analysis

oleavr
Dec/21
frida.github.io: scriptable...

chr1x
Nov/05
!apilookup - Win32 API Func...

More ...


Recent Blog Comments
pedram on:
Dec/21
frida.github.io: scriptable...

capadleman on:
Jun/19
Using NtCreateThreadEx for ...

newlulu on:
Jun/10
Branch tracing and LBR acce...

newlulu on:
Jun/10
Advanced debugging techniques

newlulu on:
Jun/10
2 anti-trace mechanisms spe...

More ...


Imagery
SoySauce Blueprint
Jun 6, 2008

[+] expand

View Gallery (11) / Submit