An Approach for Safe and Secure Software Protection Supported by Symbolic Execution

Cet article présente une nouvelle méthode de protection logicielle pour les systèmes de contrôle industriel qui lie le logiciel au matériel via des fonctions physiques non clonables (PUF) et utilise l'exécution symbolique pour garantir la sécurité et la préservation des propriétés de sûreté en cas d'exécution sur une machine non autorisée ou d'échec de la réponse PUF.

L'essentiel

Voici une explication simple et imagée de ce papier de recherche, conçue pour être comprise par tout le monde, sans jargon technique.

Imaginez que vous possédez une recette de cuisine secrète (le logiciel) qui ne fonctionne parfaitement que si vous utilisez un four spécifique (le matériel/hardware). Si vous essayez de cuisiner cette recette dans un autre four, même un clone exact, le gâteau sera toujours comestible et ne vous empoisonnera pas, mais il aura un goût bizarre et imprévisible. C'est l'idée centrale de cette recherche.

Voici comment les auteurs ont conçu ce système de protection :

1. Le Problème : Le Vol de Recettes

Dans le monde industriel, voler le "cerveau" d'une machine (son logiciel) est un gros problème. Souvent, les voleurs n'ont pas besoin de comprendre comment ça marche ; ils copient simplement le code et le mettent sur une autre machine. C'est comme photocopier une recette et l'utiliser dans n'importe quelle cuisine. Les auteurs veulent empêcher cela.

2. La Solution : L'Empreinte Digitale du Four (PUF)

Pour lier la recette au four, ils utilisent une technologie appelée PUF (Fonction Physiquement Inclonable).

• L'analogie : Imaginez que chaque four a une empreinte digitale unique, causée par de minuscules défauts de fabrication invisibles à l'œil nu (comme des grains de poussière coincés dans les rouages).
• Le fonctionnement : Le logiciel pose une question au four ("Quelle est ton empreinte ?"). Le four répond avec une réponse unique. Si le logiciel est sur le bon four, la réponse est correcte et le gâteau (le programme) se déroule parfaitement. Si le logiciel est sur un autre four, la réponse est différente.

3. Le Dilemme : Sécurité vs Sécurité des Personnes

C'est ici que ça devient intéressant. Si le logiciel détecte qu'il n'est pas sur le bon four, que doit-il faire ?

• L'ancienne méthode (dangereuse) : Elle disait : "Si la réponse est fausse, saute n'importe où !" Cela pouvait faire planter la machine ou, pire, causer un accident (ex: un feu de circulation qui passe au vert pour tout le monde en même temps).
• La nouvelle méthode (sûre) : Les auteurs disent : "Si la réponse est fausse, ne paniquez pas. Choisissez une action sûre au hasard, mais qui ne blesse personne."

4. Le Magicien : L'Exécution Symbolique

Comment savoir quelles actions sont "sûres" sans essayer toutes les possibilités (ce qui prendrait une éternité) ?
Ils utilisent une technique appelée l'exécution symbolique.

• L'analogie : Imaginez un magicien qui ne cuisine pas avec de vrais ingrédients, mais avec des étiquettes magiques ("α", "β"). Il simule des milliers de scénarios en même temps pour voir : "Si je mets l'ingrédient A ici, est-ce que ça explose ? Non. Si je mets B, est-ce que ça brûle ? Non."
• Grâce à ce magicien, le logiciel sait à l'avance : "Si je ne suis pas sur le bon four, je peux choisir n'importe quelle option parmi celles-ci (A, B ou C), car aucune ne causera d'accident."

5. Le Résultat : Un Piratage Impossible (ou très cher)

Si un voleur essaie de copier le logiciel :

1. Il ne peut pas copier l'empreinte digitale du four (le PUF est unique et physique).
2. Si le logiciel tourne sur un faux four, il se comporte de manière imprévisible (il choisit une action sûre au hasard).
3. Pour le voleur, c'est un cauchemar : il ne peut pas deviner la logique du logiciel car elle change à chaque fois. Pour comprendre comment ça marche, il devrait passer des années à analyser le code, ce qui coûte plus cher que la recette elle-même.

