Composants logiciels vérifiés en F* : Poly1305 — Benjamin Beurdouche, Jean Karim Zinzindohoue
Date : 01 June 2016 à 17:15 — 15 min.
De nos jours, simplifier la création de composants logiciels formellement vérifiés est souhaitable dans de nombreux domaines. Il s’agit d’un sujet particulièrement crucial pour les composants logiciels critiques ou sensibles. Dans cet article, nous illustrons de récentes avancées dans ce domaine grâce à l’utilisation d’un langage de programmation fonctionnelle moderne dédié à la vérification : F*. Actuellement l’objet d’un développement actif, ce langage succède à d’importants travaux ayant notamment permis la publication de la première implémentation formellement vérifiée de TLS. Nous illustrons une partie des possibilités offertes par le langage au travers de l’implémentation prouvée correcte et sûre d’une primitive de code d’authentification de messages : Poly1305, dont la version présente dans OpenSSL a été l’objet de plusieurs bugs depuis mars 2016.