We live in a network-centric world, where communication supported by robust an reliable network systems is of real importance. Malfunctioning of network systems can lead to costly losses and even endanger lives. For an example, in 2012, the Google server crashed for 40 minutes which, in turn, caused Gmail and Chrome to crash all around the world, leaving millions of users without access to their data. Troubleshooting the issue and identifying the root cause of the event revealed a faulty load balancing configuration which was eventually fixed.

In FMT, we work on projects addressing similar problems, and on developing rigorous methodologies for modeling and analysing causes of anomalous behaviours in software defined networks (SDNs). SDNs are characterised by their simplicity in network management and increased network programability, which are key factors in reducing capital expenditure and operating expenses. In short, SDN architectures decouple network control and forwarding functions, enabling the network control to become directly programmable and the underlying infrastructure to be abstracted from applications and network services.

We offer B.Sc. research projects related to the development of programming languages for SDNs and associated analysis frameworks, supported by rigorous mathematical foundations.

AVAILABLE PROJECT PROPOSALS

If you are interested in the general topic of Formal Analysis of SDNs, or if you have your own project idea related to the topic, please contact us directly. Alternatively, you can also work on one of the following concrete project proposals targeting DyNetKAT --our recently developed framework for the formal specification and verification of SDNs:

Visualisation of DyNetKAT models

In this project you will develop an (interactive) editor for state-based models of SDNs programmed in DyNetKAT. Such models can be further exploited in order to identify erroneous network behaviours, and check whether a certain network implementation complies to a set of safety requirements.

Causal Analysis of Safety Violations in DyNetKAT

In this project you will devise a framework for explaining what caused unsafe behaviours of your network, and how such errors could have been avoided. This is a useful tool network developers can use in order to debug and better understand the flaws in their programs.

Learning DyNetKAT Models from Real Data Sets

In this project you will devise a framework for learning formal models of network behaviours. These can be further analysed to ensure safety and reliability of real networks.

SOFTWARE DEFINED NETWORKS

AVAILABLE PROJECT PROPOSALS