Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Solving a Crackme using Z3: Theorem Prover

wiremask.eu

Post reply on HN
Print view View original

11–16 of 16 posts

Re: Solving a Crackme using Z3: Theorem Prover

#11

Post by xtacy »

ahelwer wrote: post #10
xtacy wrote: post #9

Earlier quoted context omitted.

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…

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?

Re: Solving a Crackme using Z3: Theorem Prover

#13

Post by ahelwer »

xtacy wrote: post #11
ahelwer wrote: post #10

Earlier quoted context omitted.

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…

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.

Re: Solving a Crackme using Z3: Theorem Prover

#14

Post by xtacy »

ahelwer wrote: post #13
xtacy wrote: post #11

Earlier quoted context omitted.

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-pred…

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?

Re: Solving a Crackme using Z3: Theorem Prover

#15

Post by ahelwer »

xtacy wrote: post #14
ahelwer wrote: post #13

Earlier quoted context omitted.

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-pred…

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.
Post reply on HN