Outsourced Control Flow Verification: How to Adapt System Security to Embedded Computing
Vérification externalisée du flot de contrôle: Comment adapter la sécurité système à l’informatique embarquée
Résumé
Embedded systems are often used to accomplish critical tasks in industrial systems such as automobile or aeronautics. Yet, many of them offer a poor hardware and software security. For example, many attacks (buffer overflow, fault injection, etc...) aim to modify software’s behavior in order to lead to an arbitrary code execution. To tackle this, a control flow integrity (CFI) policy can be deployed in order to verify in real time a program’s behavior. But, as it stands, this solution doesn’t match with embedded systems constraints due to an important overhead implied on the target.
In the first part of this thesis, I present an externalized CFI policy for embedded systems. The target code in instrumented to produce a trace during its execution and to send it to an external monitor which verifies if the trace is correct according to a control flow graph extracted by static analysis at compilation time. I evaluated the feasibility of this solution by demonstrating that it is compatible with embedded systems constraints.
The second part of this work is about control flow integrity. Usual CFI policies imply source code analysis in order to create a reference model used to verify execution. Yet, many stu- dies showed the weaknesses of these approach due to many imprecisions in the program’s behavior modelization. In response, i present a solution based on machine learning to deduce a program’s behavior from observed trusted executions. This solution use Alergia algorithm to induce a precise model from execution traces. To validate this approach, the new model’s precision is evaluated and new leads for futures researches are presented.
Les systèmes embarqués sont utilisés pour accomplir des tâches critiques dans les systèmes industriels, l’automobile ou l’aéronautique. Pourtant, beaucoup d’entre eux possèdent une faible sécurité matérielle et logicielle. Par exemple, de nombreuses attaques (dépassement de tampon, injection de faute, etc. . . ) visent à modifier le comportement du logiciel embarqué et mener à une exécution de code arbitraire. Une solution à ce problème est la mise en place d’une politique de vérification de l’intégrité du flot de contrôle (Control Flow Integrity ou CFI) qui vérifie en temps réel le comportement du programme par rapport à l’exécution attendue. Mais une telle solution ne correspond pas en l’état aux contraintes de l’informatique embarquée car elle est coûteuse en terme de temps de calcul.
Dans la première partie de cette thèse j’évalue la pertinence d’une solution externalisée de CFI pour les systèmes embarqués[62]. Celle-ci repose sur l’instrumentation du code source à protéger afin de produire, lors de l’exécution, une trace envoyée à un moniteur externe qui vérifie si elle est en accord avec un graphe de flot de contrôle extrait à la compilation. J’ai évalué la faisabilité de la démarche en démontrant qu’elle était pertinente vis à vis des systèmes embarqués.
La deuxième partie de mes travaux concerne la vérification du flot de contrôle. Les solutions de CFI classiques reposent sur une analyse du code source afin de créer un modèle de référence pour la vérification de l’exécution. Mais de nombreuses études ont démontré les faiblesses de ce modèle car il est difficile de prédire avec précision le comportement du programme. Pour résoudre ce problème, j’ai proposé une solution basée sur l’apprentissage automatique[63] afin de passer d’un modèle de prédiction du comportement à un modèle de déduction du comportement. Cette solution repose sur la mise en place d’un algorithme d’apprentissage capable d’induire un modèle précis à partir de traces réelles d’exécution. Afin de valider cette démarche, l’efficacité du mécanisme d’apprentissage ainsi que la validité et la précision du nouveau modèle sont évalués. Finalement, ces travaux incluent le résultat des expériences menées sur cette nouvelle approche ainsi que des pistes de recherche pour des travaux futurs.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|