Direction scientifique
Transfert de connaissances vers l'industrie

Nos Thèses par thème

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

Toutes les offres [+]

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-2021

SL-DRT-21-0031

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)

Attestation d'un temps écoulé dans un dispositif embarqué

Département Systèmes (LETI)

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

bac+5 / M2 sécurité des systèmes embarqués, cyber-sécurité, cryptographie

01-10-2021

SL-DRT-21-0089

christine.hennebert@cea.fr

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

Avec l'émergence d'un protocole sécurisant un historique de transactions sur un réseau de pair-à-pair, Bitcoin a introduit en 2009 la première crypto-monnaie numérique et décentralisée. La sécurité du protocole Bitcoin s'appuie sur la preuve de travail et sur des règles et procédures communes aux pairs du réseau voulant participer au consensus, c'est-à-dire au choix du prochain bloc de données qui sera ajouté au ledger partagé et répliqué. La preuve de travail présente deux inconvénients majeurs. D'une part, elle assure la sécurité par construction en requérant des n?uds participants au consensus un travail dont l'intensité correspond au maximum de la loi de Moore, ce qui est évidemment très consommateur d'énergie. D'autre part, la parallélisation de ce processus de preuve avec une implémentation dans des ASICs rend le système vulnérable à des attaques de type Sybil en recentralisant les ressources. Cette vulnérabilité est exploitée par les pools de mining. Le présent sujet de thèse vise à construire une preuve destinée à l'embarqué et aux objets contraints en ressources, qui assure la sécurité d'un historique de transactions à faible consommation. Le travail se concentrera sur l'implémentation embarqué du mécanisme de preuve sur une plateforme de type « system-on-module » en s'appuyant sur une composant matériel de sécurité de type TPM 2.0 (Trusted Platform Module) comme racine de confiance (« root-of-trust »). La solution introduite devra être robuste aux inconvénients et vulnérabilités précités.

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

Conception automatique d'architectures matérielles sécurisées

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Environnement de Conception et Architecture

Master 2 en cybersécurité

01-10-2021

SL-DRT-21-0190

caaliph.andriamisaina@cea.fr

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

Les systèmes embarqués sont de plus en plus omniprésents et interconnectés, ils sont une cible attrayante pour les attaques de sécurité. L'aspect sécurité devient ainsi de plus en plus important lors de la conception de ces systèmes dans la mesure où une vulnérabilité dans un système peut compromettre toute une infrastructure de systèmes connectés. Ainsi, chaque système contribue à la construction d'une chaine globale de confiance. En outre, étant donné la complexité croissante des applications qui fonctionnent sur ces systèmes, il devient de plus en plus difficile de répondre à tous les critères de sécurité (par exemple, le cloisonnement d'applications, l'authentification des systèmes, la protection des données secrètes et privées, la protection des communications). La conception de ces systèmes nécessite donc une analyse approfondie des différentes contraintes de sécurité auxquelles ils sont soumis en fonction d'un modèle de menaces associé à l'attaquant potentiel. Alors que les objectifs de conception extra-fonctionnelle tels que la performance, la consommation de puissance et la surface sont généralement bien pris en compte dès les toutes premières étapes de la conception des systèmes embarqués, la sécurité est encore généralement considérée à posteriori, ce qui conduit à des solutions de sécurité vues comme des ajouts au système initial. Cette approche de conception doit être repensée afin de développer des solutions intégrant la sécurité par construction et non plus comme un élément additionnel venant a posteriori ajouter certaines fonctions de sécurité. L'objectif de cette thèse est donc de prendre en compte les contraintes de sécurité en plus des contraintes de performance, de consommation de puissance et de surface lors de l'étape d'exploration de l'espace de conception (DSE) des architectures matérielles afin de générer automatiquement une architecture optimisée vis-à-vis de toutes ces contraintes. Cette étude débutera par une analyse des modèles de menaces notamment vis-à-vis des attaques matérielles et des contre-mesures existantes au niveau matériel. Un travail sur les méthodes permettant de modéliser et quantifier la sécurité dans le cadre d'une étape de DSE devra également être mené dans la mesure où il sera indispensable de bien caractériser les techniques et approches permettant de prendre en compte les besoins de sécurisation des systèmes. De cette étape, le candidat proposera un flot de DSE d'architectures matérielles prenant en compte les contraintes de sécurité, en plus des contraintes de consommation de puissance, de performance et de surface. Il s'agira de pouvoir analyser les compromis sécurité, surface, consommation et performance en fonction des spécifications des concepteurs à la fois au niveau fonctionnel et non fonctionnel. Ce flot sera ensuite appliqué à un cas concret de conception d'architecture matérielle afin de valider l'approche DSE développée. Les solutions développées devront, vis-à-vis de la contrainte sécurité, démontrer leur niveau de robustesse afin de garantir la sécurité des systèmes tout en respectant et optimisant les autres contraintes de conception.

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

