Direction scientifique
Transfert de connaissances vers l'industrie

Nos Thèses par thème

Défis technologiques >> Cybersécurité : hardware et software
11 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)

Exploitation des vulnérabilités matérielles des dispositifs mobiles comme nouvelle approche pour l'analyse Forensic

Département Systèmes (LETI)

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

master ou école d'ingénieur Mathématique, Informatique ou Électronique

01-09-2021

SL-DRT-21-0742

driss.aboulkassimi@cea.fr

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

L'objectif de la thèse est d'étudier le potentiel des vulnérabilités matérielles des dispositifs mobiles pour contourner des fonctions de sécurité d'un téléphone mobile de type smartphone, ou extraire des secrets. Les chemins de vulnérabilités à explorer tireront profit d'un accès physique au System-On-Chip réalisant des fonctions de sécurité. Par exemple, l'analyse des émanations électromagnétiques ou la perturbation par illumination laser ou électromagnétique sont des moyens efficaces pour extraire des secrets ou contourner des mécanismes de sécurités. Des travaux de l'équipe SAS ont permis de montrer que les vulnérabilités physiques peuvent être une menace pour les mécanismes de sécurité des Systems-On-Chip. L'analyse d'émissions permet potentiellement d'extraire un secret d'une enclave comme la TrustZone [1]. L'injection de fautes par perturbation électromagnétique peut permettre de réaliser une élévation de privilèges en s'authentifiant avec un mot de passe illégitime [2]. À travers cette thèse nous étudierons trois verrous qui limitent aujourd'hui le potentiel des vulnérabilités physiques sur Smartphone : la microarchitecture complexe des SoCs, la pile logicielle complexe des smartphones, et la synchronisation temporelle et spatiale des perturbations pour contourner un mécanisme de sécurité. En effet, la mise en place de ces bancs de test nécessite une bonne synchronisation entre le banc d'attaque et le code logiciel en cours d'exécution. Cette synchronisation est un verrou majeur, voire le premier à résoudre pour ouvrir de nouvelles pistes permettant l'exploitation des vulnérabilités matérielles sur smartphone. Dans un premier temps, le doctorant ou la doctorante explorera donc de nouvelles méthodes pour affronter la problématique de synchronisation du banc de test par perturbation pour l'exploitation d'injection de fautes sur Systems-On-Chip. Dans un second temps, les travaux de thèse viseront à développer de nouvelles méthodes pour contourner les verrous qui empêchent aujourd'hui l'exploitation des techniques de caractérisation sécuritaire par perturbation et par analyse de canaux auxiliaires sur téléphones mobiles pour l'extraction de données. Ce sujet de thèse s'inscrit dans le contexte du projet H2020 EXFILES. Ce projet réunit des académiques, des industrielles et des forces de l'ordre de 7 pays européens. Les travaux effectués dans le cadre de cette thèse permettront de compléter les outils d'analyse Forensic existants. Par ailleurs, l'un des problèmes majeurs de l'exploitation des techniques de perturbation par injection de fautes pour une fin FORENSIC, réside dans le taux de reproductibilité des résultats. Par exemple, en fonction des conditions expérimentales du test, un banc d'injection EM ne permet pas souvent de fournir les mêmes résultats sur la même cible : dans le cas d'une variation de la température de la salle de test de quelques degrés, ou si le sonde d'injection EM a été déplacée ensuite remise à sa position initiale, etc. Le doctorant devra donc explorer et proposer des pistes d'automatisation, assurant un important taux de reproductibilité indépendamment des conditions de test et de la cible. Le laboratoire LSOSP (Laboratoire de Sécurité des Objets et Systèmes Physiques) accueillera le/la doctorant sur son site de Gardanne au sein de l'équipe de recherche commune entre le CEA et l'EMSE: SAS "Systèmes et Architectures Sécurisés". Cette équipe dispose d'équipements de pointe avec des bancs de caractérisation sécuritaire matérielle au niveau de l'état de l'art international. Elle est située entre Aix-En-Povence et Marseille à Gardanne sur le campus Georges Charpak Provence. La thèse sera dirigée par Jessy Clédière et co-encadrée par Driss Aboulkassimi et Simon Pontié. Le candidat/La candidate pourra avoir suivi un cursus Mathématique, Informatique ou Électronique. Une expérience en lien avec l'analyse de vulnérabilités matérielles n'étant pas obligatoire, mais appréciable. La thèse démarrera en octobre 2021. Les candidatures accompagnées d'un CV, des derniers relevés de notes et d'une lettre de motivation sont à envoyer par mail avant le 15 avril 2021 à simon.pontie@cea.fr Plus d'informations: - https://www.simon.pontie.fr/sujet-these/exfiles/index.html - https://exfiles.eu/, présentation vidéo https://vimeo.com/441318313 - https://www.simon.pontie.fr/ - https://www.leti-cea.fr/ [1] P. Leignac, O. Potin, J.-M. Dutertre, J.-B. Rigaud, et S. Pontie, « Comparison of side-channel leakage on Rich and Trusted Execution Environments », in 6th Workshop on Cryptography and Security in Computing Systems, 2019. https://doi.org/10.1145/3304080.3304084. [2] C. Gaine, D. Aboulkassimi, S. Pontie, J.-P. Nikolovski, et J.-M. Dutertre, « Electromagnetic Fault Injection as a New Forensic Approach for SoCs », in 2020 IEEE International Workshop on Information Forensics and Security (WIFS), 2020. https://www.wifs2020.nyu.edu/.

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

