Direction scientifique
Transfert de connaissances vers l'industrie

Nos Thèses par thème

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

Toutes les offres [+]

Algorithmes prouvés de simplification et de résolution pour la preuve de programmes

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

Laboratoire pour la Sûreté du Logiciel

Master en méthodes formelles

01-09-2020

SL-DRT-20-0396

loic.correnson@cea.fr

Cybersécurité : hardware et software (.pdf)

La plateforme Frama-C développée au CEA permet la vérification formelle de programmes critiques. Elle est utilisée de manière industrielle dans différents domaines, comme l'aéronautique ou l'énergie, pour garantir l'absence de défaut de programmes C quelque soient leur conditions d'utilisation. Une garantie d'absence de bug ne peut être obtenue qu'en utilisant des outils de raisonnement automatique, que ce soit des assistants de preuve (Coq, PVS, HOL) ou des solveurs SMT (Z3, CVC4, Alt-Ergo). Pour le passage à l'échelle de ces techniques sur des codes industriels, il est cependant nécessaire de passer par une étape de simplification préalable des objectifs de preuve. Au sein de Frama-C, nous avons pour cela développé le moteur Qed qui est chargé de cette étape critique de simplification. Cela a permis notamment des gains d'automatisation considérables dans l'automatisation des preuves de programmes développés par Airbus, conduisant à la généralisation de cette approche dans leur processus de production industrielle. Depuis ses premiers développements en 2015 le moteur Qed a connu de nombreux perfectionnements qui sont de plus en plus difficiles à developper tout en s'assurant de la correction des simplifications réalisées. Il devient maintenant nécessaire d'automatiser la vérification du moteur Qed lui-même. Le but de la thèse est de re-developper entièrement Qed dans l'environnement de preuve Why-3 en spécifiant et en vérifiant la correction de ses algorithmes de simplification. A terme, le code extrait du développement Why-3 serait utilisé en remplacement complet du moteur actuel au sein de Frama-C.

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

Modèles sûreté/sécurité pour la charactérisation de la sécurité de dispositifs industriels

Département Systèmes (LETI)

Laboratoire Sécurité des Objets et des Systèmes Physiques

Master 2 Cybersecurié

01-10-2020

SL-DRT-20-0594

Cybersécurité : hardware et software (.pdf)

Les systèmes industriels sont souvent utilisés pour surveiller et contrôler un processus physique tel que la production et la distribution d'énergie, le nettoyage de l'eau ou les systèmes de transport. Ils sont souvent simplement appelés systèmes de contrôle de supervision et d'acquisition de données (SCADA). En raison de leur interaction avec le monde réel, la sécurité de ces systèmes est critique et tout incident peut potentiellement nuire aux humains et à l'environnement. Depuis le ver Stuxnet en 2010, ces systèmes font de plus en plus face à des cyberattaques causées par divers intrus, y compris des terroristes ou des gouvernements ennemis[1]. Comme la fréquence de ces attaques augmente, la sécurité des systèmes SCADA devient une priorité pour les organismes gouvernementaux[2]. L'un des principaux axes de recherche en cybersécurité des systèmes industriels porte sur la combinaison des propriétés de sécurité et de sûreté. La sécurité concerne les propriétés applicatives du système (par exemple, les propriétés chimiques d'une usine chimique), tandis que les propriétés de sécurité tiennent compte de la façon dont un intrus peut endommager le système. Comme le montre[3], la combinaison de la sécurité et de la sûreté est un sujet difficile car ces propriétés peuvent être dépendantes, renforçantes, antagonistes ou indépendantes. Comme le montre[4], la combinaison de la sécurité et de la sûreté dans une modélisation commune est un défi, car les deux viennent avec des sources d'explosion combinatoire. De plus, il existe des outils utilisés soit pour les analyses de sécurité, soit pour les analyses de sûreté, mais actuellement aucun outil n'est capable de traiter les deux aspects en même temps. Dans ce contexte, nous proposons une thèse de doctorat autour de la modélisation de systèmes industriels prenant en compte à la fois les propriétés de sécurité du procédé physique et les propriétés de sécurité. En plus de la définition d'un cadre ou d'un langage de modélisation précis, mais analysable automatiquement, de nombreux aspects peuvent faire partie du sujet. Par exemple, des fichiers de configuration d'automates programmables (API) pourraient être générés à partir de ce modèle afin de ne déployer que des programmes préalablement validés. Les vulnérabilités des automates peuvent être étudiées (reverse engineering de firmware, fuzzing de protocole) afin de tester la faisabilité technique des attaques trouvées. Enfin, dans un contexte de certification, les analyses de sécurité sur le modèle pourraient inclure des exigences de normes telles que CEI 62443[5] pour faciliter le processus d'évaluation.

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

