Cornelius Diekmann, M.Sc

Research

Research Interests

• IT & Network Security
• Formal Methods
• Network Management

Formal Methods for Network Security Management

Is it possible in general to enhance network security management with formal methods? Can we come up with a model of and executable code in a theorem prover? Can it be applied to real-world? State-of-the-art theoretical models are (often) too limited to be actually applied while state-of-the art empirical academic prototypes (often) rely on implicit assumptions and only work on the data from the evaluation. Do said methods scale? Are they usable? Can we come up with an automated tool for people without formal background?

Example: Netfilter Iptables Firewall

We are verifying properties of iptables firewall rulesets with the help of the Isabelle interactive proof assistant. The default Linux kernel firewall (netfilter/iptables) is known for its vast amount of features. The project contributes a semantics of the firewall's filtering behavior and presents "Semantics-Preserving Simplification of Real-World Firewall Rule Sets" (Formal Methods 2015). With direct application in the computer network domain, the project contributes an automated, executable algorithm and tool (Haskell, using Isabelle's code generation) for "Certifying Spoofing-Protection of Firewalls" (CNSM 2015). We have evaluated applicability on a large collection of real-world data.

Links

• github.com/diekmann

More Links

• cabin_data_network.pdf
• topos_cabinscenario.tar.gz
• nospoof2015poster.pdf
• verified_iptables_ruleset_poster.pdf
• IFIP NETWORKING 2016: Audience Award - Best OMM Presentation

Talks

• 32. Chaos Communication Congress (32C3) Verified Firewall Ruleset Verification - Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL [video], [slides]