Dr. Cornelius Diekmann

Research

Current State

PhD Defense Party

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.

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]

Teaching

Publications

2020-03-01 Cornelius Diekmann, Lars Hupel, “Hello World,” Archive of Formal Proofs, Mar. 2020. Formal proof development [Url] [Bib]
2020-01-01 Cornelius Diekmann, “Encryption is Not Integrity!,” PoC||GTFO: Grab gifts from the genizah, reading every last page! And write in their margins! And give them all again!, vol. 20, no. 08, pp. 62–67, Jan. 2020. Beware, PDF is a 39MB polyglot [Pdf] [Sourcecode] [Bib]
2019-11-01 Cornelius Diekmann, “Looping with Untyped Lambda Calculus in Python and Go,” Paged Out!, vol. 2, p. 22, Nov. 2019. [Url] [Pdf] [Preprint] [Bib]
2018-12-01 Cornelius Diekmann, Johannes Naab, Andreas Korsten, Georg Carle, “Agile Network Access Control in the Container Age,” IEEE Transactions on Network and Service Management, Dec. 2018. [Pdf] [DOI] [Bib]
2018-01-01 Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian Haslbeck, Georg Carle, “Verified iptables Firewall Analysis and Verification,” Journal of Automated Reasoning, Jan. 2018. [Url] [Pdf] [Preprint] [DOI] [Bib]
2017-10-01 Cornelius Diekmann, “Naming Network Interfaces,” PoC||GTFO: Pastor Laphroaig Races the Runtime Relinker and Other True Tales of Cleverness and Craft, vol. 16, no. 08, pp. 45–46, Oct. 2017. Beware, PDF is a 50MB polyglot [Pdf] [Bib]
2017-07-01 Cornelius Diekmann, “Provably Secure Networks: Methodology and Toolset for Configuration Management,” PhD thesis, Technische Universität München, Jul. 2017. [Url] [Pdf] [Preprint] [Slides] [DOI] [Bib]
2017-06-01 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. [Url] [Preprint] [Slides] [Sourcecode] [Rawdata] [Extended version] [DOI] [Bib]
2016-11-01 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-01 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-01 Cornelius Diekmann, Lars Hupel, “Iptables_Semantics,” Archive of Formal Proofs, Sep. 2016. Formal proof development [Url] [Bib]
2016-08-01 Cornelius Diekmann, Julius Michaelis, Max Haslbeck, “Simple Firewall,” Archive of Formal Proofs, Aug. 2016. Formal proof development [Url] [Bib]
2016-08-01 Julius Michaelis, Cornelius Diekmann, “Routing,” Archive of Formal Proofs, Aug. 2016. Formal proof development [Url] [Bib]
2016-06-01 Cornelius Diekmann, Julius Michaelis, Lars Hupel, “IP Addresses,” Archive of Formal Proofs, Jun. 2016. Formal proof development [Url] [Bib]
2016-05-01 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-01 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-11-01 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-06-01 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-01 Cornelius Diekmann, “Network Security Policy Verification,” Archive of Formal Proofs, Jul. 2014. Formal proof development [Url] [Bib]
2014-06-01 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-01 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-01 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] [Pdf] [Preprint] [Sourcecode] [Bib]