Quantification of the security of applications in the presence of physical attacks and detection of attack paths

Les systèmes embarqués traitent et manipulent de plus en plus de données sensibles. La sécurité de ces systèmes est une préoccupation de premier ordre pour ceux qui les conçoivent. Les attaques en fautes visent à perturber l'exécution des programmes à travers la manipulation de grandeurs physiques dans l'environnement du système. Des contre-mesures logicielles sont déployées pour faire face à cette menace. Différentes analyses sont actuellement utilisées pour évaluer l'efficacité des contre-mesures une fois déployées mais elles sont peu ou pas automatisées, coûteuses et limitées quant à la couverture des comportements possibles et aux types de fautes analysables. Nous proposons une méthode d'analyse de robustesse de code binaire combinant des méthodes formelles et de l'exécution symbolique. L'analyse au niveau du code binaire permet non seulement de se placer après la compilation, qui peut altérer les contre-mesures, mais aussi de prendre en compte des éléments du code binaire invisibles à plus haut niveau. Les méthodes formelles, capables d'exhaustivité, permettent à l'analyse de considérer toutes les configurations des paramètres d'entrée. L'analyse est toutefois réalisée vis-à-vis d'un contexte symbolique, extrait par exécution symbolique, ce qui la circonscrit à des paramètres d'entrée réalistes et limite ainsi les faux positifs. Nous avons implémenté cette méthode dans un outil, nommé \texttt{RobustB}, automatisé depuis le code source. Nous proposons trois métriques permettant de synthétiser les résultats de l'analyse et d'aider le concepteur de contre-mesures à évaluer la sensibilité globale du code ainsi qu'au niveau de chaque instruction.Embedded systems are processing and handling more and more sensitive data. The security of these systems is now a prime concern for those who designs them. Fault attacks are indented to disrupt the execution of programs through the manipulation of physical quantities in the system environment and enable an attacker to bypass security mechanisms or achieve privilege escalation. Software counter-measures are deployed to address this threat. Various analyses are now being used to assess the efficiency of the counter-measures once deployed but they are little or not automated, costly and limited in terms of code coverage of the possible behaviour and of faults types that can be analysed. We propose a method to analyse the robustness of binary code combining formal methods and symbolic execution. Performing the analysis at the binary positions the analysis after compilation which can affect the counter-measures and allows it to take into account information which is only visible at the binary level and which can be exploited to perform an attack. Formal methods are capable of exhaustiveness and thus allow the analysis to consider all possible configurations of inputs. The proposed analysis is nevertheless carried out with respect to a symbolic context, extracted by symbolic execution, which confines it to a realistic set of inputs and thus limits false positives. We have implemented this method in a tool called \texttt{RobustB}. It is automated from the source code. We propose three metrics synthesising the analysis results and helping the designer of counter-measures to assess the sensitivity of the code as a whole and at the granularity of an instruction