Atteignabilité robuste et comptage de modèles pour la sécurité logicielle

Autor: Girol, Guillaume
Přispěvatelé: Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Université Paris-Saclay, Sylvain Conchon, Sébastien Bardin
Jazyk: angličtina
Rok vydání: 2022
Předmět:
Zdroj: Cryptography and Security [cs.CR]. Université Paris-Saclay, 2022. English. ⟨NNT : 2022UPASG071⟩
Popis: Modern bug-finding techniques have become effective enough that the bottleneck is not finding bugs but finding the time to fix them. A popular way to address this problem is to focus first on bugs with a security impact, also known as vulnerabilities. This leads to the question of vulnerability assessment: could an attacker take advantage of a bug? In this thesis we attempt to assess one particular dimension contributing to the security impact of a bug: whether an attacker could trigger it reliably. We call this property replicability. Our goal is to formalize replicability to design bug-finding techniques which only report bugs which are replicable enough. We do so by considering a threat model where inputs to the program which the attacker can choose (like network inputs) are distinguished from inputs which the attacker does not control nor know (like entropy sources). We propose two approaches to replicability. Firstly, we define robust reachability, a qualitative property that expresses that a bug is not only reachable, but that when he chooses the right inputs, the attacker triggers the bug whatever the values of the program inputs he does not control. Secondly, we refine robust reachability quantitatively as the proportion of uncontrolled inputs that let the optimal attacker trigger the bug. We adapt symbolic execution to prove robust reachability and compute this proportion. Robust reachability is more coarse-grained because it is all-or-nothing but scales better than the quantitative approach. We illustrate in case studies the potential applications of these techniques, notably in terms of vulnerability assessment.; Les techniques modernes de recherche de bugs sont devenues si efficaces que le problème n'est plus de trouver des bugs mais de trouver le temps de les corriger. Une façon répandue d'éluder ce problème est de concentrer l'effort de correction de bug prioritairement sur les bugs ayant un impact en termes de sécurité, aussi désignés sous le nom de vulnérabilités. Cela conduit naturellement à la question de l'évaluation de cet impact: un attaquant pourrait-il tirer parti de tel ou tel bug ? Cette thèse se concentre sur une dimension particulière de ce problème: un attaquant serait-il capable de déclencher ce bug ? Nous appelons cette propriété la réplicabilité. Nous nous fixons pour objectif de concevoir des méthodes de recherches de bugs qui ne détectent que des bugs suffisamment réplicables. Le point de départ est de considérer des modèles de menace où l'on distingue les entrées du programme qui peuvent être choisies par l'attaquant (comme les entrées réseau) de celle qui ne peuvent ni être contrôlées ni connues de lui (comme les sources d'entropie). Nous proposons deux approches pour évaluer la réplicabilité. D'abord, nous définissons l'atteignabilité robuste, une propriété qualitative qui exprime qu'un bug est non seulement atteignable mais que lorsqu'il choisit les entrées qu'il peut correctement, l'attaquant déclenche toujours le bug, indépendamment des valeurs des entrées qu'il ne peut pas choisir. Dans un second temps, nous affinons cette approche en une approche quantitative où nous déterminons la proportion d'entrées non contrôlées qui permettent à l'attaquant optimal de déclencher le bug. Nous adaptons ensuite l'exécution symbolique pour prouver l'atteignabilité robuste ou bien calculer cette proportion. L'atteignabilité robuste est une analyse moins fine que cette approche quantitative parce qu'elle est "tout ou rien", mais en contrepartie elle passe mieux à l'échelle. Enfin nous illustrons dans des études de cas les applications potentielles de ces concepts, en particulier à l'évaluation de vulnérabilité.
Databáze: OpenAIRE
Externí odkaz: