Direction scientifique
Transfert de connaissances vers l'industrie

Les Post-Docs par thème

Défis technologiques >> Cybersécurité : hardware et software
3 proposition(s).

Voir toutes nos offres

Chiffrement homomorphe pour la confidentialité dans les réseaux de neurones à base de plongements

Département Architectures Conception et Logiciels Embarqués (LIST-LETI)

Laboratoire composants logiciels pour la Sûreté et la Sécurité des Systèmes

PhD in cryptography or machine learning

01-01-2020

PsD-DRT-20-0021

renaud.sirdey@cea.fr

L'IA émerge actuellement comme la « killer application » de la cryptographie homomorphe ou FHE. En effet, ce type de cryptographie, qui permet de réaliser des calculs directement sur des données chiffrées, a le potentiel de garantir par construction la confidentialité des données utilisateurs et/ou des modèles d'intelligence artificielle, selon les scénarios de déploiement. A plus long terme, le FHE pourrait protéger aussi les données d'apprentissage, débloquant de nouveaux usages de partage de données. Dans ce contexte, le présent postdoctorat vise à investiguer l'utilisation pratique du chiffrement homomorphe dans le cadre d'un type particulier de réseau de neurones, les réseaux à base de plongements (embeddings), qui sont, pour des raisons intrinsèques, à la fois favorables à l'obtention de bonnes performances d'exécution homomorphes mais également d'une portée applicative importante. Ainsi, le présent postdoctorat étudiera des aspects théoriques et pratiques selon plusieurs scénarios d'intégration du chiffrement homomorphe et donnera lieu à un travail de prototypage sur la base d'un système de reconnaissance de locuteurs de référence, disponible en open-source et justement basé sur un réseau à base de plongement.

Télécharger l'offre (.zip)

Vérification à l'exécution avancée sur des programmes C

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

PhD in formal methods

01-10-2020

PsD-DRT-20-0094

Julien.Signoles@cea.fr

Frama-C est une plateforme d'analyse de code C. E-ACSL est le greffon de Frama-C dédié à la vérification à l'exécution. Il convertit un programme C étendu avec des annotations formelles en un nouveau programme C qui vérifie la validité des annotations pendant l'exécution du programme: ce dernier se comporte d'une manière équivalente au programme initial lorsque toutes les annotations sont valides, ou échoue (par défaut) dès qu'une annotation est fausse. Une caractéristique d'E-ACSL est l'expressivité de son langage de spécification qui permet d'exprimer de nombreuses propriétés de sûreté et de sécurité. Une autre caractéristique est l'efficacité du code généré qui repose sur une bibliothèque et des analyses statiques dédiée. Néanmoins, de nombreuses questions de recherche restent ouvertes pour aller au delà de l'état de l'art et améliorer significativement E-ACSL : - vérification à l'exécution de définitions axiomatiques - vérification à l'exécution de propriétés localisées qui se rapportent à différents points de programme - vérification à l'exécution de "frame conditions" et de propriétés de dépendances de données - vérification à l'exécution de propriétés sur des nombres réels - analyses statiques pour l'optimisation de moniteurs Dans le contexte du projet européen H2020 ENSUREC (2020-2022) qui vise à protéger le e-commerce avec du monitoring, le postdoc collaborera avec d'autres ingénieurs et chercheurs du laboratoire et, possiblement, d'autres organismes de recherche dans le but d'adresser plusieurs des problèmes ci-dessus. Elle ou il définiera, formalisera et implémentera des solutions innovantes tout en prouvant leurs corrections.

Télécharger l'offre (.zip)

Analyse approfondie pour la sécurité des codes avec Frama-C

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

PhD in formal methods and/or in security of code

01-10-2020

PsD-DRT-20-0095

Julien.Signoles@cea.fr

Frama-C est une plateforme d'analyse de code C. Dans le contexte du projet européen H2020 ENSURESEC (2020-2022) qui vise à protéger le e-commerce, nous planifions d'utiliser Frama-C pour détecter des menaces dans les interfaces cyber comme des intergiciels, des bibliothèques cryptographiques ou des implémentations de protocoles de communication. Le postdoc adaptera des greffons existants de Frama-C et/ou en développera de nouveaux dans ce but. Entre autres, un sujet important est la sécurité des flots d'information pour y détecter des fuites. Dans ce contexte, des solutions à envisager sont : - l'interprétation abstraite en définissant un nouveau domaine dédié dans Frama-C; - la vérification à l'exécution en bénéficiant des bits aujourd'hui inutilisés de la mémoire d'ombre de Frama-C - l'extention et l'amélioration du greffon SecureFlow de Frama-C dédié à la vérification des flots d'information et qui permet de combiner analyses statiques et dynamiques. Un autre sujet d'intérêt est la vérification de politiques de contrôle d'accès qui pourrait être effectuée via SecureFlow et/ou le greffon MetACSL dédié à la spécification formelle de propriétés globales d'un programme. Définir un nouveau greffon dédié est aussi envisageable. Le postdoc devra formaliser et coder ses solutions, prouver leur correction et les évaluer sur des cas d'étude réalistes (par exemple, fournit par des partenaires industriels du projet ENSURESEC).

Télécharger l'offre (.zip)

Voir toutes nos offres