Hagrid Results #2

Online Result and Exchange Event

27th April 2020, 10:00 UTC

Information for participating are below.

A final workshop session for the challenge had been planned at ETAPS (along with the VerifyThis program verification competition). Since ETAPS has been postponed, we will meet and exchange online. We have received several 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.

Agenda

Selected timezone:

(10:00 UTC)
Greeting and Introduction to the VerifyThis Longterm Challenge 2020 by the organizers

(10:20 UTC)
Gidon Ernst and Lukas Rieger
Information Flow Testing of a PGP Keyserver

(10:50 UTC)
Diego Diverio, Cláudio Lourenço and Claude Marché
“You-Know-Why”: an Early-Stage Prototype of a Key Server Developed using Why3

(11:20 UTC)
Break (10 minutes).

(11:30) UTC)
Stijn de Gouw, Mattias Ulbrich and Alexander Weigl
The KeY Approach on Hagrid

  • Abstract
  • Resources:
    • Keyserver – A simplified single-class version of the Keyserver using arrays.
    • Map – A multi-class version using map data types.

(12:00 UTC)
Claire Dross, Johannes Kanig, and Yannick Moy
A Solution to the Long-Term Challenge in SPARK

(12:30 UTC)
Gidon Ernst, Toby Murray and Mukesh Tiwari
Verifying the Security of a PGP Keyserver

(13:00 UTC)
Final discussion and feedback to the challenge.

(13:30 UTC)
Closing

Who can join the meeting?

Everybody who is interested about the challenge, formal verification, the proposed solutions and VerifyThis is cordially to join the meeting!

How can I join the meeting?

The online event takes place with BlueJeans.

In protection against spammers, we require a short registration beforehand. The login credentials will be sent via your provided email address. Please register yourself via our Google Form or with a email to weigl at kit dot edu.

Update (2020-04-24, 13:00 o’clock): We have sent out the meeting information. If you registered before this time, you should have got an email.

Registration is still open. The meeting information will be sent manually and might take some hours.

If you havn’t got any meeting information (meeting URL + id) until Sunday evening. Please just write me (weigl at kit dot edu) short message. I have might miss you.

Meetings rules

Please respect the following simple meeting rules to have a productive meeting:

  • use your real-name (you can change it under “Poeple/Participants” in BlueJeans after joining the room.)
  • dial in 5 minutes in advance
  • mute when not speaking (avoid noise)
  • join with disabled microphone and video
  • use a headset if possible (avoid reverberation)
hagrid 

See also