You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3
| Autor: | Diego Diverio, Cláudio Belo Lourenço, Claude Marché |
|---|---|
| Přispěvatelé: | Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Service Expérimentation et Développement (SED [Saclay]), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), Marché, Claude |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: | |
| Zdroj: | VerifyThis 2020-Long-term Challenge VerifyThis 2020-Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7 HAL |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|