You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3

Diego Diverio (1, 2) , Cláudio Lourenço (3) , Claude Marché (3)

1 VALS - LRI - Vérification d'Algorithmes, Langages et Systèmes (LRI)
2 SED [Saclay] - Service Expérimentation et Développement
3 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

We report on a solution we designed for the VerifyThis Collaborative Long Term Challenge 2019. We used the Why3 verification framework to design, from scratch, a simple but running prototype implementation of a PGP key server. We exploit the ability of Why3 to extract OCaml code from verified WhyML code so as to produce code that can be compiled into an executable. Our prototype is made of a combination of unverified handwritten OCaml code and of WhyML code whose functional behaviour is formally specified and proven correct.

Domaines: Logique en informatique [cs.LO]

Diego Diverio, Cláudio Lourenço, Claude Marché. You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3. VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7. ⟨hal-03002187⟩