Dans tous les langages de programmation, certaines opérations ne peuvent être utilisées que si certaines pré-conditions sont remplies. Dans des langages comme le C/C++, l’implémentation ne vérifie pas que ces pré-conditions sont remplies, afin d’obtenir les meilleures performances. Lorsque le programme ne respecte pas ces pré-conditions, l’exécution présente un comportement indéfini. Un attaquant peut exploiter cela pour modifier le comportement prévu du programme, allant jusqu’à la prise de contrôle du processus et l’exécution de code arbitraire. Parmi tous les comportements indéfinis, l’absence de sûreté mémoire est la plus problématique, étant la source de 70% des vulnérabilités informatiques découvertes chaque année ; ce problème est donc un des problèmes majeurs de la cybersécurité à l’heure actuelle.
Le but du projet est d’augmenter le niveau de maturité technologique de l’outil Codex, qui permet de vérifier l’absence de comportement indéfini (incluant la sûreté mémoire) d’un programme, sans changer son comportement ni le réécrire dans un autre langage, et avec un faible effort ; afin qu’il puisse être utilisé par des industriels désireux de sécuriser leurs codes, comme EDF. Le projet est en effet un partenariat entre le CEA, concepteur des technologies Codex et TypedC, et EDF, utilisateur expert en utilisation de méthodes formelles, qui perçoit un potentiel fort dans l’outil et désirerait pouvoir l’utiliser.
Codex est un outil d’analyse statique par interprétation abstraite, basé sur de nouveaux concepts validés scientifiquement par des publications dans des conférences de premier plan : analyse par fonction utilisant des annotations de types légères (le langage TypedC [OOPSLA’24]), des analyses mémoires avancées s’appuyant sur une analyse numérique symbolique et basée sur les valeurs [POPL’23, PLDI’24], et ayant déjà été démontré sur de premiers exemples difficiles (une analyse de sécurité d’un système d’exploitation à partir du binaire [RTAS’21, best paper], des benchmarks d’analyses de shape [VMCAI’21], etc.).
Pour atteindre le but de rendre cet outil utilisable par tous, le projet, basé sur une interaction forte et agile entre utilisateur (EDF) et développeur (CEA), consistera à améliorer l’outil suivant 4 axes différents : Maturation et confiance dans l’outil (passage de l’outil sur des suites de tests variées, améliorations des abstractions) ; reporting et diagnostic (interface utilisateur) ; Automatisation (inférence partielle des spécifications TypedC, raffinement des traces menant à une erreur), et nouveaux langages et propriétés (intégration à un compilateur standard, analyse de code C++). Tout au long du projet, les améliorations seront testées par EDF sur des exemples réels, et les problèmes rapidement corrigés, dans le but de montrer que l’outil est d’un usage viable industriellement.
En sortie du projet, l’outil d’analyse statique open-source robuste permettra de vérifier l’absence de comportements indéfinis (dont la sûreté mémoire) dans des programmes C et C++ arbitraires (pas seulement embarqués), utilisable industriellement et de manière incrémentale. Cet outil résoudra un problème important : comment sécuriser, pour un effort raisonnable et sans besoin de changer fondamentalement de processus de développement ni de langage, des codes écrits dans des langages comme C/C++. Alors que l’appel pour avoir des développements qui soient memory-safe devient très pressant, cet outil pourra être utile pour un marché très conséquent de développeurs. Parmi eux, EDF, qui souhaite pouvoir utiliser des outils d’analyse de code sur un spectre plus large que les outils disponibles actuellement.
Partenaires : CEA et EDF