diekmann / iptables_semantics Goto Github PK

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

Title says everything. This shouldn't be too hard, most internals already work on machine words of arbitrary length. Most complicated part will probably be the toString and fromString functions because IPv6 address notation is significantly more complex than IPv4 dotted-decimal. Yes, we also want this to be formally verified :-)

Wouldn't it be great if this tool also supports the BSD pf firewall?
We need:

• a BSD pf semantics
• a parser
• a translation to a simplified firewall model so we can reuse our algorithms

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

Example:
8c42c50526a8.txt

In addition: is_iface_char needs '-'

Thanks to @jcaesar for reporting.

TODO: test on both haskell and SML, emit suitable error messages.

• Telnet, X11, NetBIOS from the Internet?
• Outbound any?
• Special-purpose IP addresses?
• ...

Checking for firewall best practices would be a nice enhancement.

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

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)

We can calculate the access control matrix for a fixed service. This answers for example the question "who is allowed to set up ssh connections with whom?".
For this feature, we want to answer the question for any any service: "Who is allowed to set up connections with which services with whom?".

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

This feature requires

• Semantics for nftables
• Verified translation of iptables <-> nftables
• A parser for nftables

Will be implemented on by ongy.

The check for spoofing protection returns false. Can it also provide a counter example? In general, can we provide examples of packets which are accepted/dropped by the firewall?

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

While being harder to administrate than stateful firewalls, stateless firewalls may be faster. This is in particular important if someone is trying to DOS a firewall. Can we translate a stateful ruleset into a stateless ruleset on the fly to withstand the DOS attack? Does this really help?

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

Move the Isabelle/haskellLookAndFeel to its own thy or remove them.

• const
• split

Maybe add it to a HSCompat.thy (Haskell Compatibility) and have const and split qualified?

@jcaesar will take care of this :-)

When talking about filtering behavior, the actions ULOG, NFLOG, and LOG all behave equally: They only log (somehow) and do not influence the filtering behavior. The parser (tokenizer) should recognize them all as just LOG.

At the moment, the tool refuses analysis because it does not know the actions NFLOG and ULOG.

This needs to implemented both in the SML parser and the haskell tool. The parser tester needs test cases for this.

Over the last releases, the performance both of the Isabelle tests and the Haskell tool declined. My guess: this is related to the upcoming support of IPv6. In general, since we support IP addresses as machine words of arbitrary (but fixed) length, performance declined.

It would be interested to profile and inspect the generated Haskell code in detail. I guess there are also many performance issues nor related to the machine word implementation. Next, hot sports with poorly performing of inefficient code need to be tuned. Of course, we want to prove that the new and efficient code computes exactly the same things as the old code. Isabelle, here we come :-)

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

Typing
./dist/build/iptables/iptables [tab][tab]
does not attempt to auto-complete filenames.
Shell: bash
System: Ubuntu
Bug caused by: Programmable bash completion

Bug description: the executable is called iptables. Because of the programmable completion feature of bash, the shell thinks I'm using /sbin/iptables which does not need a file as argument. Consequently, it will not auto-complete file names and paths.

Fix: rename binary.

New name: fffuu -- Fancy Formal Firewall Universal Understander

A semantics for OpenFlow flow table entries and packet processing and a translation from iptables to those flow tables.

Currently being worked on by @jcaesar .
https://github.com/jcaesar/Iptables_Semantics/tree/openflow/thy/OpenFlow

On master, generating haskell_tool/lib/Network/IPTables/Generated.hs from Isabelle and then using that to compile breaks.

Most likely broken since cc2ffef.

Besides source (--sports) or destination ports (--dports) multiport exstenion also has --ports option (match either the source or destination ports).

http://ipset.netfilter.org/iptables-extensions.man.html#lbBM

It would be great if you could add it to the parser.

Make it easier for regular users to obtain fffuu.

Distribute binaries. Pre-compiled and statically linked such that they can just be run on most Linux systems. We don't want to force the user to install cabal and ghc just to use fffuu (since we need quite recent versions of them; only pretty old versions of them are shipped with most stable branches of Linux distributions).

About trust: Paranoid user can build from source. A user who accepts binaries in general probably doesn't want to run an arbitrary binary (which is hosted in the cloud). Let's assume a user trusts our github page. Then we can add the sha256sum of the binary to our github. Github uses https, so the sha256 is transmitted somewhat securely.

Q: How can we always get the latest build (of master) to the github homepage? Automatically?
Q: How can we get the sha256 sum of the binary to github. In particular, if we will build somewhere in the cloud?

Currently, the service matrices (build_ip_partition_pretty) are just dumped as plain text. They could be perfectly visualized as graph. My idea: dump them as dot and run graphviz afterwards.

Code can also be added to the isabelle theories to prepare the output.

We want a fully verified converter that translates rulestes from your proprietary firewall to an open source firewall. This needs:

• A semantics for the proprietary firewall
• A verified translation algorithm
• Integration with our haskell tool

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

The semantics and the analysis algorithms do not support packet modification. Consequently, this tool is mainly applicable for the iptables filter table. It would be nice to add support for packet modification, for example NAT.
This would automatically add support for the other iptables tables: raw, mangle, nat, ...

My idea would be to add an outer semantics: The outer semantics calls the (inner) semantics (the one we have: without packet modification) until a rule which modifies the packet occurs. Then the packet is modified and the inner semantics is called again with the modified packet. This should match pretty much the model of several tables used by iptables.

Hopefully, the outer (wrapper) semantics enables reuse of all existing analysis algorithms we already have without the need to modify them.

Pull requests welcome :-)

Interested? I am happy to help. Send me an email: http://www.net.in.tum.de/de/mitarbeiter/diekmann/

This feature can also be implemented as part of a thesis or interdisciplinary project at Technische Universität München.

Probably a user does not want to write the ipassmt by hand.

• Can we infer the ipassmt from a routing table dump? That is what rp_filter does.
• Can we validate an ipassmt using the routing dump and vice versa?
• Can we visualize the routing relation?
• Can we do the same we are doing in Interface_Replace.thy (for input interfaces) also for output interfaces using a routing table?

I'm hoping for a pull request by @jcaesar :-)

The fffuu Haskell tool fails with the error message "undefined" if some precondition of the Isabelle-generated code does not hold. For example, Isabelle assumes that an ipassmt does not have wildcard interface names in it. For safety reasons, the Isabelle-generated code checks preconditions at runtime. If it fails, it just aborts with "undefined". There are many different cases how this undefined can be triggered. It is almost impossible to debug which "undefined" triggered. Feature request: human-readable error messages for each undefined!