Improve protocol optimization

[diekmann]

Once the ports have been normalized, new matches on negated protocols may be introduced. We just need an additional round of protocol optimization to remove impossible matches.

Example:

*filter
:INPUT DROP [0:0]
:FORWARD DROP [0:0]
:OUTPUT DROP [0:0]
-A INPUT -p tcp -m multiport ! --dports 80,443,6667,6697 -m hashlimit --hashlimit-above 10/sec --hashlimit-burst 20 --hashlimit-mode srcip --hashlimit-name aflood --hashlimit-srcmask 8 -j ACCEPT
-A INPUT -p udp -m multiport ! --dports 80,443,6667,6697 -m hashlimit --hashlimit-above 10/sec --hashlimit-burst 20 --hashlimit-mode srcip --hashlimit-name aflood --hashlimit-srcmask 8 -j ACCEPT
-A INPUT -p icmp -m hashlimit --hashlimit-above 10/sec --hashlimit-burst 20 --hashlimit-mode srcip --hashlimit-name aflood --hashlimit-srcmask 8 -j ACCEPT
COMMIT

Output:

== unfolded INPUT chain (upper closure) ==
sanity_wf_ruleset passed
(! -p tcp -p tcp, -j ACCEPT)
(-m tcp --dpts [0:79] -p tcp, -j ACCEPT)
(-m tcp --dpts [81:442] -p tcp, -j ACCEPT)
(-m tcp --dpts [444:6666] -p tcp, -j ACCEPT)
(-m tcp --dpts [6668:6696] -p tcp, -j ACCEPT)
(-m tcp --dpts [6698:65535] -p tcp, -j ACCEPT)
(! -p udp -p udp, -j ACCEPT)
(-m udp --dpts [0:79] -p udp, -j ACCEPT)
(-m udp --dpts [81:442] -p udp, -j ACCEPT)
(-m udp --dpts [444:6666] -p udp, -j ACCEPT)
(-m udp --dpts [6668:6696] -p udp, -j ACCEPT)
(-m udp --dpts [6698:65535] -p udp, -j ACCEPT)
(-p icmp, -j ACCEPT)
(, -j DROP)

Do you see the impossible tcp and not tcp match. This rule needs to be gone.

This may be an ideal example to get started ;-) Be warned, you will need to push a lot of invariants through a lot of theorems and functions!

The simple firewall just removes the match on negated protocols and the first rule will match all tcp packets. This is a sound overapproximation but we can do way better (by just removing this rule).

ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    
ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    dports: 0:79
ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    dports: 81:442
ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    dports: 444:6666
ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    dports: 6668:6696
ACCEPT     tcp  --  0.0.0.0/0            0.0.0.0/0    dports: 6698:65535
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    dports: 0:79
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    dports: 81:442
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    dports: 444:6666
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    dports: 6668:6696
ACCEPT     udp  --  0.0.0.0/0            0.0.0.0/0    dports: 6698:65535
ACCEPT     icmp  --  0.0.0.0/0            0.0.0.0/0    
DROP     all  --  0.0.0.0/0            0.0.0.0/0

This is a real-world example: http://serverfault.com/questions/793631/iptables-multiport-and-negation/795234

THIS HAS BEEN FIXED, remaining issue below

[diekmann]

Another example:

*filter
:INPUT ACCEPT [0:0]
:FORWARD ACCEPT [0:0]
:OUTPUT ACCEPT [0:0]
:CHAIN - [0:0]
-A FORWARD -j CHAIN
-A CHAIN -p tcp -m tcp --sport 22 -j RETURN
-A CHAIN -p udp -m udp --dport 80 -j RETURN
-A CHAIN -j DROP
COMMIT

The simple firewall overapproximation gives:

ACCEPT     all  --  0.0.0.0/0            0.0.0.0/0

But we see that we can do better. All the DROPs for protocols can be preserved because the negated protocols apply due to the primitive protocol in the port:

(! -p tcp ! -p udp, -j DROP)
(! -p udp ! -p tcp, -j DROP)
(! -p tcp -m udp --dpts [0:79], -j DROP)
(! -p tcp -m udp --dpts [81:65535], -j DROP)
(! -p udp -m tcp --spts [0:21], -j DROP)
(! -p udp -m tcp --spts [23:65535], -j DROP)
(-m udp --dpts [0:79] -m tcp --spts [0:21], -j DROP)
(-m udp --dpts [81:65535] -m tcp --spts [0:21], -j DROP)
(-m udp --dpts [0:79] -m tcp --spts [23:65535], -j DROP)
(-m udp --dpts [81:65535] -m tcp --spts [23:65535], -j DROP)
(, -j ACCEPT)

[diekmann]

Protocols_Normalize.thy should contain everything that is necessary.

[diekmann]

Fixed in 2eea5dcc4f1b8c33546c72d1673a5c52d93463e5