Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Verifying the Hagrid Key-Server with JJBMC

Typ: BA / MA
Datum: 2021-01-20
Betreuer: Mattias Ulbrich
Jonas Klamroth
Aushang:

Problem

When using public key encryption and signatures in e-mails, one challenge is to obtain the public key ofrecipients. To this end, public key servers have been installed that can be queried for public keys. The most popular public key server OpenPGP was recently shown to have severe security flaws. As a consequence, the OpenPGP community decided to implement a new server framework that manages the access to public keys. The new official server is called hagrid, it is open source, and it is already in production. Hagrid is written in the programming language Rust and comprises some 6,000 lines of code in total. This implementation is thereference implementation of a verifying keyserver.

In 2020 the VerifyThis competition challenged researchers to specify and verify this reference implementation.

Goal

The goal of this thesis is to use the tool JJBMC developed at the KIT and FZI to verify a Java implementation of a hagrid server. Main challenges will include the adaptation and extension of the specification and implementation as well as the tool itself.

Contact: