Cornelius Diekmann, M.Sc

Research Associate
Image 50e0559c

Postal address

  • Institut für Informatik der
  • Technischen Universität München
  • Lehrstuhl I8
  • Boltzmannstr. 3
  • 85748 Garching bei München - Germany

Contact

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.

Talks

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

Teaching

Publications

2017.06 Marcel von Maltitz, Cornelius Diekmann, Georg Carle, “Privacy Assessment using Static Taint Analysis (Tool Paper),” in FORTE – 37th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems, Neuchatel, Switzerland, Jun. 2017. to appear soon [Preprint] [Sourcecode] [Rawdata] [Bib]
2016.11 Marcel von Maltitz, Cornelius Diekmann, Georg Carle, “Taint Analysis for System-Wide Privacy Audits: A Framework and Real-World Case Studies.” 1st Workshop for Formal Methods on Privacy, Nov-2016. workshop without proceedings [Preprint] [Sourcecode] [Rawdata] [Bib]
2016.10 Julius Michaelis, Cornelius Diekmann, “LOFT – Verified Migration of Linux Firewalls to SDN,” Archive of Formal Proofs, Oct. 2016. Formal proof development [Url] [Bib]
2016.09 Cornelius Diekmann, Lars Hupel, “Iptables_Semantics,” Archive of Formal Proofs, Sep. 2016. Formal proof development [Url] [Bib]
2016.08 Julius Michaelis, Cornelius Diekmann, “Routing,” Archive of Formal Proofs, Aug. 2016. Formal proof development [Url] [Bib]
2016.08 Cornelius Diekmann, Julius Michaelis, Max Haslbeck, “Simple Firewall,” Archive of Formal Proofs, Aug. 2016. Formal proof development [Url] [Bib]
2016.06 Cornelius Diekmann, Julius Michaelis, Lars Hupel, “IP Addresses,” Archive of Formal Proofs, Jun. 2016. Formal proof development [Url] [Bib]
2016.05 Cornelius Diekmann, Julius Michaelis, Maximilian Haslbeck, Georg Carle, “Verified iptables Firewall Analysis,” in IFIP Networking 2016, Vienna, Austria, May 2016. [Url] [Pdf] [Slides] [Sourcecode] [Rawdata] [Bib]
2015.11 Cornelius Diekmann, Lukas Schwaighofer, Georg Carle, “Certifying Spoofing-Protection of Firewalls,” in 11th International Conference on Network and Service Management, CNSM, Barcelona, Spain, Nov. 2015. [Url] [Preprint] [Sourcecode] [Rawdata] [DOI] [Bib]
2015.11 Cornelius Diekmann, Andreas Korsten, Georg Carle, “Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations,” in 2nd International Workshop on Management of SDN and NFV Systems, manSDN/NFV, Barcelona, Spain, Nov. 2015. [Url] [Preprint] [Slides] [Sourcecode] [DOI] [Bib]
2015.06 Cornelius Diekmann, Lars Hupel, Georg Carle, “Semantics-Preserving Simplification of Real-World Firewall Rule Sets,” in 20th International Symposium on Formal Methods, Jun. 2015, pp. 195–212. [Url] [Preprint] [Slides] [Sourcecode] [Rawdata] [DOI] [Bib]
2014.07 Cornelius Diekmann, “Network Security Policy Verification,” Archive of Formal Proofs, Jul. 2014. Formal proof development [Url] [Bib]
2014.06 Cornelius Diekmann, Stephan-A. Posselt, Heiko Niedermayer, Holger Kinkelin, Oliver Hanka, Georg Carle, “Verifying Security Policies using Host Attributes,” in FORTE – 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems, Berlin, Germany, Jun. 2014, vol. 8461, pp. 133–148. [Pdf] [Preprint] [Slides] [Sourcecode] [Rawdata] [DOI] [Bib]
2014.05 Cornelius Diekmann, Lars Hupel, Georg Carle, “Directed Security Policies: A Stateful Network Implementation,” in Engineering Safety and Security Systems, Singapore, May 2014, vol. 150, pp. 20–34. [Url] [Pdf] [Preprint] [Slides] [Sourcecode] [DOI] [Bib]
2013.05 Lothar Braun, Cornelius Diekmann, Nils Kammenhuber, Georg Carle, “Adaptive Load-Aware Sampling for Network Monitoring on Multicore Commodity Hardware,” in IFIP Networking 2013, New York, NY, May 2013. [Url] [Preprint] [Bib]