Etude de la vulnérabilité des systèmes électroniques de type objet connecté contre les agressions électromagnétiques induites

Département Systèmes (LETI)

Centre d'Evaluation de la Sécurité des Technologies de l'Information

Master elctromagnétisme, électronique analogique

01-09-2020

SL-DRT-20-0830

Cybersécurité : hardware et software (.pdf)

Dans le domaine de l'évaluation des systèmes matériels, le CESTI-Leti évalue leurs résistances vis-à-vis des attaques en perturbation via les techniques classiques (glitch de tension, glitch d'horloge, perturbation par effet photoélectrique, perturbation par effet électromagnétique). Les techniques habituelles permettent d'injecter des fautes sur la cible avec beaucoup de précision mais nécessitent généralement un accès physique privilégié au produit pour être au plus près de la zone à perturber, ce qui n'est pas toujours réaliste. En effet, la technique de perturbation électromagnétique actuellement utilisée au CESTI-Leti nécessite de mettre une bobine à moins de 1mm du produit et à faire passer plusieurs centaines d'ampères pendant une très courte période. Le CESTI souhaite donc développer une méthode de perturbation à distance basée sur l'injection d'ondes électromagnétiques. De son côté le CEA-DAM de Gramat a une longue expertise sur la susceptibilité des systèmes électroniques aux agressions d'origine électromagnétique et aimerait utiliser cette expertise pour évaluer la vulnérabilité d'un système communicant électronique (type objet connecté) vis-à-vis d'une agression électromagnétique. Objectifs Les travaux s'inscriront dans le prolongement de travaux effectués au CEA-DAM de Gramat sur la vulnérabilité des systèmes électroniques au rayonnement électromagnétique qui ont prouvé leur efficacité sur le plan du déni de service temporaire et définitif. ? Il s'agira tout d'abord de faire le lien entre une technologie permettant de perturber un système électronique de façon macroscopique (déni de service) et les technologies couramment utilisées aux CESTI-Leti qui permettent une action plus ciblée. ? Puis il s'agira de développer un démonstrateur de laboratoire permettant de mener des attaques en perturbation sur un objet connecté à une distance de quelques centimètres tout en minimisant la puissance requise pour perturber la cible. Déroulement de la thèse La première partie sera consacrée à une revue de la bibliographie sur les effets des perturbations électromagnétiques sur les systèmes électroniques et l'étude les différents moyens d'émission des perturbations électromagnétiques. Dans la deuxième partie des travaux, les différents moyens sélectionnés seront testés contre différentes cibles représentatives d'objets connectés. Il sera alors nécessaire de mesurer l'impact des perturbations sur les différents systèmes et d'en déduire un modèle. La dernière partie sera consacrée au développement d'un générateur de puissance réduite garantissant la sécurité de personnel se trouvant à proximité. Le Leti mettra à disposition les plateformes à évaluer ainsi que le support pour réussir à exploiter les perturbations pour mener une attaque complète sur un objet connecté. Le centre CEA-DAM de Gramat mettra à disposition ses plateformes d'essais permettant de générer des fautes via les rayonnements électromagnétiques ainsi que son savoir-faire sur le domaine qui permettra de développer un prototype adapté aux besoins des expérimentations.

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

Construction systématique et interprétation de modèles de fuites électromagnétiques pour des processeurs embarqués

Département Systèmes (LETI)

Laboratoire Sécurité des Objets et des Systèmes Physiques

Bac +5 Microélectronique ou mathématique

01-10-2020

SL-DRT-20-0838

maxime.lecomte@cea.fr

