GrAdual sessIoN typEs for pRivacy

The main feature of modern computing system is that they are
structured into multiple nodes and communicate by means of exchanging messages. As they scale, the complexity of such systems is constantly rising, posing a huge problem on how they can be programmed correctly. Privacy is a property that concerns the governance of sensible information. A key feature of being able to control privacy is that of controlling how information flows between nodes such that sensitive data is never revealed to nodes that are not supposed to know about it. Consider, for example, a group of federated message servers distributed over several nodes around the globe. Messages (data) flow between servers, but, since servers may be located in different jurisdictions, they may have to follow different policies, and therefore some data may flow between the servers while other data may not. Given the high complexity of such a system, it is not clear how developers can make sure that such policies are satisfied. A first attempt could be made at the level of the software architecture, using models for describing how sensitive data must flow. However, the problem would still persist at the code level. Therefore, we ask: Is
it possible to provide software programmers with artefacts that allow them to control message privacy in distributed systems? This project attempts to answer this question by implementing a gradual type system for privacy in the main-stream programming language Erlang.