Project Details
Projekt
Causal Reasoning in NetKAT
Applicant
Dr. Georgiana Caltais
Subject Area
Theoretical Computer Science
Term
from 2018 to 2021
Project identifier
Deutsche Forschungsgemeinschaft (DFG) - Project number 398056821
The current project aims at developing a methodology for integrating a “causal” formal framework based on counterfactual reasoning, within the context of software-defined networks (SDN’s). SDN’s are a major trend in industry, as they lift the level of abstraction above hardware-oriented applications, thus enabling the rapid deployment of new applications and services.We are targeting NetKAT. This is an SDN programming language gaining popularity due to its solid mathematical foundation that facilitates the development of competitive tools for the rigorous analysis of its associated applications. NetKAT reached the right level of maturity to answer interesting questions such as Reachability: “Can host A communicate with host B? Can every host communicate with every other host?”, or Security: “Does all untrusted traffic pass through the intrusion detection system located at C?”. Additionally, this SDN programming language is already applied in practice, as part of the Frenetic suite of network management tools.The successful outcome of the proposed project encompasses a mathematical framework for network debugging: we aim at efficiently reasoning on and explaining what caused failures of NetKAT applications, who is to be blamed and who is responsible for these erroneous behaviours. This paves the way to formalising liability for NetKAT –an important feature from an industrial viewpoint as well–. We consider addressing issues of real-world networks, develop automatic verification tools and relevant benchmarks.The proposed methodology will exploit algebra and coalgebra –two formal frameworks successfully applied for the modelling and efficient analysis of safety-critical systems and, in particular, NetKAT–. The existing (co-)algebraic formal foundation of NetKAT represents the perfect layout for integrating causality and associated reasoning mechanisms. Thus, a timely action is necessary to ensure a pioneering result along this line of research.The efforts in this project will be carried out in close collaboration with prestigious researchers in the field. This will also benefit our research group, and students at the University of Konstanz that can experience working in an international, outstanding setting.
DFG Programme
Research Grants
International Connection
Iceland, Sweden, United Kingdom