Cybersécurité : hardware et software (.pdf)

Les attaques par canaux auxiliaires ou side-channel consistent à mesurer l'activité physique émise par un circuit (processeur, micro contrôleur ou accélérateurs cryptographique) dans le but d'en extraire des secrets. La consommation du circuit ou le champ électromagnétique émis sont les phénomènes les plus couramment exploités. Avec le développement de l'Internet des objets (IoT), de plus en plus de systèmes sont exposés à ces attaques. Malheureusement, intégrer des contremesures (logicielles ou matérielles) contre de telles attaques est extrêmement couteux. C'est pourquoi, il est essentiel d'avoir une idée précise des fuites side-channel aussi tôt que possible dans les phases de conception. D'une part pour cibler les contremesures sur les zones critiques et d'autre part pour avoir une vision réaliste des fuites dans le but d'automatiser l'application de contremesures. Cette thèse porte sur l'exploration des modèles de fuites électromagnétiques et des différentes manières de les interpréter. L'objectif général de ces travaux est de modéliser les fuites d'un processeur à partir de son état à différents niveaux d'abstractions : Register Transfert Level (RTL), micro-architecture ou encore au niveau simulateur de jeu d'instruction (ISS). Le laboratoire LSOSP du CEA-LETI où se déroulera la thèse a une forte expérience sur les mesures physiques et déjà effectué des recherches préliminaires sur le sujet. Le candidat partira donc de ces résultats et sera amené à effectuer des mesures physiques sur circuit et à manipuler différent modèles logiques afin d'en créer un modèle de fuite précis.

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

Impact de la micro-architecture sur les protections contre les attaques par canal auxiliaire

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

Laboratoire Infrastructure et Ateliers Logiciels pour Puces

master ou école d'ingénieur informatique

01-09-2020

SL-DRT-20-0921

nicolas.belleville@cea.fr

Cybersécurité : hardware et software (.pdf)

La thèse se place dans le contexte de la cyber-sécurité des systèmes embarqués et objets connectés. Elle concerne plus précisemment l'application de contre-mesures à la compilation contre les attaques par canaux auxiliaires exploitant la consommation électrique ou les émissions électromagnétiques, qui représentent une forte menace pour ces systèmes. Pour appliquer les contre-mesures contre ces attaques, on utilise souvent un modèle de fuite, qui modélise comment les fuites par canal auxiliaire sont liées au programme et aux données manipulées par le processeur. Un modèle infidèle ne permet pas d'appliquer la contre-mesure de manière efficace. Les modèles actuellement utilisés sont insuffisants dès lors qu'ils ne prennent pas en compte la micro-architecture des composants. En effet, la micro-architecture et notamment les éléments invisibles au niveau assembleur (registres ou tampons cachés) peuvent induire des fuites. L'objectif de cette thèse sera d'étudier l'impact de la micro-architecture sur l'application automatisée des contre-mesures contre les attaques par canal auxiliaire à la compilation. Un premier axe est d'étudier comment modifier la manière d'appliquer les contre-mesures au sein du compilateur pour prendre en compte des modèles de fuites précis tenant compte de la micro-architecture, par exemple comment adapter la sélection d'instructions ou l'allocation de registres dans le compilateur en fonction du modèle de fuite. Un second axe est d'adapter les contre-mesures elles-mêmes afin de mieux prendre en compte la nature des fuites, dans l'objectif de réduire les fuites d'information plus efficacement et d'améliorer le compromis sécurité / performance.

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

Analyse mémoire précise et efficace pour les languages de bas niveau

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

Laboratoire pour la Sûreté du Logiciel

Master en informatique, avec une formation en méthode formelle ou sémantique des languages de programmation (compilation). La connaissance des languages fonctionnels (OCaml,Haskell,Lisp) et/ou bas-niveau (C, assembleur) est un plus.

01-10-2020

SL-DRT-20-1088

matthieu.lemerre@cea.fr

Cybersécurité : hardware et software (.pdf)

