Formally computer-verified protections against timing-based side-channel attacks

Protections vérifiées formellement par ordinateur contre les attaques par canaux auxiliaires basées sur le temps Les développeurs de logiciels critiques cherchent à concevoir des logiciels fonctionnellement corrects, dotés de propriétés telles que la confidentialité. Cependant, la confidentialité n'est pas une conséquence directe de la correction fonctionnelle, car il peut y avoir des fuites par canaux auxiliaires, comme le temps d'exécution, qui peuvent aider l'attaquant à récupérer des données secrètes.Par exemple, un algorithme de comparaison de chaînes de caractères qui compare deux chaînes caractère par caractère et se termine en cas de non-concordance ou renvoie un succès lorsque les chaînes sont égales est un algorithme fonctionnellement correct pour vérifier un mot de passe. Cependant, un attaquant peut deviner la longueur du mot de passe en mesurant le temps d'exécution de l'algorithme, ce qui montre qu'il n'est pas protégé contre les attaques par mesure de temps. Plus généralement, le branchement sur des secrets peut entraîner une fuite de données secrètes, car les deux branches peuvent avoir des temps d'exécution différents. Les processeurs modernes utilisent la prédiction de branchement pour maximiser la performance des programmes. Par exemple, si la destination d'une condition de branchement conduit à une lecture en mémoire, le processeur contourne la vérification de la condition et exécute l'opération de lecture en mémoire de manière spéculative. En cas d'erreur de prédiction, le processeur revient en arrière et recommence l'exécution avec le résultat correct de l'évaluation de la condition. Bien que le retour en arrière corrige les résultats spéculatifs, il laisse cependant une trace dans le cache, que l'attaquant peut exploiter pour accéder aux données secrètes (illustré dans les attaques Spectre). Ainsi, la spéculation améliore la performance globale au détriment de la sécurité.Les effets des canaux auxiliaires ne sont pas pris en compte dans la sémantique formelle classique des programmes et, par conséquent, cette sémantique ne peut pas être utilisée pour raisonner sur les hyperpropriétés telles que les attaques par canaux auxiliaires basées sur le temps. Sans la notion de modèles formels prenant en compte les effets secondaires produits au cours de l'exécution d'un programme, les développeurs ne peuvent que corriger manuellement le programme pour s'assurer qu'il prenne toujours le même temps pour s'exécuter et supposer que le compilateur ne casse pas la propriété lors de la compilation, sans garantie formelle, du programme vers l'assembleur. Traditionnellement, les cryptographes ont utilisé la propriété de temps constant pour se défendre contre les attaques par canaux auxiliaires basées sur le temps. Un programme à temps constant n'effectue pas d'accès mémoire ni de branchement dépendants du secret. Malheureusement, les optimisations effectuées par le compilateur pour accroître l'efficacité du programme ont tendance à casser la propriété de temps constant. Tout ceci plaide pour l'existence d'un modèle formel qui capture les effets secondaires produits pendant l'exécution d'un programme.Cette thèse vise à fournir des modèles formels prenant en compte les effets secondaires produits lors de l'exécution d'un programme, ainsi que des définitions formelles de propriétés de sécurité, comme le temps constant et le temps constant spéculatif. La thèse inclut le développement d'un compilateur sécurisé, formellement vérifié, qui préserve la propriété de temps constant, et des méthodologies pour ajouter des protections contre différentes formes d'attaques Spectre. Elle définit des systèmes de types qui permettent de vérifier l'utilisation correcte de ces protections et illustre une méthode efficace de protection contre les attaques Spectre v1 appelée Selective Speculative Load Hardening. Tous ces travaux sont formellement vérifiés en utilisant l'assistant de preuve Coq, leur donnant la solidité des preuves vérifiées par ordinateur.