Les attaques en fautes constituent une menace sérieuse pour les applications embarquées. Pour s’en prémunir, le code peut être renforcé par l’insertion de protections visant à détecter ou tolérer des attaques en fautes et la robustesse obtenue doit être évaluée. Dans cette thèse, nous présenterons une approche combinant des analyses statiques et dynamiques de code avec de la vérification formelle et un ensemble de métriques pour évaluer la robustesse d'un code binaire soumis à des attaques en faute. Notre approche modélise la recherche de vulnérabilités par des problèmes d'équivalence-checking résolus par un SMT sovler. L'approche proposée a été implémentée dans un outil, RobustB, qui permet d’analyser la robustesse de code après compilation et qui, grâce aux métriques, permet de comparer des codes intégrants différentes protections et/ou compilés avec différents compilateurs et/ou différents niveaux d’optimisation.