Nicolas Szlifierski (Dpt INFO – Laboratoire Lab-STICC) soutient sa thèse de doctorat le 17/12/2020

Titre : Contrôle sûr de chaînes d'obfuscation logicielle
Mots-clés : Obfuscation, Chaînes de compilation, Langage dédié, Typage, Sémantiques formelles

Texte

Le jury est composé de :
- M. Fabien DAGNAT- Maître de conférences (HDR), IMT Atlantique
- Mme Laure GONNORD - Maître de conférences, Université de Lyon 1
- M. Serge GUELTON -Ingénieur, Redhat
- M. Thomas JENSEN- Directeur de recherche, INRIA
- Mme Catherine DUBOIS - Professeur, ENSIIE
- M. Pierre-Etienne MOREAU -Professeur,Mines Nancy - Université de Lorraine

Invité :
- M. Sébastien JOSSE - Docteur, Ingénieur DGA Maitrise de l'Information

Soutenance le vendredi 27 novembre 2020 à  09h00 à IMT Atlantique (campus de Brest) en Visio-conférence totale (dispositions exceptionnelles durant la crise sanitaire liée au Covid19)

résumé : L'obfuscation de code est une technique de protection de programme qui consiste à rendre la rétro-ingénierie d'un programme plus difficile, afin de protéger des secrets, de la propriété intellectuelle, ou de compliquer la détection (malware). L'obfuscation est généralement effectuée à l'aide d'un ensemble de transformations sur le programme cible. L'obfuscation est également souvent utilisée en conjonction avec d'autres techniques de protection de programmes telles que le watermarking ou le tamperproofing. Ces transformations sont généralement intégrées dans les transformations de code appliquées pendant le processus de compilation, comme les optimisations. Cependant, appliquer des transformations d'obfuscation demande plus de préconditions sur le code et de précisions
dans l'application pour offrir un compromis performance/sécurité acceptable ce qui rend les compilateurs traditionnels peu adaptés à l'obfuscation.
Pour répondre à ces problèmes, cette thèse propose SCOL, un langage qui permet de décrire le processus de compilation d'un programme en prenant en compte les problématiques spécifiques à l'obfuscation. Celui-ci permet de décrire des chaînes de compilation avec un haut niveau d'abstraction, tout en permettant une précision élevée sur la composition des transformations. Le langage possède un système de types qui permet de vérifier la cohérence de la chaîne de compilation. C'est-à-dire que vérifier que la composition des transformations permet d'obtenir le niveau de protection et de couverture visé.

 

 

Contacts

avis de soutenance : Nicolas Szlifierski
lien de diffusion: direct

Publié le 11.12.2020

par Pascale MÉNARD