Une approche langages pour comprendre et affronter les injections de fautes

Est-ce que votre dernier programme fonctionnerait si je sautais une ligne de code ? Deux ? Si je corrompais une variable aléatoirement ? Alors il ne résiste pas aux _attaques par injection de faute_, qui ciblent le matériel et produisent ce type d'effets. Pour être honnête, rien n'y résiste vraiment. Les efforts pour s'en protéger ont malgré tout bien progressé, principalement (et c'est peut-être contre-intuitif) en durcissant le code, qui se déploie bien plus facilement que le matériel. Naturellement, modéliser l'effet d'une interférence matérielle au niveau d'abstraction d'un programme est fondamentalement une approximation, et des travaux récents ont montré que même les protections contre des modèles au niveau assembleur (les plus courants) peuvent être contournées en abusant des effets micro-architecturaux perdus dans l'approximation. 

Dans cette présentation non-experte, je parlerai des attaques en faute du point de vue langages de programmation, pour montrer comment les fautes et contremesures affectent les programmes. Je déroulerai comment la construction d'un modèle sémantique pour un saut d'instruction vicieux nous amène à une contremesure mixte logicielle/matérielle que l'on peut formellement prouver correcte. Je discuterai brièvement des défis d'implémenter des transformations de sécurité dans la compilateur LLVM, qui comprend à peu près aussi bien la sécurité que le C (i.e., pas du tout). Cette petite histoire contiendra à la fois des règles d'inférence et des relocalisations à l'édition des liens.