Lorsqu’on cherche à garantir l’absence de vulnérabilités dans un code source, il ne suffit pas de disposer d’un outil capable de les détecter : on souhaite s’assurer qu’il n’en existe aucune.
C’est un des objectifs de l’outil de vérification formelle Frama-C du CEA-List : vérifier automatiquement, à l’aide de preuves mathématiques, l’absence d’une large classe de vulnérabilités, telles que les buffer overflows (dépassements de l’emplacement mémoire réservé pour des données, dus à l’absence de précautions lors de la programmation).
Cette vérification demande un certain investissement, mais est d’autant plus facile à mettre en œuvre qu’elle est intégrée tôt dans le cycle de développement. Cela permet de détecter l’introduction de défauts à un moment où ils restent faciles à corriger. Cela permet également de mettre en évidence, très en amont, les contraintes de l’analyse et d’inciter les développeurs à adopter un style de programmation mieux adapté à la vérification automatique.
L’utilisation de Frama-C s’intègre idéalement dans un processus d’intégration continue, pratique de développement dans laquelle le code est testé et validé à chaque modification, dès le début du projet. Pour que Frama-C puisse être intégré à un tel processus, son temps d’analyse doit rester comparable à l’intervalle entre deux modifications du code. Pour répondre à cette contrainte, nous avons développé dans Frama-C des techniques d’analyse incrémentale.
Le principe consiste à repartir d’une analyse déjà effectuée et à réutiliser autant que possible ses résultats afin d’accélérer l’analyse d’une version modifiée du code. La difficulté majeure est d’établir formellement que cette réutilisation ne compromet pas la correction : les résultats doivent rester aussi fiables que si l’analyse était complète.
Deux techniques ont été mises en œuvre.
La première repose sur la réutilisation de résumés de fonctions du code que l’analyseur a produits lors de la première analyse. Ces résumés correspondent à des propriétés mathématiques déduites de chaque fonction. En comparant les versions du code et en explorant leur structure, on détermine quels résumés peuvent être réutilisés pour la nouvelle analyse de la fonction.
La seconde technique vise à accélérer la recherche des invariants de boucle (propriétés logiques du code) : les invariants découverts lors d’une analyse précédente sont réutilisés comme points de départ pour trouver plus rapidement les invariants de la nouvelle version du code.
Les premiers résultats expérimentaux, à partir de codes open source dont l’historique de modifications est public, montrent que l’analyse incrémentale de code avec Frama-C permet de réduire le temps d’analyse d’un facteur de ×1,5 à ×28, avec une moyenne de ×7,83. L’expérimentation met également en évidence une très faible variation des résultats de l’analyse, sans remettre en cause sa fiabilité. Cela confirme ainsi la pertinence de notre approche dans un contexte d’intégration continue.
Un usage précoce de Frama-C dans le développement logiciel permet de détecter les vulnérabilités au moment où elles sont faciles à corriger.
Ces travaux ont été réalisés en partenariat avec Sorbonne Université et s’inscrivent dans le cadre du projet SecurEval du PEPR Cybersécurité, financé par France 2030.
Ils ont donné lieu à une publication :
