Journey to a RTE-free X.509 parser — Arnaud Ebalard, Patricia Mouy, Ryad Benadjila
Date : 06 June 2019 à 09:00 — 30 min.
Nous présentons le travail de développement en C d'un parseur de certificats X.509 garanti sans bugs (de type "runtime errors"). L'objectif est de faire un retour d'expérience concret à destination des développeurs sur l'utilisation du framework de validation Frama-C afin d'obtenir ces garanties de sécurité. Une comparaison des résultats d'analyse du parseur (9000 lignes de C) avec d'autres outils sera également présentée. Le code du parseur (incluant les annotations permettant sa validation) sera publiié avant la présentation.