Model-based scenario testing

La plupart des logiciels que l'on utilise tous les jours sont écrits en langage bas-niveau C/C++, et certaines applications ont mêmes des parties en assembleur. Ces langages permettent de créer des programmes très efficaces et performants mais restent très vulnérables à des attaques de type injection de code, corruption de code, fuite d'information, etc \(\ldots\) En effet, ceux-ci exploitent des bugs de programmation le plus souvent liés à la (mauvaise) gestion de la mémoire [1]. Par ailleurs, les applications s'exécutant sur de petits systèmes embarqués peuvent aussi être soumis à des attaques physiques qui permettent de récupérer des informations, d'accéder à des services sans y être autorisé, prendre le contrôle du système sans même exploiter de vulnérabilités logicielles.

L'ajout de protections logicielles permet de se prémunir contre ses attaques ou les rendre trop difficiles à réaliser. Toutefois, il faut pouvoir cibler les parties de code à sécuriser et garantir que l'application est robuste. Sécuriser une application vise à protéger sa fonctionnalité ou les données sensibles manipulées. Elle dépend donc de l'application et vérifier qu'une application est sécurisée nécessite de connaitre la propriété de sécurité que l'on souhaite garantir.

L'équipe ALSOC étudient depuis plusieurs années les effets d'attaques sur des codes assembleurs et s'appuient sur les méthodes formelles pour vérifier des contre-mesures, évaluer la robustesse de code contre des attaques physiques. De plus, l'équipe dispose d'une plateforme de vérification au niveau assembleur RobustA [2].

Le Model-based security testing [6], c'est à dire la génération de test pour des propriétés de sécurité, émerge comme une nouvelle approche pour améliorer les campagnes de tests des systèmes sécurisés ou des mécanismes de protection.

L'objectif du stage est de concevoir et développer une méthode de génération automatique de scénarios d'attaque à partir des modèles d'attaques et de vulnérabilités en se concentrant dans un premier temps sur la génération de test de scénarios connus.

La première partie du stage consistera à faire une étude bibliographique sur les techniques de model-based testing en général et orienté sécurité pour les tests bas-niveau et les tests d'intégrations logiciel/matériel.

La seconde partie du stage consiste à construire un modèle de test pour :

• un exemple jouet : le code pin
• un exemple un peu plus conséquent : une fonctionnalité du code de FreeRTOS

Le modèle de test contient le code, mais aussi une modélisation de la classe d'attaque que l'on souhaite considérer et qui nous permettra de guider la génération automatique de scénarios d'attaque.

Les étapes suivantes pour chaque modèle consisteront à

• générer des à l'aide de l'outil RT-tester (de

l'université de Brême) ;

• Analyser les tests trouvés pour affiner les critères de sélection utilisés lors de la génération. Cela passera par la définition d'une métrique pour quantifier la qualité des tests générés.

• Connaissance de la programmation C/C++/assembleur,
• Modélisation haut-niveau type SysML,
• Connaissance en sécurité et des notions d'attaque bienvenues.