Contexte
CompCeRt compile des programmes C en langage assembleur de plusieurs processeurs. Contrairement aux autres compilateur comme Visual C++, GCC ou LLVM, ses phases de compilation sont prouvées correctes avec un vérificateur de théorèmes (en l’occurrence Coq). Ces autres compilateurs peuvent contenir des bugs, dits de « miscompilation », conduisant à produire du code incorrect. De tels bugs peuvent être dramatiques dans les applications critiques et conduisent parfois à les concepteurs de telles applications à compiler sans optimisation pour vérifier “manuellement” que le code assembleur correspond au code source.
CompCeRt, bien que ne réalisant pas toutes les optimisations de ses concurrents, optimise les programmes assembleurs générés avec un niveau de sûreté inégalé. Mais, face à des attaques de sécurité, les optimisations réalisées par le compilateur, même quand elles sont fonctionnellement correctes, peuvent être indésirables. Typiquement, elles peuvent invalider (voire éliminer) des contre-mesures logicielles, comme la mise à zéro de données sensibles ou les calculs redondants détectant les incohérences induites par attaque matérielle. Or, ces contre-mesures sont plus faciles à mettre en place lors de la conception du logiciel (i.e. au niveau source) : idéalement elles doivent donc être transportées du source au binaire. De plus, il serait intéressant de mettre en lien (par exemple par un système d’annotations) les contre-mesures et leur objectif de sécurité.
Des premiers travaux dans ce sens ont été développés dans la thèse de Son Tuan Vu autour du compilateur LLVM. Le principe est de poser des observateurs imposant au compilateur de préserver des valeurs en un point du programme et de rendre opaque certaines valeurs de calcul afin d’empêcher certaines optimisations.
Objectifs de la thèse
Le point de départ de cette thèse sera de reprendre ces travaux et de voir comment les intégrer dans CompCeRt, sachant que CompCeRt propose déjà des systèmes d’annotations qui garantissent la préservation de certaines observations par le code généré (avec une preuve formelle de cette préservation dans les passes successives du compilateur). En particulier :
- Il faudra mener des études de cas (inspirée de l’état de l’art) sur certains objectifs de sécurité et certaines contre-mesures : quelles garanties les contre-mesures permettent d’assurer face aux objectifs de sécurité (e.g. sous quelles hypothèses la mise à zéro d’une mémoire garantit l’absence de fuite d’informations sensibles) ? quelles observations faut-il faire sur ces contre-mesures afin d’assurer leur préservation par la chaîne de compilation ?
- Quelles contre-mesures/objectifs de sécurités sont difficilement exprimables dans le système d’annotations de Vu ? Comment étendre celui-ci ?
- Comment utiliser le mécanisme d’annotations pour évaluer l’efficacité et la pertinence des contre-mesures vis-à-vis des objectifs de sécurité (en lien par exemple, avec un outil comme Lazart) ?
- La sémantique formelle offerte par CompCeRt permet-elle de formaliser (au moins partiellement) les garanties offertes par les contre-mesures vis-à-vis des objectifs de sécurité ?
- Comment cette approche, où c’est le programmeur qui indique comment garantir l’objectif de sécurité, se compare avec d’autres approches, où c’est CompCeRt qui prend en charge les objectifs de sécurité ? A priori, on s’attend à ce que l’approche par annotation soit plus facilement généralisable à divers objectifs de sécurité, et que la mise en œuvre soit moins lourde au niveau du développement de CompCeRt (quitte à demander plus de travail à l’utilisateur de CompCeRt). À quel point ce point-de-vue à priori se vérifie-t-il en pratique ?
Contact
Si vous êtes intéressé(e)s, n’hésitez pas à contacter Marie-Laure Potet et Sylvain Boulmé
