What is the project about?
Communication networks have become a critical infrastructure of our digital society. This introduces stringent requirements on dependability.
We envision more automated approaches to operate communication networks, overcoming today's manual and error-prone approach.
We develop a software tool which performs what-if analysis of computer network configurations (especially MPLS and SR networks). That is, checking policy compliance etc. under network failures.
AN AUTOMATA-THEORY APPROACH
Our approach relies on automata theory: network configurations are automatically collected from the routers and transformed into a push-down automaton, together with the invariants that a network should fulfill. Fast reachability analysis allows to provide verification in minutes or even seconds.
The tool hence disburdens network operators from their most complex
tasks, and ensures a high dependability.
AUTOMATION FOR DEPENDABILITY
Use Cases
TESTING POLICY
COMPLIANCE OF
NETWORK
TESTING
REACHABILITY AND
LOOP-FREEDOM
TESTING
WAYPOINT
ENFORCEMENT
Everything under failures
TESTING POLICY COMPLIANCE OF NETWORK:
The tool supports automated what-if analysis of the network policy, answering questions such as:
Does the current network configuration fulfill the network policy?
What happens under failures: is the network configuration policy-compliant even under up to k link failures?
The tool applies to MPLS networks and can be extended to Segment Routing networks.
TESTING REACHABILITY AND LOOP-FREEDOM:
The tool allows to test reachability, answering questions such as:
"is it ensured that A can reach B?" and "is it ensured that A cannot reach C?".
Similarly, the tool allows to answer questions related to loop-freedom:
"is it ensured that packets are never forwarded along loops, even if there are up to k failures?"
Again, the tool currently applies to MPLS networks and can be extended to Segment Routing networks.
TESTING WAYPOINT ENFORCEMENT:
The tool also allows to test properties related to waypoints, such as:
"is it ensured that traffic from A to B never goes through C?" and "is it ensured that traffic from A to B always goes via C (e.g., a firewall)?".
These questions can also be answered in a way which accounts for failures.
Our Team
Peter Gjøl
Jensen
Bernhard Clemens
Schrenk
Stefan
Schmid
Jiri
Srba
Peter Gjøl Jensen
Peter G. Jensen has been reasearching, preaching and teaching formal methods at Aalborg University for several years (since 2012 as a MSc student), most recently in the position of Tenure Track Assistant Professor (2019).
His research focuses on the construction of efficient, applicable tools and algorithms for model-driven disciplines such as verification, synthesis and learning.
Bernhard Clemens Schrenk
Bernhard Schrenk is a professional software developer and student of computer science at the University of Vienna, Austria.
Since 2019 he is working for the communication technologies research group as student researcher and programmer on the next generation of What-If analysis tools.
Stefan Schmid
Stefan Schmid is a Full Professor at the University of Vienna, Austria. MSc and PhD at ETH Zurich, Postdoc at TU Munich and University of Paderborn, Senior Research Scientist at T-Labs in Berlin, and Associate Professor at Aalborg University, Denmark.
Stefan Schmid received the IEEE Communications Society ITC Early Career Award 2016 and an ERC Consolidator Grant 2019.
Read here ZOIS interview with Stefan Schmid.
Jiri Srba
Jiri Srba is a full professor in computer science at Aalborg University. He holds MSc from Faculty of Informatics, Masaryk University in Brno and PhD degree from Aarhus University. Since 2005, he has been employed at Aalborg University.
Jiri Srba is interested in applying formal methods such as model checking into industrial cases from computer networking, supervisory control and wireless adhoc networks.