Build a model of iptables firewalls and analyze them with Z3
iptables-analyze takes a set of iptables rules and builds a model of them using the python Z3 bindings.
I find it difficult to reason about iptables changes:
- Could the existing set of rules be simplified?
- Are there redundant entries?
- What effect does a change to the rules actually have?
- Are these two sets of rules identical?
Instead we can build a logical model of the set of firewall rules and use Z3 to answer these questions.
Each firewall rule is a set of constraints on the following inputs for IPv4:
- Source IP CIDR (32-bit + mask)
- Source IP Port (16-bit)
- Destionation IP CIDR (32-bit + mask)
- Destionation IP Port (16-bit)
- Protocol (8-bit)
TODO: describe output as a state machine that connects chains
TODO: describe "default drop, first match" semantics.
iptables can be modeled by a function is the conjunction of each rule -- i.e. each set of constrained input tuples are short-circuit boolean OR'd together.
With this model we can:
- Check if a specific connection should be accepted or rejected
- Check if a two models of different firewalls are equivalent and if the aren't provide counter-examples
- Check if a model meets specific constraints on rules
- Initial hacker news comment that described a system like this
- Microsoft whitepaper that described a system like this - Automated Analysis and Debugging of Network Connectivity Policies
- Z3 - a tutorial
- Z3 API in Python
- Fill out this README
- Link to original Azure whitepaper
- Pull apart functionality to separte files and functions
- Add basic sanity tests
- Build out iptables rules parser
- Build out usecases
- Check a single connection against a model
- Check static contracts against a model
- Check two models for equivalence
- Simplify an existing model
- Check connectivity with multiple models