Solving a Crackme using Z3: Theorem Prover | Hacker News Reader

Solving a Crackme using Z3: Theorem Prover

wiremask.eu

78 pointsWiremask14 comments

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!

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

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.

Thanks for the detailed explanation. It's interesting to note that firewall rules are well captured in the predicate logic.

Just curious: Have you encountered rules that cannot be cast into predicate logic framework in Z3?

I've not. Firewall rules are of the form {predicate} -> {decision}, where {decision} is block/allow and {predicate} defines a set of packets: something like a source address range, source port range, destination address range, destination port range, and protocol. When a packet comes in, the firewall finds all matching predicates (there can be multiple) and makes a block/allow decision. Since checking for packet-predicate matches is done with simple and/or/not formulas, I can't think of a rule which could not be expressed in Z3. Also, this is hardly taxing Z3: it supports reasoning with real numbers and nonlinear constraints.

Thanks again. I didn't know Z3 could handle formulae with real numbers. I will take a closer look at it. :)

On the network firewall rules (at multi-tenant Azure, I presume), what were Z3's runtimes look like?

Z3 was able to check equivalence of firewalls with a few hundred rules in a fraction of a second on a standard workstation. I was extremely impressed, especially since the brute-force IPv4 packet search space is 2^112! There's some wizardry going on beneath the hood.

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.

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

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

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.

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

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!

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

Reply on news.ycombinator.com