Protections vérifiées formellement par ordinateur contre les attaques par canaux auxiliaires basées sur le temps ; Formally computer-verified protections against timing-based side-channel attacks
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Protections vérifiées formellement par ordinateur contre les attaques par canaux auxiliaires basées sur le temps ; Formally computer-verified protections against timing-based side-channel attacks
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 ...