Symposium sur la sécurité des technologies de l'information et des communications

Conférence francophone sur le thème de la sécurité de l'information.
Elle a eu lieu à Rennes du 1 au 3 juin 2016.

Composants logiciels vérifiés en F* : Poly1305Benjamin Beurdouche, Jean Karim Zinzindohoue


Date : 01 juin 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.