Hacker News Reader

Comment by xtacy | Hacker News Reader

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.

Reply on news.ycombinator.com