Solving a Crackme using Z3: Theorem Prover
wiremask.eu
Solving a Crackme using Z3: Theorem Prover
1–10 of 16 posts
Re: Solving a Crackme using Z3: Theorem Prover
#2A hash table lets you look up a word in a dictionary.
Usually you use hash tables for looking-up unique values.
A less common use of hashing is cryptography.
Re: Solving a Crackme using Z3: Theorem Prover
#3Strictly 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.
Re: Solving a Crackme using Z3: Theorem Prover
#4Strictly 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.
Re: Solving a Crackme using Z3: Theorem Prover
#5Here'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!
Re: Solving a Crackme using Z3: Theorem Prover
#6What are some of the good resources to get started with Reverse Engineering?
Re: Solving a Crackme using Z3: Theorem Prover
#7What 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.
Re: Solving a Crackme using Z3: Theorem Prover
#8This 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!
Re: Solving a Crackme using Z3: Theorem Prover
#9Here'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?
Re: Solving a Crackme using Z3: Theorem Prover
#10Here'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.