Assume that rules with output interfaces not part of the routing table never match

diekmann / Iptables_Semantics

Verified iptables Firewall Ruleset Analysis

http://iptables.isabelle.systems/

BSD 2-Clause "Simplified" License

96 stars 13 forks source link

Assume that rules with output interfaces not part of the routing table never match #146

Open l-jonas opened 5 months ago

l-jonas commented 5 months ago

This has an effect if a routing table was specified only. The current implementation keeps the interfaces if they are not part of the routing table. Due to the over approximation, this assumes that traffic is allowed while it is not.

This modifieds the generated code which is a bad practice. However, I could not make isabelle generate code at all.