En Résumé

Les chercheurs ont créé un système où :

• Le logiciel est lié au matériel comme une clé à une serrure spécifique.
• Si la clé ne tourne pas, la porte ne s'ouvre pas violemment (pas de crash), mais elle s'ouvre sur un couloir de secours sécurisé (comportement sûr mais erratique).
• La sécurité est garantie par un "magicien mathématique" qui a vérifié toutes les issues de secours avant même que le logiciel ne soit lancé.

C'est une façon intelligente de dire : "Vous pouvez copier mon logiciel, mais sans mon four spécial, il ne servira à rien, et il ne fera pas de mal à personne."

Résumé technique

Voici un résumé technique détaillé de l'article « An Approach for Safe and Secure Software Protection Supported by Symbolic Execution » en français.

1. Problématique

L'article aborde le problème critique du vol de propriété intellectuelle (PI) dans l'industrie, en particulier pour les logiciels de contrôle industriel. Les pertes annuelles estimées sont considérables (6,4 milliards d'euros en Allemagne uniquement).

• Le défi : Contrairement au matériel, le logiciel peut souvent être copié à l'identique sans nécessiter de rétro-ingénierie complexe. Les attaquants tentent de répliquer le matériel ou de copier le binaire pour voler la PI.
• La limitation des approches existantes : Les mécanismes de protection actuels, comme ceux basés sur les fonctions physiques non clonables (PUF) dynamiques (ex: Xiong et al.), lient le logiciel au matériel en vérifiant les temps de réponse ou les sommes de contrôle. Cependant, si la réponse du PUF est incorrecte (ou si le logiciel est exécuté sur un matériel non autorisé), ces méthodes peuvent entraîner un comportement imprévisible, des plantages ou des états non sécurisés, ce qui est inacceptable pour les systèmes industriels critiques.
• L'objectif : Développer une méthode de protection par copie qui lie le logiciel à un matériel spécifique via des PUF, tout en garantissant que, même si le logiciel est exécuté sur un mauvais matériel ou avec une réponse PUF erronée, il continue de fonctionner de manière sûre (satisfaisant les contraintes de sécurité), bien que de manière incorrecte et non déterministe.

2. Méthodologie

L'approche proposée repose sur trois piliers technologiques : les Fonctions Physiques Non Clonables (PUF), les Automates d'État Abstraits (ASM) et l'Exécution Symbolique.

A. Modélisation par ASM

Les programmes de contrôle industriel sont modélisés sous forme d'Automates d'État Abstraits (ASM) à états de contrôle. Ces ASM définissent des règles de transition de la forme si Condition alors Mises à jour. Cette formalisation permet de traiter le logiciel comme un programme abstrait exécutable.

B. Liaison Logiciel-Matériel via PUF

Le cœur de la protection consiste à lier les transitions d'états du programme aux réponses uniques d'un PUF intégré au matériel cible.

• Fonctionnement : Lors d'une transition d'état, le programme interroge le PUF avec un défi (challenge) spécifique.
• Comportement sur le matériel cible : Si la réponse du PUF correspond à l'état attendu, la transition se fait normalement.
• Comportement sur un matériel non autorisé (ou PUF défaillant) : Si la réponse est incorrecte, le programme ne plante pas. Au lieu de cela, il choisit non déterministiquement un état de contrôle parmi un ensemble d'états "sûrs" (safePhases). Cela rend le comportement du logiciel illisible et imprévisible pour un attaquant, tout en évitant les catastrophes physiques.

C. Garantie de Sécurité par Exécution Symbolique

C'est la contribution méthodologique majeure. Pour garantir que le choix non déterministe ne mène jamais à un état dangereux (ex: deux feux de circulation verts simultanément), les auteurs utilisent l'exécution symbolique :

1. Analyse : Au lieu d'exécuter le programme avec des valeurs concrètes, on utilise des symboles pour représenter les états et les conditions.
2. Détermination des états sûrs : L'algorithme analyse symboliquement toutes les transitions possibles pour identifier les conditions pathologiques qui violeraient les contraintes de sécurité ($\Psi$).
3. Construction de l'ensemble sûr : L'ensemble des états autorisés en cas d'échec de la vérification PUF est défini comme l'ensemble des états qui ne satisfont pas les conditions de violation de sécurité.
4. Transformation : Le code original est transformé automatiquement pour inclure la logique de vérification PUF et le fallback vers les états sûrs.

3. Contributions Clés

• Approche "Safe-by-Design" : Contrairement aux méthodes précédentes qui risquent de provoquer des plantages en cas d'échec de protection, cette méthode garantit par construction que le logiciel reste dans un état sûr, même lors d'une exécution non autorisée.
• Généralisation aux ASM à états de contrôle : La méthode est formalisée pour s'appliquer à toute classe d'algorithmes spécifiables par des ASM à états de contrôle, une classe très fréquente dans l'industrie (diagrammes d'activité UML, automates finis).
• Algorithme de transformation automatisable : Les auteurs proposent un processus en 7 étapes pour transformer une spécification ASM non protégée en une spécification protégée, en utilisant l'exécution symbolique pour calculer dynamiquement les ensembles d'états sûrs.
• Résistance à la rétro-ingénierie : En rendant le flux de contrôle dépendant d'une réponse matérielle unique et en introduisant du non-déterminisme sûr en cas d'erreur, la tâche de rétro-ingénierie devient extrêmement coûteuse et complexe.