Preuve d'équivalence fonctionnelle de codes binaires dans le cadre de la sécurisation de programmes

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Fonctions Innovantes pour circuits Mixtes

Master 2 informatique

01-10-2021

SL-DRT-21-0192

damien.courousse@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 des objets connectés, plus particulièrement de leur sécurisation contre les attaques physiques (attaques par canal auxiliaire et attaques par injection de fautes). Le CEA List développe une chaîne de compilation basée sur LLVM, COGITO, pour l'application automatisée de contre-mesures contre les attaques physiques. Deux éléments sont cruciaux pour renforcer la confiance dans la robustesse des contre-mesures appliqués dans les programmes binaires compilés : 1. la preuve de robustesse des contre-mesures mises en ?uvre, 2. la preuve que l'ajout de contre-mesures au programme cible n'en modifie pas la fonctionnalité. Cette thèse ciblera le deuxième point : pouvoir apporter des garanties formelles sur la conformité fonctionnelle d'un programme sécurisé. Notre approche visera à prouver l'équivalence fonctionnelle du programme sécurisé à un autre programme de référence. Nous utiliserons BINSEC (), une plate-forme open-source d'analyse de code binaire développée au CEA List s'appuyant sur l'état de l'art en matière d'analyse de code binaire et de méthodes formelles. La thèse se déroulera sur le centre de Grenoble du CEA, dans un environnement pluridisciplinaire : cyber-sécurité, conception logicielle et matérielle de circuits, intelligence artificielle, etc. Plusieurs séjours courts seront prévus pour assurer une étroite collaboration avec l'équipe de recherche qui travaille sur BINSEC, basée sur le centre de Saclay du CEA.

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

Vérification formelle de la micro-architecture pour l'analyse des effets des injections de fautes et de la robustesse de contre-mesures

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Environnement de Conception et Architecture

Master 2 recherche (cyber-sécurité ou architecture)

01-10-2021

SL-DRT-21-0276

Mathieu.Jan@cea.fr

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

La course sans fin vers l'accroissement des performances en moyenne des systèmes numériques engendre une augmentation perpétuelle de la complexité des architectures matérielles modernes. Ceci met en danger la conception de systèmes embarqués sécurisés via l'ouverture de nouveaux vecteurs d'attaques. Par exemple, la famille d'attaque de type Spectre a mis en lumière les problèmes que peuvent poser les mécanismes de spéculation d'exécution des architectures matérielles. Dans le contexte de cette proposition de thèse, nous considérons que plus l'architecture d'un processeur est complexe, plus la surface d'attaque par injection de fautes est importante. De telles attaques, mises en ?uvre par le biais de perturbations sur les circuit numériques, visent à exploiter la perturbation logique générée au niveau du calcul pour atteindre différents objectifs: réaliser une fuite d'informations, contourner des procédures d'authentification, réaliser une escalade de privilèges, etc. La modélisation des effets logiques d'une perturbation physique sur un système numérique a été étudiée en détails, mais cela reste toujours un défi d'en réaliser une modélisation précise. De plus, des travaux récents ont montrés que la prise en compte des fautes au niveau de la micro-architecture peut engendrer des phénomènes subtils, ouvrant des perspectives de recherche intéressantes quant à la modélisation et l'analyse de ces effets ainsi qu'à leur réduction. L'objectif de cette thèse est d'étudier l'apport d'une approche de modélisation formelle du matériel pour tout d'abord mieux comprendre les conséquences d'injections de fautes puis de vérifier l'efficacité des contre-mesures utilisées dans les systèmes embarqués sécurisés.

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

Amélioration du désassemblage par canaux auxilaires

Département Systèmes (LETI)

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

Bac +5 Informatique ou Mathématique

01-09-2021

SL-DRT-21-0375

thomas.hiscock@cea.fr

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

