Iptables_Semantics
Iptables_Semantics copied to clipboard
diekmann
Verified iptables Firewall Ruleset Analysis
This PR corrects misspellings identified by the [check-spelling action](https://github.com/marketplace/actions/check-spelling). The misspellings have been reported at https://github.com/jsoref/Iptables_Semantics/commit/4e47dd8199b05da0a171b5ded631a2dacaa0170b#commitcomment-58472241 The action reports that the changes in this PR would make it happy: https://github.com/jsoref/Iptables_Semantics/commit/613b3168d5569f5ea71cecd455a817be8b43f14c...
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...
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...
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...
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...
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...
- 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 :-)...
This feature requires - Semantics for nftables - Verified translation of iptables nftables - A parser for nftables Will be implemented on by ongy.
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 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...