Le but de la thèse est de développer une analyse statique automatique (basée sur l'interprétation abstraite) permettant de vérifier l'absence d'erreurs mémoire dans des langages bas-niveau compilés (de type C, C++, assembleur, Rust). Cette problématique est très importante pour la cybersécurité, car la plupart des erreurs de sécurité liées au logicielles proviennent d'erreurs de sûreté mémoire (buffer overflows, use-after-free, mauvaises conversions de pointeurs). Les trois grands problèmes lorqu'on conçoit une telle analyse statique automatique est de demander un faible effort de vérification de la part de l'utilisateur, de gérer des systèmes larges et complexes, et d'être assez précis pour que l'analyse ne rapporte pas un grand nombre de fausses alarmes. Nous reposons sur le succès d'une nouvelle méthode utilisant des domaines abstraits paramétrés par des invariants de type, qui permis en particulier de prover entièrement automatiquement l'absence d'erreurs mémoire d'un micronoyau industriel existant à partir de son code machine, en utilisant seulement 58 lignes d'annotations; et nous cherchons à étendre cette analyse à des systèmes plos gros. En particulier, l'analyseur devrait être étendu pour améliorer le passage à l'échelle (en utilisant une analyse compositionelle), pour améliorer la précision (en utilisant la logique de séparation et des domaines abstraits de formules), et pour réduire encore plus le nombre d'annotations (en inférant automatiquement des invariants de type plus précis)

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

Dossier d'assurance de sécurité pour les systèmes basés sur l'IA

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

Labo.conception des systèmes embarqués et autonomes

Master 2 en informatique

01-10-2020

SL-DRT-20-1206

morayo.adedjouma@cea.fr

Cybersécurité : hardware et software (.pdf)

L'utilisation de systèmes basés sur l'intelligence artificielle (IA) se développe rapidement et trouve des utilisations dans de nombreuses industries. Cela est particulièrement vrai pour les systèmes autonomes, où les déploiements ciblent de plus en plus des exigences importantes, voire critiques, mais dont les défaillances entraîneraient des conséquences indésirables ou intolérables. La pratique actuelle consiste à suivre un processus de certification fastidieux pour démontrer que le système est sécurisé pour permettre son déploiement. Fournir un argument convaincant en matière de sécurité logicielle comme brique pour créer des cas d'assurance pour la sécurité du système est une partie fondamentale mais difficile de cette démonstration. Une partie du problème réside dans le besoin de fournir des preuves pour justifier des propriétés systèmes où des techniques de vérification formelles telles que le model-checking sont recommandés pour une évaluation efficace. Il est également difficile de structurer l'argument couvrant l'ensemble du système de manière lisible et réutilisable. De plus, étant donné que les systèmes basés sur l'IA peuvent acquérir de nouvelles aptitudes en phase opérationnelle, - aptitudes non prises en compte lors de leur développement - pour pouvoir réagir correctement aux environnements changeants, incertains et inconnus, on ne peut pas définir le dossier d'assurance uniquement sur les artefacts produits au cours d'un processus de développement adéquat. Dans nos travaux précédents, nous avons étudié l'ingénierie, la validation et l'évaluation de la cybersécurité dans le contexte des infrastructures critiques, des systèmes cyberphysiques et distribués. L'objectif principal de cette thèse est de poursuivre sur ces travaux en considérant le cas où certains composants logiciels des systèmes utilisent l'intelligence artificielle (IA), en particulier les algorithmes et techniques d'apprentissage automatique. La thèse contribuera à cette problématique en décrivant un support méthodologique pour construire et réutiliser des cas d'assurance de sécurité sous la forme de modèles réutilisables dans le contexte de l'architecture système des systèmes basés sur l'IA et de leur interaction avec les propriétés de sécurité. Cela impliquera de développer (1) un cadre de conception pour spécifier et vérifier formellement la sécurité des systèmes basés sur l'IA, (2) une structure d'argumentation pour raisonner sur la sécurité de ces systèmes et (3) des approches pour générer des preuves suffisantes pour soutenir les revendications de l'argumentaire. A partir de cela, la thèse proposera des principes génériques pour générer des explications et des preuves à communiquer aux autorités réglementaires, aux organismes de certification et aux éventuels utilisateurs de ces systèmes, à les comprendre et à les accepter.

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

Voir toutes nos offres