LACL : thèses et valorisation industrielle

Un projet en co-tutelle avec l’université québécoise de Sherbrooke

Un premier projet a pour thème les spécification et vérification de systèmes ferroviaires. C’est le sujet d’une thèse de doctorat, en co-tutelle avec l’université de Sherbrooke au Québec http://www.usherbrooke.ca/. Le travail académique est effectué en collaboration avec la société spécialisée dans le secteur ferroviaire IKOS consulting, qui finance la thèse via un « contrat industriel » pour le doctorant. L’étude porte sur la mise au point de logiciels (et de systèmes informatiques) fiables, à partir de spécifications très abstraites et de très haut niveau.

Les différentes étapes
Dans ce cadre, le projet présente plusieurs étapes : développer une méthode, construire un outil, étudier sa mise en œuvre sur des cas pratiques.

Lors de la première étape, le doctorant conçoit un langage de spécifications de systèmes, qui combine notations mathématiques et graphiques, afin de construire des modèles de systèmes qui pourront être validés par les ingénieurs experts du domaine.

Une deuxième étape consiste à réaliser des opérations de vérification de propriétés sur ces systèmes, notamment des opérations de preuves de propriétés de sûreté (comme l’absence de collision entre deux trains, par exemple).

La troisième phase consiste en la construction d’outils logiciels pour accompagner la méthode. Ces outils vont permettre aux ingénieurs experts du domaine de construire leurs modèles et d’aider à la vérification des propriétés de sûreté.

Un  projet de recherche via une convention CIFRE
Un autre projet de valorisation industrielle conduit au LACL concerne un projet de sécurité de « systèmes à logiciel prépondérant ». Les travaux de thèse sont financés via une Convention Industrielle de Formation par la Recherche, par la société privée Safe River, une société de conseil spécialisée en sûreté de fonctionnement et en cyber-sécurité des systèmes à logiciel prépondérant.

Si généralement le LACL s’intéresse à la partie « logiciels », ceux-ci sont de fait implémentés dans des systèmes (que ce soit des systèmes bancaires, des systèmes de transports, des outils cryptographiques) : les codes informatiques peuvent être vulnérables en termes de sécurité et faire l’objet d’attaques impactant leur sûreté. Le rôle du chercheur est dans ce cas de figure de vérifier et de détecter les logiciels (dont le code a déjà été écrit), d’évaluer la vulnérabilité (avec des échelles de degrés de gravité) et de trouver quels circuits/scénarios conduisent à cette vulnérabilité.

Les outils et les développements
Dans cette étude, le doctorant utilise des outils d’analyse statique et d’audit de code, qu’il enrichit en intégrant de nouvelles techniques formelles, puis conduit une analyse de haut niveau, une interprétation abstraite : il s’agit là d’une démarche inverse par rapport à celle mise en oeuvre dans le projet de recherche en co-tutelle avec l’université de Sherbrooke.

Les développements et les analyses réalisés durant cette thèse permettent d’apporter des solutions concrètes répondant à des besoins réels d’industriels, comme par exemple dans le domaine de l’avionique civil (CORAC PANDA pour Dassault aviation) et d’autres industriels du domaine (SAFRAN, SAGEM...), et également pour la RATP.