Spécification et vérification multi-niveau de propriétés de cybersécurité pour les programmes C critiques

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

Laboratoire pour la Sûreté du Logiciel

master analyse de programmes/ingénierie logicielle

01-09-2021

SL-DRT-21-0866

virgile.prevosto@cea.fr

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

Ce sujet s'inscrit dans la problématique de spécification et vérification de logiciels en visant en particulier les propriétés de cybersécurité. Les outils de vérification déductive permettent d'effectuer une preuve rigoureuse qu'un programme respecte les propriétés spécifiées. Le greffon WP de Frama-C vise la preuve des propriétes spécifiées en ACSL. Un autre greffon, MetAcsl, a été récemment développé pour faciliter l'expression et la vérification des propriétés de haut niveau, telles que les propriétés de cybersécurité (e.g. isolation, integrité, confidentialité). MetAcsl permet entre autres d'imposer des contraintes sur toutes les opérations d'écriture et de lecture. Cependant, la vérification des propriétés de haut niveau sur les logiciels industriels complexes est souvent confrontée à l'incapacité des outils automatiques à déduire les propriétés nécessaires. Cela est souvent dû à deux raisons. D'une part, les logiciels utilisent des opérations de bas niveau (e.g. opérations bit-à-bit, casts de pointeurs) qui rendent la preuve beaucoup moins efficace. D'autre part, la quantité et la complexité des propriétés indépendantes, notamment des invariants à maintenir sur les structures de données complexes, peuvent empêcher le prouveur de produire une preuve automatiquement. Ainsi, le prouveur se trouve incapable de déduire des propriétés logiquement correctes à cause d'un niveau de complexité élevé des propriétés. Cependant, on observe souvent qu'un sous-ensemble très limité de propriétés est réellement impacté par chaque fonction du code, alors que les autres propriétés sont juste maintenues et complexifient le contexte de preuve. Pour certaines propriétés impactées, leur préservation pourrait être établie plus facilement à un niveau plus abstrait. Par ailleurs, les propriétés spécifiées à un niveau plus abstrait ont l'avantage d'être plus faciles à comprendre et diminuent le risque d'erreur de spécification pour l'ingénieur vérification. De même, un modèle abstrait exécutable peut être animé et évalué plus facilement par rapport au codé réel. Cette thèse vise à développer une démarche de spécification et de vérification multi-niveau pour les programmes C. Dans cette démarche, une partie des propriétés logiques seront vérifiées sur une version abstraite du logiciel à prouver. La version abstraite sera représentée par un code C plus simple à analyser (faisant abstraction de certaines fonctions, de certaines variables, ou en simplifiant leur représentation par rapport au code réel), encodant par exemple un système de transitions, tout en restant représentatif par rapport aux propriétés à prouver. S'inspirant des techniques de raffinement connues (par exemple pour les machines B), le lien entre le système abstrait et le code réel sera rigoureusement établi afin d'assurer la correction de la démarche. Ainsi, la preuve du code réel sera facilité: il suffira de vérifier que le code réel respecte les propriétés de raffinement pour déduire certaines propriétés complexes sans devoir les prouver sur le code réel. La spécification et la vérification des propriétés de raffinement pourra notamment s'appuyer sur MetAcsl. Par exemple, le maintien des propriétés non impactées pourrait être déduit plus facilement quand le code ne modifie pas leur empreinte mémoire, c'est-à-dire, les variables impliquées dans l'expression de la propriété. Une première étape de la thèse consistera à concevoir une démarche de spécification d'un système abstrait adapté pour un logiciel réel. Il s'agira de définir un lien entre les données et les fonctions des deux systèmes et leurs propriétés. Il faudra également définir les propriétés de raffinement qui permettront d'assurer les propriétés sur le système réel. La technique proposée devra être adaptée à la fois aux logiciels industriels complexes (avec des structures de données optimisées, de bas niveau, avec plusieurs invariants à préserver) et aux propriétés de cybersécurité. Pour garantir son applicabilité sur les logiciels industriels existants, elle pourra s'appliquer de bas en haut, en partant d'une implémentation réelle existante en visant les propriétés et les fonctions dont le preuve nécessite réellement cette démarche. Elle devra notamment permettre l'utilisation de plusieurs abstractions possibles pour prouver différentes propriétés (typiquement, impactées par des ensembles de fonctions différentes). Par exemple, on peut vouloir vérifier le mécanisme de création des objets (ou de tâches dans un micronoyau) avec un modèle abstrait différent par rapport au mécanisme d'exécution des tâches ou de contrôle des droits d'accès. Enfin, elle pourra s'appuyer sur MetAcsl pour assurer les propriétés de raffinement sur le code réel. Une deuxième étape consistera à automatiser cette démarche en développant un outil dédié. Enfin, ces nouveaux mécanismes seront évalués sur des études de cas open-sources ou issues de projets industriels.

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

