Safe Distributed Programming with Sessions

Distributed (or communicating) systems are collections of autonomous software that realise global tasks through network communication. They play an increasingly important part in both industry and our every-day life as they power the Internet giants that everyone uses such as Google, Facebook or Amazon, as well as the infrastructure of financial and manufacturing companies. Recent advances such as cloud-computing or many-core machines are only broadening the number of critical software systems that are distributed. Distributed programming is different from traditional programming: autonomous programs need to (1) cooperate to achieve their tasks safely, (2) achieve highly complex and interactive behaviours that are hard to program, debug and test, (3) execute in open environments where untrusted agents can interfere. However, existing tools are in general not adapted to this new distributed programming paradigm, since compilers and verification tools are local, and security and networking libraries are very
low-level and do not scale. This situation currently results in very long and hazardous development time and frequent discoveries of
security flaws.

In this context, we are exploring formal (mathematically proven) methods to propose a new programming framework, based on
message-passing, which can achieve global safety and security properties. This project is made possible by several recent advances: first, the development of formal verification tools that are able to handle real programs; second, the invention of protocol specification languages that are designed towards applicability. The goal is to design message-passing abstractions and certified infrastructure components that enable programmers to handle the complexity of distributed programming. The exact project to be undertaken by the student is a matter for discussion, taking into account the student's interests and the feasibility of the project.

The project is suitable for a student with a strong mathematical background, ideally a first-class degree in Computer Science. Some
knowledge of logic and a taste for programming are essential.