EMASS: Analyse Mémoire Efficace de Logiciel Système – EMASS

La corruption mémoire dans les logiciels systèmes écrits dans des langages non-sûrs (C, assembleur...), est toujours la source de la plupart des vulnérabilités à fort impact. En plus de la sûreté mémoire, beaucoup de propriétés de sécurité concernent des valeurs passant par la mémoire. Ce projet fournira une méthode effective pour vérifier des propriétés de sécurité liées à la mémoire dans les programmes systèmes, à partir du source ou de l'exécutable compilé. Nous nous concentrerons en particulier sur la sûreté mémoire et les propriétés de flot d'information, comme la séparation entre les tâches dans un noyau de système d'exploitation.

La méthode s'inspirera d'une analyse statique utilisant un faible nombre de simples annotations de types, développée lors de travaux préliminaires pour vérifier l'absence d'escalade de privilège dans un micronoyau embarqué [RTAS 2021, best paper]. Inspirés par ce prototype, nous voulons aborder des problèmes notoirement difficiles qu'il faut résoudre pour être utilisable industriellement?; comme passer l'analyse à l'échelle, savoir vérifier des propriétés de flot d'information, ou améliorer la précision sur certains codes difficiles.

Ce projet sera réalisé par un fort consortium rassemblant des experts en conception d'analyseurs statique, en analyse statique de C, de binaire, ou de noyaux d'OS; en vérification automatique de propriétés cyber; ou en application de méthodes formelles dans l'industrie.

Les résultats du projet consisteront en des outils d'analyse statique efficaces pour vérifier des propriétés de sécurité liées à la mémoire dans du code système, avec une méthodologie industrielle démontrée sur cas d'usage réels. Le projet proposera de nouvelles abstractions et outils qui impacteront différents champs scientifiques comme la cybersécurité, les méthodes formelles, l'ingénierie logicielle, et l'ingénierie système; et impactera aussi des utilisateurs industriels qui ont besoin de sécuriser leurs logiciels systèmes.