Solving a Crackme using Z3: Theorem Prover

http://wiremask.eu/hackingweek-2015-reverse-4/

by Wiremask • 11 years ago

78 14 11 years ago

Strictly speaking this problem is more of a "keygenme", since a crackme is usually approached in the "figure out which conditional jump(s) to patch" manner.

Wiremask• 11 years ago

Yes I totally agree, I just kept the file original name.

ahelwer4• 11 years ago

Here's a similar use of Z3 as a keygen:

http://www.slideshare.net/extremecoders/keygenning-using-the...

I've been using Z3 at work for checking firewall properties (will have a blog post up soon) and it's pretty close to magic!

xtacy3• 11 years ago

Interesting! Would love to hear more. What are the classes of firewall properties you can express in Z3?

ahelwer4• 11 years ago

Firewalls are sets of rules which culminate in a decision to accept or block a packet. The rules are easily expressed in predicate logic accepted by Z3. You can do all sorts of neat stuff then; check out https://github.com/Z3Prover/z3/wiki/Publications

Some general examples:

* Does firewall 1 accept a subset of the packets accepted by firewall 2?

* Does firewall 1 accept the same set of packets as firewall 2?

* Does this firewall accept some arbitrary set of packets? (useful for proving implementation of security rules)

* Do any of the firewall rules overlap?

* Do any of the firewall rules conflict?

Z3 will also provide examples or counter-examples to the above true/false questions. I like to think of Z3 as an Oracle. You give it a bunch of statements describing what you're looking for, and it magically spits out an answer.

noobie• 11 years ago

What are some of the good resources to get started with Reverse Engineering?

thoth• 11 years ago

Get used to reading code in a debugger. ;)

There is a great free text, the author asks for a donation: Reverse Engineering for Beginners, http://beginners.re/

The RCE Endeavors blog has many great posts that aren't difficult to follow, http://www.codereversing.com/

CMU's "bomb lab" is pretty famous for providing an executable to play with. Actually I think all the assignments that go along with the CS:APP2e text look very valuable, http://csapp.cs.cmu.edu/2e/labs.html

It's just one of those areas you have to get some hands-on practice doing.

fierycatnet• 11 years ago

Here are some other popular resources for reversing.

LoR's blog -> http://thelegendofrandom.com/blog/sample-page

Lena's tuts -> https://tuts4you.com/download.php?list.17

qqqgg• 11 years ago

This is fascinating, I had no idea such techniques exist.

The last reversing project I worked on was to crack a BIOS setup password that had no obvious method of reset (I could dump the BIOS flash memory but not write to it). Having to write a brute force cracker at the end of such a joyous slog of disassembly, due to having no clue on how to pick apart what appeared to be a reasonably simple hashing function, was really quite disappointing.

I'll have to try it again soon using Z3 to solve. Thanks for such a inspiring blog post!

dennis714• 11 years ago

Couple of other articles about Z3 which may be also interesting: http://yurichev.com/writings/z3_rockey.pdf http://blog.yurichev.com/node/86

Solving a Crackme using Z3: Theorem Prover

Related Stories