StarMalloc : un allocateur de mémoire moderne renforcé formellement vérifié

Malgré la popularisation de langages modernes qui permettent une gestion sûre de la mémoire, C et C++ restent des langages de choix pour le développement de nombreux logiciels très couramment utilisés. Si ces langages permettent d’obtenir de bonnes performances, ils sont particulièrement vulnérables aux attaques par corruption mémoire. Des études récentes estiment que des erreurs de gestion de la mémoire, telles que des dépassements de tampon, sont la cause principale de 70% des vulnérabilités dans des logiciels très utilisés comme Android ou Google Chrome.

Pour contrer ces attaques, les allocateurs mémoire modernes adoptent généralement un design orienté pour la sécurité, qui permet de limiter le risque de corruption mémoire. Dans cet exposé, nous présentons StarMalloc, un allocateur moderne orienté pour la sécurité vérifié formellement en utilisant l’assistant de preuve F* et la logique de séparation concurrente Steel. Nous montrons comment spécifier et vérifier les invariants de cet allocateur, dont l’architecture est inspirée de celle de hardened_malloc, ainsi que la correction des mécanismes de sécurité implémentés. Enfin, nous présentons des résultats expérimentaux comparant StarMalloc à d’autre allocateurs, en évaluant leur performance sur différentes applications, dont le navigateur Firefox.