Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée – ProMiS

La vulnérabilité Spectre, affectant les derniers processeurs, a été récemment découverte. Un attaquant peut extraire des informations privées via une attaque temporisée. Il s'agit d'un cas d'attaque par canal auxiliaire, où des information fuitent non intentionnellement. Il est essentiel de prévenir de telles attaques.

Nous proposons de mitiger les attaques par canal auxiliaire (p.ex. temporisée ou par cache) en utilisant des techniques formelles de vérification. L'idée est de réduire ce problème à celui de la synthèse de paramètres pour un certain formalisme (p.ex. des variantes du formalisme bien connu des automates temporisés paramétrés). Étant donné un programme ou système avec des paramètres pouvant être modifiés pour éviter les attaques par canaux auxiliaires, notre approche consiste à automatiquement synthétiser des valeurs de ces paramètres garantissant la sécurité.
Nous allons utiliser une approche en 3 phases :
1. définir formellement le problème des attaques par canal auxiliaire temporisé;
2. proposer des algorithmes optimisés pour le model-checking paramétré dédiés à la vérification de fuites d'information;
3. proposer des optimisations et des méthodes traduisant des systèmes ou programmes réels vers notre formalisme afin d'obtenir un passage à l'échelle effectif.
Nous développerons une suite logiciel pouvant être automatiquement appliquée à des études de cas réelles incluant celles du challenge DARPA.
Ce projet bénéficiera de la synergie de 5 chercheurs dans 4 laboratoires partenaires, avec une expertise complémentaire en sécurité, méthodes formelles et analyse de programmes.