Authors

Lars Hupel Viktor Kunčak
International Joint Conference on Automated Reasoning (IJCAR), 2016
The final publication is available at Springer Link.

Research Topic & Supplementary Material

Scala

Abstract

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semiautomated tactics. The integration of these two systems allows us to exploit Isabelle’s rich standard library and give greater confidence guarantees in the correctness of analysed programs.

Authors

Cornelius Diekmann Lars Hupel Georg Carle
Formal Methods (FM), 2015
The final publication is available at Springer Link.

Research Topic & Supplementary Material

Network Security

Abstract

The security provided by a firewall for a computer network almost completely depends on the rules it enforces. For over a decade, it has been a well-known and unsolved problem that the quality of many firewall rule sets is insufficient. Therefore, there are many tools to analyze them. However, we found that none of the available tools could handle typical, real-world iptables rulesets. This is due to the complex chain model used by iptables, but also to the vast amount of possible match conditions that occur in real-world firewalls, many of which are not understood by academic and open source tools. In this paper, we provide algorithms to transform firewall rulesets. We reduce the execution model to a simple list model and use ternary logic to abstract over all unknown match conditions. These transformations enable existing tools to understand real-world firewall rules, which we demonstrate on four decently-sized rulesets. Using the Isabelle theorem prover, we formally show that all our algorithms preserve the firewall’s filtering behavior.

Authors

Jasmin Christian Blanchette Lars Hupel Tobias Nipkow Lars Noschinski Dmitriy Traytel
Haskell Symposium, 2014

Abstract

We report on our experience teaching a Haskell-based functional programming course to over 1100 students for two winter terms. The syllabus was organized around selected material from various sources. Throughout the terms, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition and gave away trophies in a award ceremony.