4. Résultats et Évaluation de la Sécurité

L'évaluation de la sécurité (Section 5) examine le modèle de menace où un attaquant possède un accès blanc (white-box) aux binaires et peut tenter de les décompiler ou de les exécuter.

• Analyse Statique : Un attaquant ne peut pas déduire la fonction PUF ni les valeurs correctes de nextCtlState simplement en analysant le binaire ou le code décompilé. La logique de contrôle est masquée par la dépendance au matériel. Reconstruire la logique à partir de zéro serait plus rapide que de casser la protection.
• Analyse Dynamique :
  • Sur un matériel cloné (sans le PUF original), le comportement est non déterministe, rendant le traçage du flux correct impossible.
  • Sur le matériel original, l'attaquant peut suivre le flux, mais cela est long et complexe, surtout pour des systèmes avec de nombreux chemins d'exécution. De plus, les techniques d'analyse dynamique peuvent interférer avec les réponses du PUF (ex: accès mémoire pour les PUF DRAM).
• Conclusion : La protection rend la rétro-ingénierie économiquement non viable pour l'attaquant, car le coût et le temps nécessaires dépassent largement la valeur du logiciel volé.

5. Signification et Perspectives

• Signification Industrielle : Cette méthode offre une solution viable pour la protection de la PI dans l'industrie 4.0, où la sécurité fonctionnelle (ne pas causer de dommages) est aussi importante que la sécurité de l'information. Elle permet de protéger le logiciel sans sacrifier la sûreté de fonctionnement.
• Limitations actuelles : La méthode nécessite actuellement une identification manuelle des états de contrôle et une spécification formelle des contraintes de sécurité. L'étape 7 (calcul des formules logiques) peut générer des expressions complexes affectant les temps de réponse.
• Travaux futurs : Les auteurs prévoient d'automatiser l'identification des états de contrôle et l'application de la méthode à des études de cas industrielles. L'utilisation de solveurs SMT (Satisfiability Modulo Theories) est envisagée pour simplifier les expressions logiques complexes générées par l'exécution symbolique et garantir la performance temps réel.

En résumé, cet article présente une avancée significative en combinant sécurité matérielle (PUF) et vérification formelle (exécution symbolique) pour créer un système de protection de logiciel qui est à la fois robuste contre le vol et intrinsèquement sûr en cas de défaillance ou d'attaque.