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.
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.
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!
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!