Le désassemblage par canaux auxiliaires (ou Side Channel Based Disassembling, SCBD) consiste à retrouver le code exécuté par un microprocesseur à partir de phénomènes physiques produits par le circuit lors de son fonctionnement. La consommation de courant ou encore le rayonnement électro-magnétique sont particulièrement faciles à mesurer et très exploitables par ce type d'attaques. Avoir une fine caractérisation de ce type d'attaques est essentiel pour sécuriser les systèmes, notamment contre de la rétro-conception. Le laboratoire LSOSP est très actif sur le sujet et a notamment proposé une technique de reconstruction mono-bit très efficace sur des petit microcontrôleurs. L'objectif de cette thèse est de contribuer à l'amélioration des techniques de désassemblage par canaux auxiliaires. Nous chercherons notamment à prouver si ce type d'attaques peuvent être applicables à des processeurs plus complexes, comme ceux que l'on peut trouver sur un téléphone. Au cours de la thèse, nous chercherons donc à étudier finement les fuites de c?urs complexes et adapter des outils du machine learning pour extraire des informations à partir de mesures extrêmement bruitées. Au bout des trois ans, nous espérons avoir une meilleur vue de la faisabilité du désassemblage sur des c?urs complexes et également des réflexions sur des contremesures qu'il serait possible d'utiliser.

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

Techniques de fuzzing pour le support aux analyses statiques de sécurité

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

Laboratoire pour la Sûreté du Logiciel

Master/Ingénieur en Informatique

01-10-2021

SL-DRT-21-0557

michael.marcozzi@cea.fr

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

Garantir la sécurité numérique est un enjeu crucial. Dans ce contexte, les analyses statiques et le fuzzing sont des approches populaires permettant de détecter les vulnérabilités logicielles directement au niveau binaire. Ces deux approches sont complémentaires: les analyses statiques peuvent soit fournir des garanties que le programme est sûr, soit signaler des exécutions de programme potentiellement dangereuses. Au contraire, le fuzzing ne peut fournir aucune garantie stricte sur la sécurité du programme, mais est capable d'identifier à coup sûr des exécutions qui présentent une vulnérabilité. Dans cette thèse, nous utiliserons donc le fuzzing pour confirmer les rapports de vulnérabilité issus de l'analyse statique. Cela nous demandera de développer un fuzzer capable de cibler les exécutions potentiellement non sécurisées identifiées par l'analyseur statique. Ceci est assez complexe car le fuzzing ciblé est un domaine difficile et peu recherché. De plus, les analyseurs statiques fournissent des descriptions assez vagues des exécutions potentiellement vulnérables, ce qui rend la tâche du fuzzer encore plus compliquée. Pour surmonter ces défis, nous profiterons de solutions éprouvées dans les domaines du test basé sur la recherche et des critères de couverture avancés, et qui sont sous-exploitées dans le domaine du fuzzing. Le fuzzer développé sera évalué à grande échelle dans des cas d'utilisation réels et nous déterminerons dans quelle mesure il permet une meilleure prioritisation et une élaboration plus précise des rapports de vulnérabilité. Enfin, nous fournirons des éléments de généralisation, afin de rendre le fuzzing ciblé plus facilement adaptable à d'autres problèmes partageant des similitudes avec la confirmation de rapports de vulnérabilité.

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

Sécurité du code et spéculations

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

Laboratoire pour la Sûreté du Logiciel

M2 en informatique. Spécialisation en méthodes formelles, sécurité ou compilation

SL-DRT-21-0559

sebastien.bardin@cea.fr

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

Nous considérons le cadre général de l'analyse automatique de programmes pour la sécurité. Tandis que les attaques standards profitent de bugs de programmation (ex : débordement mémoire et injection de code), les récentes attaques micro-architecturales profitent elles de comportements subtiles des microprocesseurs, typiquement les comportements spéculatifs, afin de récupérer des données sensibles. Ces vulnérabilités sont très difficiles à trouver pour un expert humain, car elles demandent de raisonner à un très bas niveau de code, sur des comportements non naturels. Le but de ce sujet de thèse est de comprendre comment les techniques avancées d'analyse de code pour la sécurité (notamment, l'exécution symbolique) peuvent être adaptées au cas des attaques micro-architecturales par spéculation, avec en ligne de mire la vérification et la sécurisation de primitives de sécurité essentielles dans les librairies cryptographiques et dans les systèmes d'exploitation. Les défis principaux sont la compréhension de la sémantique par spéculation, la compréhension des propriétés de sécurité impliquées, et finalement la conception de techniques de vérification capables de passer à l'échelle pour les attaques spéculatives. Ces résultats seront implémentés dans l'outil open-source BINSEC d'analyse de code binaire.

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

Voir toutes nos offres