Department of Computer Science

Hot topics in language-based security is a series of seminars that will be held by well-known international speakers, organised by the PhD in Computer Science of University of Pisa in collaboration with IMT Lucca, as part of their Research Topics in Computer Science series.
The first part of these seminars, mainly devoted to secure compilation and isolation mechanisms, will also be offered to MS students within the course "Laboratory for innovative software".
To get the credits for this seminar series, each PhD student must attend 80% of the seminars.
The seminars address methods and techniques that foster the security of applications and systems from their design and implementation, by focusing on formal methods and the features and properties of programming languages.

• March, 17, at 14:00: Véronique Cortier
  Title: Electronic voting: design, attacks and proofs
  Abstract: Electronic voting aims to achieve the same properties as traditional paper based voting. Even when voters vote from their home, they should be given the same guarantees, without having to trust the election authorities, the voting infrastructure, and/or the Internet network. The two main security goals are vote privacy: no one should know how I voted; and verifiability: a voter should be able to check that the votes have been properly counted. In this talk, we will explore how these properties can be realized, attacked, and proved. We will in particular illustrate our presentation with the Belenios protocol.
  Short Bio: Véronique Cortier is CNRS research director at Loria (Nancy, France). In 2003, she received her Ph.D. degree in Computer Science from the École Normale Supérieure de Cachan, from which she graduated. Her research focuses on formal verification of security protocols, in particular e-voting, using formal techniques or provable security. She is editor in chief of JCS and editorial member of TOPS, member of the steering committee of Esorics. In 2010, she was awarded an ERC starting grant and in 2015, she received the INRIA - Académie des Sciences young researcher award.
• March, 22, at 16:00: Matteo Busi
  Title: Securing Interruptible Enclaved Execution on Small Microprocessors
  Abstract: Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features brings a risk of introducing new software-based side-channel attacks.
  In this talk we show how we extended a processor with new features without weakening the security of the isolation mechanisms that the processor offers. Our solution is heavily based on techniques from research on programming languages. More specifically, we propose to use the programming language concept of full abstraction as a general formal criterion for the security of a processor extension. We instantiate the proposed criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, prove that it satisfies our security criterion and explain how such design drove the actual implementation of an enclave-enabled microprocessor.
  Short Bio: Matteo Busi got his PhD at the University of Pisa and he is currently a post-doc at the Ca' Foscari University of Venice. His research interests include cybersecurity, programming languages, and formal methods. Currently, he is focusing is on secure compilation, that is "how is it possible to guarantee that program transformations preserve security properties?''
• March, 24, at 16:00: Dominique Devriese
  Title: Towards Rigorous Verification of Large Systems with Capability Machines, Program Logics and Universal Contracts
  Abstract: In this presentation, I will present an overview of my research on formalizing security guarantees of ISAs with a particular focus on capability machines.
  I will explain the core ideas behind capability machines, and how one can can rigorously reason about security of software running on them, using a library called Cerise. Next, I will explain how we intend to scale up Cerise to real ISAs and real systems. Particularly, I will explain talk about Katamaran: a tool we are building to verify universal contracts for existing, large formal ISA specifications.
  Short Bio: Dominique Devriese is a professor in the research group DistriNet, at KU Leuven, Belgium. He has previously worked at Vrije Universiteit Brussel and has recently been awarded a prestigious ERC Starting Grant on formalizing ISA security properties. His research interests lie around the boundary of computer security, programming languages and verification. Current topics include particularly object capabilities and capability machines, formally characterizing security properties of ISAs, secure compilation and rigorous reasoning about systems' security. In addition, he has an active interest in functional and dependently typed programming and programming languages, particularly Agda and Haskell.
