What is VerifyThis?
The VerifyThis verification competition is a regular event run
as an onsite meeting with workshop character in which three
challenges are proposed that participants have to verify in 90
minutes each using their favourite program verification tool.
We have experienced that the state of the art of program
verification allows the participants to specify and verify
impressively complex algorithms in this short a time span. If
such sophisticated, realistic but not real, problems can be
solved in real-time, what would be achievable if (a)~we as the
program verification community collaborated and (b)~the time
constraints were removed?
The Challenge
This VerifyThis Collaborative Large Scale Challenge
aims at proving that deductive program verification can produce
relevant results for real systems with acceptable effort.
For this year, we selected HAGRID,
a PGP-keyserver, for the challenge.
HAGRID is a fresh development, which became necessary as the old
keyserver (SKS) is vulnerable against DoS attacks
CVE-2019-13050,
is not conform with GPRD, and had performance issues.
More background information are available in the
blog
post of the developers HAGRID is already in production.
How to participate?
Participation on the challenge is easy. You should pick your favourite
tool for the formal software assessment, and try whether you
find a bug or prove adhering of the specification in HAGRID (or
a suitable abstraction).
Of course you can participate in groups. Moreover, we would like to foster
collaboration between participating groups. Therefor we would
appreciate if you register your group.
Do not forget to also subscribe to our
mailing list
(verifythis-ltc@lists.kit.edu) to be able to share your questions and
your work and to keep up to date with the work of the rest of the teams.
We plan to publish on the VerifyThis workshop at the
ETAPS2020,
where we kindly invite each participant to present their results
of this challenge.