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.
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.
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.
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.
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.
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!
15 comments
[ 2.8 ms ] story [ 42.8 ms ] threadUsually you use hash tables for looking-up unique values.
A less common use of hashing is cryptography.
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!
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.
Just curious: Have you encountered rules that cannot be cast into predicate logic framework in Z3?
On the network firewall rules (at multi-tenant Azure, I presume), what were Z3's runtimes look like?
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.
LoR's blog -> http://thelegendofrandom.com/blog/sample-page
Lena's tuts -> https://tuts4you.com/download.php?list.17
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!