• April 7 at 16:00: Frank Piessens
  Title: Formal language-based methods for studying transient execution attacks and defenses
  Abstract: Microarchitectural security is one of the most challenging and exciting problems in system security today. With the discovery of transient execution attacks, it has become clear that microarchitectural attacks have significant impact on the security properties of software running on a processor that runs code from various stakeholders (such as, for instance, in the cloud). This seminar will provide an introduction to transient execution attacks and defenses using formal language-based models for processors. We will first briefly recap the constant-time leakage model commonly used to model microarchitectural leakage when studying implementations of cryptographic primitives. Next, we turn to modeling speculative and out-of-order execution, and we discuss by means of examples how these features lead to powerful new classes of attacks. Finally, we turn to formal statements of security objectives for defenses. Part of the challenge here is to find good trade-offs between the strength of the security objective, and the efficiency of the mechanisms realizing that security objective.
  Short Bio: Frank Piessens is a full professor in the Department of Computer Science at the Katholieke Universiteit Leuven, Belgium. His research field is software and system security, where he focuses on the development of high-assurance techniques to deal with implementation-level vulnerabilities and bugs, including techniques such as software verification, run-time monitoring, hardware security architectures, type systems and programming language design. He has served on the program committee of numerous security and software conferences including ACM CCS, Usenix Security, IEEE Security & Privacy, and ACM POPL. He acted as program chair for the International symposium on Engineering Secure Software and Systems (ESSOS 2014 & 2015), for the International Conference on Principles of Security and Trust (POST 2016), for the IEEE European Symposium on Security & Privacy (Euro S&P 2018 & 2019) and for the IEEE Secure Development Conference (SecDev 2021 & 2022)
• April 28 at 16:00: Roberto Guanciale
  Title: Validation of Abstract Side-Channel Models for Computer Architectures
  Abstract: Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We present a methodology to validate observational models for modern computer architectures. This approach combine symbolic execution and relational analysis to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. This approach has been evaluated by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. The results show that this approach can generate tests that invalidate the models due to hidden microarchitectural behavior, including new types of speculative leakage.
  Short Bio: Roberto Guanciale is an associate professor within the Division of Theoretical Computer Science, EECS, KTH, where he works on system security and formal verification. He received his bachelor and master degrees in Computer Science from University of Pisa and his Ph.D. from IMT Lucca in 2009. His research focuses on Computer Security, in particular on formal verification low level code and design of separation kernels. He also designed methods to analyze coordination of distributed services.
• May 3 at 15:00 and May 5 at 10:00: Marco Patrignani
  Title 1st part: Secure compilation: theory
  Title 2ndpart: Secure compilation: practice
  Abstract: This seminars explore the theory and practice aspects of the nascent field of secure compilation, which sits at the intersection between security and programming languages. The goal of a secure compiler is to compile programs in order to preserve source security properties like data confidentiality and code integrity. This is challenging because attackers operating at the level of the compiler output are inherently more powerful than attackers in the source language. For example, target attackers can mount buffer overflows that bypass compiled code security abstractions that derive e.g., from compiled source level type annotations.
  This seminar will describe: the threat model that secure compilers consider and the correctness criteria for secure compilation (May 3); specific instances of secure compilers and proof techniques for secure compilation (May 5).
  Short Bio: Marco Patrignani is Assistant Professor at the University of Trento. Previously, he was a PhD student at KU Leuven (with Dave Clarke and Frank Piessens), a postdoctoral researcher at MPI-SWS (with Deepak Garg), a visiting assistant professor at Stanford University (with John Mitchell) and a research group leader at Cispa. He is interested in formal methods, programming language and security, and he is one of the main promoters of the secure compilation research field, having developed with his collaborators: secure compilation criteria, proof techniques for secure compilation, and instances of secure compilers.
• June 9, at 14:00: Riccardo Focardi
  Title: Breaking and fixing cryptographic systems
  Virtual Location
  Abstract: In recent years, we have faced an increasingly pervasive use of cryptography. The expansion of IoT, home automation and industry 4.0 has worryingly increased the attack surface, making it necessary to use cryptographic protocols to protect communications and data. However, cryptography is complex: not all cryptographic mechanisms offer the same level of protection; management and configuration is often the Achilles' heel of cryptographic systems; finally, protocols and implementations may present bugs that weaken or, in some cases, cancel the security guarantees offered by the adopted mechanisms. In this talk we will give an overview of the problems and attacks encountered in real cryptographic systems, discussing their weaknesses and possible remedies. We will present some practical case studies we have dealt with, highlighting how we improved the security of real cryptographic systems through foundational research and formal verification.
  Short Bio: Riccardo Focardi is Full Professor of Computer Science and coordinates the Cybersecurity Reserach Lab at Ca' Foscari University, Venice. His research interests include: system and network security, analysis of security APIs and trusted hardware, cryptography, specification and automated verification of security properties. He has been involved into national and European projects on Computer Security. He has been member of many program committees of international conference and has been program chair of the IEEE Computer Security Foundation Symposium in 2003 and 2004. He is founder and member of the steering committee of the Italian Conference on Cybersecurity (ITASEC). From 2016 to 2019 he has been chair of the IFIP Working Group 1.7 "Theoretical Foundations of Security Analysis and Design" and from 2005 to 2019 he has been member of the editorial board of the Journal of Computer Security. From 2012 to 2019 he has coordinated the PhD program in Computer Science at CaÕFoscari, starting an international double-degree in Cybersecurity with Masaryk University, Brno. In 2013 he has co-founded Cryptosense, a spin-off that develops software for security analysis of cryptographic systems and in 2020 he has co-founded 10Sec, a spin-off developing advanced solutions for the security of IoT devices.
