[TYPES/announce] VTLTC 2020 - Final Call for Online Participation

[r.e.monti at utwente.nl]

                    Final Call for Online Participation

                 VerifyThis Long-Term Challenge 2020

                -- Online Result and Exchange Event --

                      27th April 2020, 10:00 UTC [0]

         >>> https://verifythis.github.io/online-event <<<


!! Please register on this website if you want to participate
!! (There are no costs involved in participating)


## Introduction
 
The VerifyThis Long-Term Challenge complements the on-site format of
the VerifyThis competition with a verification challenge, in which
teams contribute to the verification of a practically relevant piece
of software over a longer period of time. The challenge aims to be a
showcase that deductive program verification can produce relevant
results for real systems with acceptable effort.

The challenge system to be verified is the new implementation of the
PGP server infrastructure, called HAGRID [2]. The old implementation
did not conform to GDPR and was known to be vulnerable against DoS
attacks.


## The Online Result and Exchange Workshop

A final workshop session for the challenge had been planned at ETAPS
(along with the VerifyThis program verification competition [1]).
Since ETAPS has been postponed, we will meet and exchange online.

We have received five submissions that each contribute a solution to
different aspects of the challenge using different abstractions,
different assumptions and different verification techniques.

During this online meeting, the different solutions will be briefly
explained, and we discuss the approaches, how they can benefit from
one another and how further verification success can be stipulated.

This meeting is not meant as a replacement of the on-site event. It is
meant as an informal event to exchange ideas, to give positive
impulses on further advances of approaches, or on how to combine
solutions. If the situation permits, the onsite event will take place
in autumn during ETAPS.

## Call for Participation

Everybody who is interested about the challenge, the proposed
solutions and VerifyThis is cordially invited to join the meeting! To
avoid spammers, you need to register yourself. An email with login
credentials will be sent in advance. Registration information, agenda
and resources are on our webpage of the online workshop:

          >>> https://verifythis.github.io/online-event <<<



## Agenda

We start at 10:00 UTC. Please join the meeting in-time.

1. Greeting and Introduction to the VerifyThis Longterm Challenge 2020

2. Claire Dross, Johannes Kanig, and Yannick Moy
   A Solution to the Long-Term Challenge in SPARK

3. Diego Diverio, Cláudio Lourenço and Claude Marché
   ``You-Know-Why'': an Early-Stage Prototype of a Key Server
   Developed using Why3

4. Stijn de Gouw, Mattias Ulbrich and Alexander Weigl
   The KeY Approach on Hagrid

5. Gidon Ernst and Lukas Rieger
   Information Flow Testing of a PGP Keyserver

6. Gidon Ernst, Toby Murray and Mukesh Tiwari
   Verifying the Security of a PGP Keyserver

7. Final discussion and feedback to the challenge.

8. Closing (ca. 14:00)


## Program Chairs and Organizers

Marieke Huisman                 Raul E. Monti

Mattias Ulbrich                 Alexander Weigl


[0] Find out your local time here:
    https://www.timeanddate.com/worldclock/fixedtime.html?msg=VerifyThis%20Online&iso=20200427T12&p1=964&ah=3

[1] https://www.pm.inf.ethz.ch/research/verifythis.html

[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/