VASCO signifie "VAlidation de Systèmes Composants et Objets logiciels". La recherche développée par l’équipe VASCO s’inscrit dans le champ du génie logiciel et des méthodes formelles appliquées. L’équipe appartient à l’axe "Génie des Logiciels et des Systèmes d’Information" du LIG, et partage avec plusieurs de ses équipes la conviction que les outils de génie logiciel doivent être articulés autour des modèles. Notre activité principale est la validation qui concerne tant le logiciel que les modèles, avec un intérêt particulier pour la validation de la sécurité des systèmes informatiques.

 

La validation des logiciels se traduit principalement en diverses activités de test, de la génération des tests à leur évaluation, ce qui inclut également des recherches sur la mesure de testabilité. Le test d’un logiciel suppose aussi que l’on dispose d’un oracle pour décider du succès ou de l’échec du test. Cet oracle fait le plus souvent référence à des modèles décrits dans les phases initiales du développement logiciel (analyse des besoins, spécification, conception). La mise en œuvre de l’oracle dans l’équipe VASCO utilise des techniques de « monitoring » : vérifications à l’exécution ou, a posteriori, sur des traces d’exécution.

 

Lorsque le développement est basé sur des modèles, il est essentiel de valider également ces modèles. La validation des modèles passe généralement par leur compréhension par des êtres humains (analystes, clients), et peut être facilitée en liant des modèles formels à des représentations graphiques ou par l’utilisation de techniques d’animation. Les thèmes de recherche de VASCO sont donc la modélisation et le test. Nos recherches ont été appliquées dans des domaines très variés, le plus souvent dans le cadre de projets ANR ou européens : avionique, systèmes de télécommunications, domotique, interfaces multi-modales, applications embarquées (Android, micro-controlleurs, cartes à puce), Internet des services, systèmes d’information sécurisés et réglementations de la sécurité des aéroports. Au cours de ces dernières années, l’équipe a participé à de nombreux projets relatifs à la sécurité informatique, incluant la modélisation et le test de politiques de sécurité et la recherche de vulnérabilités.

 

Les méthodes formelles appliquées sont par essence reliées au développement ou à l’utilisation d’outils logiciels. VASCO développe des outils pour la génération automatique de tests (Kameleon Fuzz, Tobias, Lutess, Jartege), la localisation de fautes dans des traces d’exécution (COMET) , la construction ou réingénierie de modèles (Simpa, B4MSecure, RoZ), et la modification d’applications Android sans accès au code (Weave Droid).

 

Nos recherches s’inscrivent dans les défis "Sécurité, sûreté, fiabilité", "Systèmes embarqués" et "Bâtiment intelligent" du projet scientifique du LIG et du projet PILSI. Elles contribuent au projet "informatique ambiante et durable" du LIG par ses contributions en sûreté, sécurité et qualité du logiciel.