• June 16 at 17:00: Moshe Vardi
  Title: Lessons from Texas, COVID-19 and the 737 Max: Efficiency vs Resilience
  Virtual Location
  Abstract: In both computer science and economics, efficiency is a cherished property. In computer science, the field of algorithms is almost solely focused on their efficiency. In economics, the main advantage of the free market is that it promises "economic efficiency". A major lesson from many recent disasters is that both fields have over-emphasized efficiency and under-emphasized resilience. I argue that resilience is a more important property than efficiency and discuss how the two fields can broaden their focus to make resilience a primary consideration. I will include a technical example, showing how we can shift the focus in strategic reasoning from efficiency to resilience.
  Short Bio: Moshe Y. Vardi is University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the recipient of several awards, including the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Knuth Prize, the IEEE Computer Society Goode Award, and the EATCS Distinguished Achievements Award. He is the author and co-author of over 700 papers, as well as two books. He is a Guggenheim Fellows as well as fellow of several societies, and a member of several academies, including the US National Academy of Engineering and National Academy of Science. He holds seven honorary doctorates. He is a Senior Editor of the Communications of the ACM, the premier publication in computing. Moshe Y. Vardi Home page: http://www.cs.rice.edu/~vardi
• June 23, at 14:00: Jan Friso Groote
  Title: Behavioural modelling and model checking are becoming very effective tools indeed.
  Virtual Location (Also in presence in Classroom 1 at IMT)
  Abstract: Milner initiated process algebras to describe and study the behaviour of interacting systems. Various people added modal logics to denote properties using which this behaviour can be studied. We brought these together in the language/toolset mCRL2 on which we have been working for more than 30 years now. The result is an abstract, but versatile modelling and analysis formalism, which we are using to develop and analyse distributed and parallel algorithms, solve behavioural puzzles, check communication protocols and produce software. The mCRL2 toolset has been adopted by a number of companies as verification backend. Multiple companies in the region around Eindhoven develop substantial parts of their software through verified models and some have literally many thousands of them. In this talk I will explain behavioural modelling and analysis via mCRL2, guided via a number of examples, and hope to convince you why I believe that process algebras and modal logics are utterly effective tools.
  Short Bio: Jan Friso Groote ?is a Full Professor and Chair of Formal Systems Analysis group in the Department of Mathematics and Computer Science at Eindhoven University of Technology (TU/e). His areas of expertise include Computer systems, architectures, software, algorithms, embedded systems and formal methods. Jan Friso has contributed to? structural operational semantics? and verification technology. His particular contributions include the? tyft/tyxt format?for operational rules, the first and also the most efficient algorithms to determine ?branching bisimulation?and the?cones and foci method?to prove correctness of protocols and distributed algorithms. He is the founding father of the process modeling language and analysis tool set? mCRL2. More details at https://www.tue.nl/en/research/researchers/jan-friso-groote/

• Chiara Bodei: chiara.bodei@unipi.it
• Matteo Busi: matteo.busi@unive.it
• Gabriele Costa: gabriele.costa@imtlucca.it
• Pierpaolo Degano: pierpaolo.degano@unipi.it
• Gian-Luigi Ferrari: gian-luigi.ferrari@unipi.it
• Letterio Galletta: letterio.galletta@imtlucca.it