[isabelle] Feature: Packet modification

[diekmann]

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.