Prof. Riccardo Sisto

Thesis Proposals

The proposed theses are all related to research activities about the development of distributed systems using formal approaches.
These approaches use sophisticated software development tools that automate a large part of software or system development and that enable the production of high quality (especially in terms of correctness) products. Because of this feature, these techniques are applied especially to software and systems classified as critical (e.g. safety-critical or security-critical). As distributed applications are becoming more and more complex (with many distributed interactions), and pervasive in our daily life, they are also becoming more and more critical. Typical examples are avionics, automotive, industrial, medical, e-commerce, e-banking, e-power, etc. For this reason, the importance of formal techniques in system and software development is constantly increasing. Of course, the networking infrastructures and the middleware used to build distributed critical applications should be themselves reliable and dependable. This is why telecommunication providers and vendors of software for communication infrastructures are also interested in these techniques, especially now that network infrastructures are going to be "softwarized", with massive use of virtualization and data centers.
The research activities these thesis proposals refer to aim to experiment and improve new development tools and new development methodologies.
  1. A framework for Virtual Network Functions (VNF) modeling and Service Graph verification in SDN/Cloud context
  2. Performance monitoring of virtualized networks deployed in data centers
For further information: Prof. Riccardo Sisto (Phone. 011 090 7073, e-mail:

  A framework for Virtual Network Functions (VNF) modeling and Service Graph verification in SDN/Cloud context

The networking panorama is dramatically evolving towards flexible and dynamic virtualization technologies, which allows the deployment of complex network services and functionalities. According to this trend, some functions (firewall, cache, NAT, etc.) that were traditionally deployed by means of static appliances running on dedicated hardware, are now becoming light software images running on commodity hardware that can be managed very easily, thus allowing frequent reconfiguration of network service graphs in a cloud-like environment.

In this context, a key challenge is represented by the need of continuously ensuring (before deploying) that some desired network properties or invariants are always guaranteed, especially in networks where automatic reconfiguration is expected to be triggered very frequently in response to higher-level events (customer requests, administrator actions, etc.). As an example of such properties, a network operator may require that a given network configuration is always loop-free or a customer may want to be sure that all his traffic traverses a firewall for security reasons and so on. Our research group is working at the development of a framework that allows the interested actors to define the behavior of any VNF in a Java-like fashion and allows the extraction of an abstract formal model from the Java code in order to verify the above mentioned network properties. The verification is performed by a third-party general-purpose verification engine. The same model can also be used as a basis for the automatic generation of implementations of the virtual function.

With reference to this framework, which is under development, a number of thesis works are available with different aims, ranging from the experimentation of different verification engines, to the definition of ways for expressing properties that are seamless and intuitive, to the automatic generation of implementation code. For the last point, an option that will be explored is the possibility to generate implementations in the form of eBPF programs running in the Linux kernel and making use of the IOVisor technique.

Performance monitoring of virtualized networks deployed in data centers

Telecommunication providers are currently very interested in allowing the management of Service Level Agreements (SLA) with their internal and external customers. This interest is stimulating research for improving the technical solutions that allow performance monitoring of IP networks.

At the same time, telecommunication providers are progressively moving their infrastructures towards intensive use of Network Function Virtualization (NFV) and data centers. The current trend is to provide services to clients through data centers using this approach.

This thesis proposal is about performance monitoring in virtualized network environments. The final aim is to realize a virtual performance monitoring system that can monitor the performance of the connections among different data centers, each one providing virtualized services. According to this approach, the monitoring system will be itself implemented as a collection of virtual network services hosted in the same data centers that are monitored. As these services are expected to have very high performance and low overhead, they will be developed using a new approach which consists of implementing the virtual monitoring functions as eBPF programs running in the Linux kernel, making use of the IOVisor technique.

The thesis will be done in collaboration with TIM and part of the work will be done in the TIM premises in Turin (TIlab). As TIM is currently creating a number of data centers, the prototype developed in the thesis will be experimented in these data centers. The monitoring algorithm will be based on the PNPM SLA technique (see IETF draft draft-fioccola-ippm-rfc6812-alt-mark-ext), for which a C implementation already exists. This implementation has to be turned into a virtual network function using the approach described above, and deployed in the TIM data centers. Performance and scalability tuning will complete the work.

A prize of 4000 euros may be available if good quality results are achieved.
The thesis is a good opportunity to learn about NFV and to get in touch with TIM.

Last change: March 2017