The security of modern distributed systems is an important and complex challenge, which has attracted the interest of a growing research community over the last decade. The cryptographic protocols used to securely transmit data over an untrusted network, and even more so their software implementations, are extraordinarily difficult to design and to prove secure, as witnessed by the continuously growing list of discovered vulnerabilities. The complexity of cryptographic systems stem from several factors and has significantly increased over the years. First of all, while early academic protocols mostly consisted of simple combinations of signature and encryption schemes, modern ones rely on much more sophisticated, and arguably fascinating, cryptographic primitives, such as zero-knowledge proofs and secure multiparty computations. Secondly, the security and privacy properties required by modern applications go well beyond the well-understood secrecy and authenticity properties, covering, e.g., indistinguishability relations and differential privacy.

Language-based techniques, and type systems in particular, lived up to the challenge, constituting a solid and expressive framework for the verification and design of cryptographic systems. While early academic cryptographic protocols required relatively simple type and effect systems, modern cryptography called for more powerful techniques, such as refinement types, union and intersection types, linear types, and relational refinements.

The goal of this tutorial is to guide the audience through the literature on type theory for cryptographic applications, giving a consolidated view of the research development in this field and establishing bridges with various subdisciplines of interest to the POPL community (e.g., type theory, SMT solving, linear logic, proof-carrying authorization, relational verification, and concurrent programming), with the final goal of fostering cross-fertilizing research ideas.

This tutorial will consist of two identical sections in order to give as many people as possible the possibility to follow the tutorial.

I studied Computer Science at the University of Venice (Italy), where I received the Laurea in 2002 and the Ph.D. in 2006. In the years 2006-2008, I conducted postdoctoral research at the Information Security and Cryptography group at Saarland University. In the years 2008-2013, I led the Language-Based Security group, which was affiliated with the Cluster of Excellence “Multimodal Computing and Interaction” and, since 2009, supported by the Emmy Noether fellowship by the German Research Foundation. In 2013 I have been appointed associate professor at Saarland University within the Competence Center on IT-Security, Privacy, and Accountability, where I am currently heading the Secure and Privacy-preserving Systems Group.

I am generally interested in the design of cryptographic solutions to protect the privacy of users in the digital world and in the development of verification techniques to enforce security and privacy properties in programs, devices, and systems. More specifically, my research interests embrace: Formal analysis of security and privacy properties in distributed systems (cryptographic protocols, web applications, …); Formal analysis of mobile apps; Program verification (type systems, abstract interpretation, SMT solving, …); Security and privacy by design; Privacy-enhancing technologies (ORAM, SMPC, zero-knowledge proofs, …); Privacy in cloud applications