Détection d'intrusion distribuée dans un contexte de réseau périphérique contraint

Département Intelligence Ambiante et Systèmes Interactifs (LIST)

Laboratoire Systèmes Communiquants

Informatique, IA, Telecom

01-09-2021

SL-DRT-21-0965

alexis.olivereau@cea.fr

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

L'objectif du travail de thèse proposé consiste à définir un système de sécurité réactif autonome distribué capable de se reconfigurer en temps réel afin de prendre en particulier en compte les attaques éventuelles, le modèle de trafic à surveiller et ses propres ressources. Dans ce système, les sondes de détection d'intrusion sont des composants essentiels. Elles mettent en oeuvre une détection par anomalie fonctionnant par intelligence artificielle, capable de détecter des signaux faibles en environnement potentiellement à très haut débit. Les analyses des différentes sondes sont corrélées de manière à accroitre la capacité globale d'identifier des comportements malveillants à l'échelle d'un réseau à protéger. Enfin, la problématique de l'efficacité énergétique est à considérer tant au niveau des sondes individuelles que de l'orchestration de la fonction globale de surveillance. Sujet de thèse proposé dans le cadre du projet européen GREENEDGE: https://greenedge-itn.eu/wp-content/uploads/2021/03/ESR11_description.pdf Toute candidature doit être soumise via le site du projet GREENEDGE: https://greenedge-itn.eu/phd-hiring-call/

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

Voir toutes nos offres