Research

Current State

I finished my PhD in August 2017 summa cum laude and I will leave TUM in September 2017. This means, I am not offering student theses anymore, and I am the wrong person to ask about upcoming lectures, exams, exercises, and ECTS. Don't hesitate to write me an email if you have any question regarding my research, if you cannot reproduce results, if you cannot find any raw data, or if a proof is failing.

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 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? The answers can be found in my PhD thesis.

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) and "Verified iptables Firewall Analysis" (Networking 2016). 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]

Further Talks (German)

• Verified Firewall Ruleset Verification (1/2) [video]
• Verified Firewall Ruleset Verification (2/2) [video]
• Make Firewalls Verified Again [video]
• Linux Container in Rust [video]