2020-02890 - Une infrastructure de vérification pour l’apprentissage machine sécurisé

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Ingénieur scientifique contractuel

Mission confiée

L’apprentissage machine utilise massivement des données utilisateurs (incluant des données personelles) pour produire des modèles analytiques, qui sont ensuite utilisés pour faire des décisions de classification sur des nouvelles données sans intervention humaine. Alors que les applications de l’apprentissage machine deviennent de plus en plus sophistiquées, la sécurité et la confidentialité des données dans ce contexte ont reçues moins d’attention. Avec l’apprentissage machine préservant la vie privée (Privacy Preserving Machine Learning, PPML), un tel classifieur (sur un serveur) doit traiter les requêtes de l’utilisateur de manière opaque, et ne rien apprendre sur la requête ni sur la réponse. Un client doit seulement apprendre la réponse associée à sa requête, et ne doit rien apprendre sur le modèle.
Atteindre ces objectifs, aussi simples qu’ils paraissent, se trouvent être difficiles et coûteux en pratique, et sont un domaine actif de recherche.

Principales activités

Notre but dans ce projet est de faire une implémentation vérifiée de SPDZ2k, un protocole de calcul multi-parti sécurisé, dans le but de l’appliquer au PPML.
L’implémentation et la vérification se fait en F*, un langage fonctionnel type ML avec un système de type incluant polymorphisme, types dépendants, effets monadiques, sous-typage. Ce langage a pour but la vérification via un solveur SMT, et peut ensuite être compilé en OCaml, F#, C ou même WebAssembly.


Une spécification haut-niveau et bas-niveau du protocole étant déjà écrites, nous avons les objectifs suivants :
— Preuve de sécurité de la spécification bas-niveau

— Écriture et preuve de l’implémentation bas-niveau

— Application au PPML

Avantages

  • Restauration subventionnée
  • Transports publics remboursés partiellement
  • Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
  • Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
  • Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
  • Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
  • Accès à la formation professionnelle
  • Sécurité sociale