École Nationale Supérieure de
Techniques Avancées

Résumé

Nous présentons une nouvelle méthode d’analyse statique pour calculer un graphe de flot de contrôle sûr et une empreinte mémoire sûre pour un exécutable binaire. Cette analyse utilise une nouvelle technique, l’exécution symbolique abstraite, ainsi qu’un nouvel algorithme d’élimination de flot de données. Nous appliquons cette analyse à l’exécutable binaire d’un noyau embarqué. Cela nous permet de vérifier, sous certaines hypothèses concernant la mémoire, certaines propriétés de sûreté et de sécurité : l’absence de « crashes » du noyau, et l’impossibilité pour les applications d’accéder à la mémoire de celui-ci ou d’altérer son flot de contrôle.