Photo credit: Robin Mathlener via Unsplash

Invited Speakers

We are pleased to announce the following keynote speakers. For further details, please visit the programme page.

Tuesday, June 18: Laura Kovács

Vienna University of Technology, Austria

Automated Reasoning in BlockChain Security

We describe a game-theoretic framework for the security analysis of blockchain protocols. We apply automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. Doing so, we reduce security analysis to satisfiability checking in first-order real arithmetic. Our approach is implemented in the CheckMate verifier and successfully applied to decentralized protocols, board games, and game-theoretic examples.

Wednesday, June 19: Paulo Veríssimo

KAUST, CEMSE, RC3 (Resilient Computing and Cybersecurity Center), Saudi Arabia

Platform Resilience? Beware of Threats from the “basement”

Modern distributed and/or modular computer systems rely on support abstractions to ease the task of building applications, such as middleware, hypervisors, libraries of secure or fault-tolerant functions, specialized hardware extensions, etc.

Over the years, given the undeniable successes of these abstractions, there has been a tendency to overestimate their reliability. For example, considering that complex middleware can be made fault free, or assuming that a hypervisor is a TCB. Such threats coming “from the basement” (since they were not assumed) can lead to unexpected and severe failures.

What has been done about this, and what more can we do? I will digress through several approaches aiming at achieving sufficient resilience of platforms at several levels, namely middleware and hypervisor fault and intrusion tolerance. But this is not enough. As years go by, threats appear at progressively lower levels. I will report some recent results aiming at achieving resilience at quite low levels of platform architectures, such as MPSoC (multi-processor systems-on-a-chip), and FPGA fabrics, exemplifying how these mechanisms yield resilience at the higher levels of modular and distributed systems.

Thursday, June 20: Marieke Huisman

University of Twente, The Netherlands

VerCors: Inclusive Software Verification

VerCors supports deductive verification of concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-/postcondition contracts using permission-based separation logic. Work on the VerCors verifier has started more than a decade ago. In this decade, the focus of the work on VerCors has shifted from verification of (concurrent) Java programs only to the development of a verifier that can support different programming languages, by exploiting their commonalities for developing efficient verification support.

In this talk, I will first give an overview of the VerCors verifier:

how it is set up as a program transformation tool that translates an annotated program into input for the Viper framework, which is then used as verification back-end
how it supports different programming languages and features, and
how it has been used on different case studies (and how this has further improved VerCors).

In the last part of my talk, I will sketch my ideas and plans to further increase the inclusiveness of VerCors, so that it becomes easier to support new programming languages and to reuse the existing verification infrastructure in new settings.