Symbolic binary-level code analysis for security. Application to the detection of microarchitectural timing attacks in cryptographic code

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

Analyse symbolique de code binaire pour la sécurité. Application à la détection d’attaques microarchitecturales dans les implémentations cryptographiques Les logiciels informatiques manipulent fréquemment des données secrètes, garantissant généralement leur confidentialité à l’aide de programmes cryptographiques. Dans ce contexte, il est crucial de s’assurer que ces programmes cryptographiques ne peuvent être exploités par un attaquant pour en extraire les données secrètes. Malheureusement, même si les algorithmes cryptographiques sont basés sur des fondations mathématiques solides, leur exécution dans le monde physique produit des effets secondaires pouvant être exploités par un attaquant. En particulier, un attaquant peut exploiter le temps d’exécution d’un programme pour inférer des informations sur ses entrées secrètes, ou pour extraire des données secrètes encodées dans la microarchitecture grâce aux attaques microarchitecturales. Plus récemment, les attaques Spectre ont montré qu’il est aussi possible d’exploiter les optimisations des processeurs — en particulier les mécanismes de spéculation — pour extraire des données secrètes.Dans cette thèse, nous développons des outils d’analyse automatique de programme permettant de vérifier la confidentialité des données secrètes dans les logiciels cryptographiques. En particulier, nous ciblons trois propriétés cruciales pour les programmes cryptographiques : (1) secret-erasure, qui s’assure que les données secrètes sont effacées de la mémoire à la fin d’un programme, (2) constant-time, qui protège des attaques microarchitecturales, (3) speculative constant-time, qui protège contre les attaques Spectre. Ces propriétés ont en commun deux caractéristiques qui les rendent difficiles à analyser. Premièrement, il s’agit de propriétés de paires d’exécution (c’est-à-dire de 2-hypersûreté), ce qui les rend incompatibles avec les outils de vérification habituels (conçus pour la sûreté). Deuxièmement, elles ne sont généralement pas préservées par les compilateurs.Dans cette thèse, notre objectif est de concevoir des outils d’analyse symbolique automatiques, modélisant des paires d’exécution, fonctionnant au niveau du code binaire, incluant les mécanismes de spéculation des processeurs, et passant à l’échelle sur des logiciels cryptographiques existants. Nos analyses sont basées sur l’exécution symbolique relationnelle — une adaptation de l’exécution symbolique à la 2-hypersûreté — que nous complétons avec des optimisations permettant de : (1) la rendre efficace au niveau binaire, et (2) de modéliser de manière efficace la sémantique spéculative des programmes. Nous proposons deux outils open source : Binsec/Rel, un outil pour la recherche de bugs et la vérification bornée de constant-time et secret-erasure ; et Binsec/Haunted, un outil pour détecter des vulnérabilités aux attaques Spectre. Notre évaluation expérimentale montre que nos optimisations permettent une amélioration drastique des performances en comparaison aux approches antérieures : elles diminuent le temps d’analyse, trouvent plus de bugs, et permettent la vérification de primitives cryptographiques jusqu’alors hors de portée des approches antérieures.Nous analysons, grâce à nos outils, un large éventail de primitives cryptographiques et de fonctions utilitaires de bibliothèques open source (telles que Libsodium, OpenSSL, BearSSL and HACL*) pour constant-time (338 binaires), secret-erasure (680 binaires), et Spectre (45 binaires). Au cours de ces travaux, nous découvrons quelques bugs nouveaux, ainsi que des faiblesses dans certaines protections logicielles.