Emanuele D'Osualdo

Researcher in Computer Science

EU Emblem This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 795218

The VeSPA project

Verification and Specification through Progress Abstractions

A Marie Curie Individual Fellowship project

Acronym VeSPA Period Sep 2018–Aug 2020
Fellow Emanuele D’Osualdo Funding Scheme MSCA-IF-EF-ST
Host Philippa Gardner Agreement 795218


Concurrent computation, organised as a decentralised collection of interacting components, is now ubiquitous. Our society increasingly relies on such systems for sensitive and critical infrastructure. To make this safe and sustainable we need a formal approach to analyse and certify the correctness of concurrent software. Our trust in concurrent systems is based on three key properties:

  1. Safety: can the system crash?
  2. Progress: will the system be reactive to requests?
  3. Security: no secret is ever leaked.

Analysing these properties is vastly more complicated for concurrent software: the decentralised interaction between processes introduces much more subtle behaviour than what is found in sequential centralised computation. Proving such properties of concurrent systems must take into consideration all possible interactions, a space is so huge and complex that we lack proper tools to reason about it, both manually and automatically. This is called the analysis scalability problem. While the case of Safety has been extensively studied, Progress and Security still lack a scalable methodology for verification.

VeSPA’s approach to solve the analysis scalability problem for Progress and Security is based on two strategies:

  1. Devising modular specifications for concurrent components.
  2. Developing automatic analysis techniques to offload parts of the analysis task to the computer.

The first strategy aims at breaking up the task of a complex concurrent system into smaller, more manageable sub-tasks about its components. This is far from trivial because progress-related arguments are typically about the interaction between components rather than individual properties of components. One of VeSPA’s main results was an analysis framework to reason about concurrent programs which can express the progress properties of a component without having to talk about the whole system. This allows for proofs that are:

The second strategy aims at automating as much as possible some parts of the correctness proofs. Ideally, the human should be able to focus on the high-level insightful aspects of a proof, and leave the tedious and very complicated reasoning for the computer to check. VeSPA advanced the state of art in automation, for proofs of correctness of cryptographic protocols. These are protocols that underpin every online activity requiring authentication, physical access control devices, e-voting systems and more. They aim at achieving secure communication in an insecure channel, through the use of cryptography. They are notoriously tricky to design and flaws are discovered every day in deployed protocols, causing huge societal and economic damages. VeSPA contributed a method and a prototype tool to automate complex steps in the verification of security properties of these protocols.



GitHub 2019