Oh hey, I worked on this a while back. At the end of 2021 I also did work for Teleport extending this same approach and applying it to Role-Based Access Control rules. This was interesting because it exercised Z3's string analysis capabilities, even checking regular expressions for equivalence: <a href="https://ahelwer.ca/post/2022-01-19-z3-rbac/" rel="nofollow">https://ahelwer.ca/post/2022-01-19-z3-rbac/</a><p>People get intimidated by the terms SMT or theorem prover but I want to emphasize this is actually a really simple process. Any time you have two sets of logical rules (often found in access control systems) you want to compare, translating them into Z3 is really quite easy. There are Z3 bindings in lots of languages, I used Python for the Teleport work: <a href="https://github.com/gravitational/rbac-linter">https://github.com/gravitational/rbac-linter</a><p>My friends and I have also used Z3 to solve various math puzzles. It's useful for checking whether a solution exists when you start modifying the puzzle to see how far you can push it. We used it for this puzzle, for example: <a href="https://www.nsa.gov/Press-Room/News-Highlights/Article/Article/1627320/august-puzzle-periodical-50-for-all/" rel="nofollow">https://www.nsa.gov/Press-Room/News-Highlights/Article/Artic...</a>
Stupid question: isn’t this actually a “simple” problem for which something like Z3 is in some sense overkill?<p>Firewall rules are just a binary colouring of the 4D volume defined by the four-touples of all possible flows. (Two addresses, two ports)<p>Because of the way rules are typically defined this is a very sparse set with huge consistent rectilinear areas.<p>A brute-force solution might be to simply build the 4D equivalent of a quad tree, optionally with splits at the optimal boundaries instead of at “halves”. Then the equivalence check is just a set “xor” operation. That will also reveal examples that are treated inconsistently.<p>Such a tree could represent any reasonable set of rules in surprisingly small amounts of memory. Also, it’s a good way to find “equivalent but more efficient” rules by <i>reversing</i> the process. Adjacent areas that make larger contiguous rectilinear areas can be merged fairly easily in the tree and then written out as the equivalent rule.<p>I’m not entirely pulling this out of a hat, I did something vaguely similar (for a related problem) when analysing complex AWS security groups a few years ago…<p>Similarly I wrote a tool to take a set of arbitrary subnets, union them, and then compute the inverse to “exclude the whole internet except some countries and networks.” I did this with a four-gigabit array in the naive way and it worked great!
Actual code is here: <a href="https://github.com/Z3Prover/FirewallChecker">https://github.com/Z3Prover/FirewallChecker</a><p>Constraint solvers are awesome.
Very cool. Looks similar to the underlying technology in Network Access Analyzer from AWS:<p><a href="https://docs.aws.amazon.com/vpc/latest/network-access-analyzer/how-network-access-analyzer-works.html" rel="nofollow">https://docs.aws.amazon.com/vpc/latest/network-access-analyz...</a>