Port numbers belong to a specific protocol

[diekmann]

The following firewall, in the FORWARD chain accepts everything from TCP srcport 22 and UDP dstport 80. It drops everything else.

*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

However, the simple firewall looks as follows:

DROP     all  --  0.0.0.0/0            0.0.0.0/0   sports: 0:21 dports: 0:79
DROP     all  --  0.0.0.0/0            0.0.0.0/0   sports: 0:21 dports: 81:65535
DROP     all  --  0.0.0.0/0            0.0.0.0/0   sports: 23:65535 dports: 0:79
DROP     all  --  0.0.0.0/0            0.0.0.0/0   sports: 23:65535 dports: 81:65535
ACCEPT   all  --  0.0.0.0/0            0.0.0.0/0

This simple firewall accepts everything from srcport 22 to dstport 80, for any protocol! This is because the model allows to consider ports independent from the protocol. When doing algebra on match expressions, it may be possible to construct rules which separate the protocol and the port match. The problem exists already before the simple firewall:

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

Note that the resulting firewall is syntactically invalid since it matches on ports without matching on protocols. This can be easily seen and a validity constraint already exists in the thy for some time.

The fix is that we check for syntactic validity and abort if we cannot handle the firewall. So our tool is still safe to use :-) Check will soon be merged to master. The check in the thy examples has been there all the time.

One fix would be to change the parser to only recognize tcp ports. Then the tool would abstract over udp ports, which is fine (but looses some accuracy). A long term goal would be to have independent fields for tcp and udp ports in the model. (The best model would probably be where the protocol field is enhanced with port numbers)

[diekmann]

Add a primitive_protocol to the Src_Ports and Dst_Ports. They can still be easily negated. Let (tcp ∧ p80) denote the new _Ports datatype with added primitve_protocol.

lemma "¬(tcp ∧ p80) ⟷ ¬tcp ∨ (tcp ∧ ¬ p80)" by simp

Note that negating a ports matches then creates a new (negated) protocol match. This is desired behavior and avoids above issues.

[diekmann]

Work in progress, branch "ports".

TODO: reactivate simple_match_to_ipportiface_match_correct again, this will actually need the simple firewall wellformedness constraint

[diekmann]

Branch ports looks good.

Reactivated missing lemma. Done.

TODO: somehow the port normalization could be better. Now some rulesets got slightly larger

Example:

-   ''-d 131.159.14.111/32 --dpts [21:22] -o vlan96 -p tcp -m state --state NEW --tcp-flags [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST] [TCP_SYN] -j ACCEPT'',
+   ''-d 131.159.14.111/32 --dpts [21] -o vlan96 -p tcp -m state --state NEW --tcp-flags [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST] [TCP_SYN] -j ACCEPT'',
+   ''-d 131.159.14.111/32 --dpts [22] -o vlan96 -p tcp -m state --state NEW --tcp-flags [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST] [TCP_SYN] -j ACCEPT'',

fixed (hopefully)

[diekmann]

Fixed in 69c6042ce6487006b1399f88183e5e4393aaf2f7

TODOs:

• merge to master
• cleanup
• remove (optimize away) impossible matches on protocols. issue #122

[diekmann]

Merged to master in pull request #123 (commit 119159d3bb81873cc38fc0933fe2bc016ce418cc). Bug is gone. Further optimizations (just a feature) got its separate issue.