Tri :
Date
Titre
Auteur
|
|
Informatique
/ 05-09-2017
Aljarbouh Ayman
Voir le résumé
Voir le résumé
Cette thèse apporte quatre principales contributions : une méthode d'éliminateur de phénomènes de ''chattering'' d'automates hybrides, par calcul d'une dynamique régulière équivalente à l'aide d'une convexification de Filippov ; une méthode d'accélération de la simulation de certains comportements Zénon, dits géométriques, pour certains automates hybrides ; des preuves de préservation par les méthodes ci-dessus d'une sémantique des automates hybrides à base d'analyse non-standard ; développement de trois logiciels prototypes, l'un sous la forme d'une bibliothèque Simulink, le second sous la forme d'un environnement de simulation de composants FMI, et le troisième étant une implémentation de la méthode de régularisation dans le langage de modélisation de systèmes hybrides Acumen.
|
|
Informatique
/ 24-03-2023
Allenet Thibault
Voir le résumé
Voir le résumé
Les réseaux de neurones convolutifs et les réseaux neurones récurrents (RNN) ont été largement utilisés dans de nombreux domaines tels que la vision par ordinateur, le traitement naturel du langage et le traitement du signal. Néanmoins, la charge de calcul et le besoin en bande passante mémoire impliqués dans l'inférence des réseaux de neurones profonds empêchent souvent leur déploiement sur des cibles embarquées à faible ressources. De plus, la vulnérabilité des réseaux de neurones profonds à de petites perturbations sur les entrées remet en question leur déploiement pour des applications impliquant des décisions de haute criticité. Pour relever ces défis, cette thèse propose deux principales contributions. D'une part, nous proposons des méthodes de compression pour rendre les réseaux de neurones profonds plus adaptés aux systèmes embarqués ayant de faibles ressources. D'autre part, nous proposons une nouvelle stratégie pour rendre les réseaux de neurones profonds plus robustes aux attaques adverses en tenant compte des ressources limitées des systèmes embarqués. Dans un premier temps, nous présentons une revue de la littérature sur des principes et des outils de bases de l'apprentissage profond, des types de réseaux de neurones reconnus et un état de l'art sur des méthodes de compression de réseaux de neurones. Ensuite, nous présentons deux contributions autour de la compression des réseaux de neurones profonds : une étude de transférabilité du Lottery Ticket sur les RNN et une méthode de quantification à l’apprentissage. L’étude de transférabilité du Lottery Ticket sur les RNN analyse la convergence des RNN et étudie son impact sur l'élagage des paramètres pour des taches de classification d'images et de modélisation du langage. Nous proposons aussi une méthode de prétraitement basée sur le sous-échantillonnage des données qui permet une convergence plus rapide des LSTM tout en préservant les performances applicatives. Avec la méthode Disentangled Loss Quantization Aware Training (DL-QAT), nous proposons d'améliorer une méthode de quantification avancée avec des fonctions de coût favorables à la quantification afin d'atteindre des paramètres binaires. Les expériences sur ImageNet-1k avec DL-QAT montrent une amélioration de près de 1 % sur la précision du score de ResNet-18 avec des poids binaires et des activations de 2 bits. Il apparaît clairement que DL-QAT fournit le meilleur profil du compromis entre l'empreinte mémoire et la performance applicative. Ce travail étudie ensuite la robustesse des réseaux de neurones face aux attaques adverses. Après avoir présenté l'état de l'art sur les attaques adverses et les mécanismes de défense, nous proposons le mécanisme de défense Ensemble Hash Defense (EHD). EHD permet une meilleure résistance aux attaques adverses basées sur l'approximation du gradient tout en préservant les performances de l'application et en ne nécessitant qu'une surcharge de mémoire au moment de l'inférence. Dans la meilleure configuration, notre système réalise des gains de robustesse significatifs par rapport aux modèles de base et à une approche de robustesse basée sur la fonction de coût. De plus, le principe de l'EHD la rend complémentaire à d'autres méthodes d'optimisation robuste qui permettraient d'améliorer encore la robustesse du système final. Dans la perspective de l'inférence sur cible embarquée, la surcharge mémoire introduite par l'EHD peut être réduite par la quantification ou le partage de poids. En conclusion, les travaux de cette thèse ont proposé des méthodes de compression de réseaux de neurones et un système de défense pour résoudre des défis importants, à savoir comment rendre les réseaux de neurones profonds plus robustes face aux attaques adverses et plus faciles à déployer sur les plateformes à ressources limitées. Ces travaux réduisent davantage l'écart entre l'état de l'art des réseaux neurones profonds et leur exécution sur des cibles embarquées à faible ressources.
|
|
Informatique
/ 14-12-2022
Almeida Braga Daniel de
Voir le résumé
Voir le résumé
Les attaques par canaux auxiliaire sont redoutables face aux implémentations cryptographiques. Malgré les attaques passées, et la prolifération d'outils de vérification, ces attaques affectent encore de nombreuses implémentations. Dans ce manuscrit, nous abordons deux aspects de cette problématique, centrés autour de l'attaque et de la défense. Nous avons dévoilé plusieurs attaques par canaux auxiliaires microarchitecturaux sur des implémentations de protocoles PAKE. En particulier, nous avons exposé des attaques sur Dragonfly, utilisé dans la nouvelle norme Wi-Fi WPA3, et SRP, déployé dans de nombreux logiciel tels que ProtonMail ou Apple HomeKit. Nous avons également exploré le manque d'utilisation par les développeurs d'outil permettant de détecter de telles attaques. Nous avons questionné des personnes impliqués dans différents projets cryptographiques afin d'identifier l'origine de ce manque. De leur réponses, nous avons émis des recommandations. Enfin, dans l'optique de mettre fin à la spirale d'attaques-correction sur les implémentations de Dragonfly, nous avons fournis une implémentation formellement vérifiée de la couche cryptographique du protocole, dont l'exécution est indépendante des secrets.
|
|
Informatique
/ 12-12-2023
Amalou Abderaouf Nassim
Voir le résumé
Voir le résumé
L'estimation du temps d'exécution des programmes est une tâche clé mais difficile, rendue encore plus complexe par la croissance de la complexité et l'insuffisance de la documentation des architectures de processeurs modernes. Bien que les méthodes traditionnelles comme les simulateurs précis au cycle soient exactes, elles sont également longues et nécessitent une compréhension approfondie de l'architecture du processeur. Pour aborder ces limitations, une nouvelle approche basée sur les données et utilisant des techniques d'apprentissage automatique a été développée. Cependant, bien que les modèles d'apprentissage automatique existants offrent des estimations rapides, ils sont principalement adaptés à des architectures simples avec des temps d'instruction constants. Ce document vise à développer de nouvelles méthodes d'apprentissage automatique pour des processeurs complexes et non documentés en introduisant la prise en compte du contexte dans les modèles de timing basés sur l'apprentissage automatique. Une approche novatrice traitant les séquences d'instructions comme un langage naturel et emploie des algorithmes d'apprentissage automatique avancés tels que les réseaux Long Short-Term Memory et les Transformers. Ceci permet au modèle de prendre en compte des caractéristiques complexes telles que les effets de cache et de pipeline, améliorant la précision pour les temps d'exécution moyens et pires cas.
|
|
Informatique
/ 19-10-2022
Ambal Guillaume
Voir le résumé
Voir le résumé
Les sémantiques squelettiques sont un cadre logique pour décrire les sémantiques opérationnelles. Tout d'abord, nous présentons une transformation automatique d'une sémantique squelettique écrite en style grand-pas vers une sémantique équivalente en style petit-pas. Cette transformation est implémentée dans l'outil Necro, ce qui nous permet de générer automatiquement un interpréteur OCaml pour la sémantique petit-pas ainsi qu'une formalisation Coq des deux sémantiques. Nous certifions la transformation de deux manières : nous donnons une preuve papier du cœur de la transformation, et nous générons des scripts de preuve Coq spécialisés durant la transformation. Nous proposons également une méthode automatique pour générer un interpréteur OCaml certifié pour n'importe quel langage défini en sémantiques squelettiques. Pour cela, nous présentons deux nouvelles interprétations des sémantiques squelettiques, sous la forme de machines abstraites déterministe et non-déterministe. Ces machines sont obtenues à partir de l'interprétation grand-pas principale en utilisant la correspondance fonctionnelle, une méthode connue pour transformer un évaluateur en machine abstraite. Ces nouvelles interprétations sont formalisées en Coq, et nous vérifions leur correction. Enfin, nous utilisons le système d'extraction de Coq vers OCaml pour obtenir un interpréteur certifié.
|
|
Informatique
/ 07-12-2017
Amdouni Emna
Voir le résumé
Voir le résumé
En médecine personnalisée, les mesures et les descriptions radiologiques jouent un rôle important. En particulier, elles facilitent aux cliniciens l’établissement du diagnostic, la prise de décision thérapeutique ainsi que le suivi de la réponse au traitement. On peut citer à titre d’exemple, les critères d’évaluation RECIST (en anglais Response Evaluation Criteria in Solid Tumors). De nombreuses études de corrélation en radiologie-pathologie montrent que les caractéristiques d'imagerie quantitative et qualitative sont associées aux altérations génétiques et à l'expression des gènes. Par conséquent, une gestion appropriée des phénotypes d'imagerie est nécessaire pour faciliter leur utilisation et leur réutilisation dans de multiples études concernant les mesures radiologiques. En littérature, les mesures radiologiques qui caractérisent les processus biologiques des sujets imagés sont appelées biomarqueurs d'imagerie. L'objectif principal de cette thèse est de proposer une conceptualisation ontologique des biomarqueurs d'imagerie pour rendre leur sens explicite et formel, améliorer le reporting structuré des images. La première partie de la thèse présente une ontologie générique qui définit les aspects fondamentaux du concept de biomarqueur d'imagerie, à savoir : les caractéristiques biologiques mesurées, les protocoles de mesure et les rôles des biomarqueurs imagerie dans la prise de décision. La deuxième partie de la thèse traite des problèmes de modélisation sémantique liés à la description des données d’observation en neuro-imagerie en utilisant les connaissances biomédicales existantes. Ainsi, elle propose des solutions ''pertinentes'' aux situations les plus typiques qui doivent être modélisées dans le glioblastome.
|
|
Informatique
/ 08-07-2021
Amirian Javad
Voir le résumé
Voir le résumé
Nos vies sont de plus en plus influencées par les robots. Ils ne se limitent plus à travailler dans les usines et apparaissent de plus en plus dans des espaces partagés avec les humains, pour livrer des biens et des colis, transporter des médicaments ou tenir compagnie à des personnes âgées. Par conséquent, ils doivent percevoir, analyser et prévoir le comportement des personnes qui les entourent et prendre des mesures sans collision et socialement acceptables des actions sans collision et socialement acceptables. Dans cette thèse, nous abordons le problème de la prédiction de la trajectoire humaine (à court terme), afin de permettre aux robots mobiles, tels que Pepper, de naviguer dans des environnements bondés. Nous proposons une nouvelle approche socialement consciente pour la prédiction de plusieurs piétons. Notre modèle est conçu et entraîné sur la base de réseaux adversariaux génératifs, qui apprennent la distribution multimodale des prédictions plausibles pour chaque piéton. De plus, nous utilisons une version modifiée de ce modèle pour effectuer une simulation de foule basée sur des données. La prédiction de l’emplacement des piétons occultés est un autre problème abordé dans cette thèse. Nous avons également réalisé une étude sur des jeux de données courants de trajectoires humaines. Une liste de métriques quantitatives est proposée pour évaluer la complexité de la prédiction dans ces jeux de données.
|
|
Informatique
/ 09-12-2019
Anapparakkal Arif Ali
Voir le résumé
Voir le résumé
Les évolutions de l'architecture des processeurs visent à améliorer les performances des applications, mais les éditeurs de logiciels sont souvent limités au plus petit dénominateur commun afin de maintenir la compatibilité avec la diversité du matériel de leurs clients. Avec des informations plus détaillées, un compilateur peut générer un code plus efficace. Même si le modèle de processeur est connu, les fabricants ne divulguent pas de nombreux détails pour des raisons de confidentialité. En outre, l'efficacité de nombreuses techniques d'optimisation peut varier en fonction des entrées du programme. Cette thèse introduit deux outils, FITTCHOOSER et OFSPER, qui effectuent des optimisations au niveau des fonctions les mieux adaptées à l'environne-ment d'exécution et aux données en cours. FITTCHOOSER explore de manière dynamique les spécialisations des fonctions les plus gourmandes en ressources d'un programme pour choisir la version la plus adaptée – non seulement à l'environnement d'exécution en cours,mais également à l'exécution en cours du programme. OFSPER applique une spécialisation de fonction dynamique, c'est-à-dire la spécialisation de fonctions dans une application sur un processus en cours d'exécution. Cette technique capture les valeurs réelles des arguments lors de l'exécution du programme et, si rentables, crée des versions spécialisées et les inclut au moment de l'exécution.
|
|
Informatique
/ 29-05-2017
Andreescu Oana Fabiana
Voir le résumé
Voir le résumé
Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites constituent les propriétés de frame (frame properties en anglais). Elles sont habituellement spécifiées manuellement par le programmeur et leur validité doit être vérifiée: il est nécessaire de prouver que les opérations du programme n'outrepassent pas les limites ainsi déclarées. Dans le contexte de la vérification formelle interactive de systèmes complexes, comme les systèmes d'exploitation, un effort considérable est investi dans la spécification et la preuve des propriétés de frame. Cependant, la plupart des opérations ont un effet très localisé et ne menacent donc qu'un nombre limité d'invariants. Étant donné que la spécification et la preuve de propriétés de frame est une tache fastidieuse, il est judicieux d'automatiser l'identification des invariants qui ne sont pas affectés par une opération donnée. Nous présentons dans cette thèse une solution inférant automatiquement leur préservation. Notre solution a pour but de réduire le nombre de preuves à la charge du programmeur. Elle est basée sur l'analyse statique, et ne nécessite aucune annotation de frame. Notre stratégie consiste à combiner une analyse de dépendances avec une analyse de corrélations. Nous avons conçu et implémenté ces deux analyses statiques pour un langage fonctionnel fortement typé qui manipule structures, variants et tableaux. Typiquement, une propriété fonctionnelle ne dépend que de quelques fragments de l'état du programme. L'analyse de dépendances détermine quelles parties de cet état influent sur le résultat de la propriété fonctionnelle. De même, une fonction ne modifiera que certaines parties de ses arguments, copiant le reste à l'identique. L'analyse de corrélations détecte quelles parties de l'entrée d'une fonction se retrouvent copiées directement (i.e. non modifiés) dans son résultat. Ces deux analyses calculent une approximation conservatrice. Grâce aux résultats de ces deux analyses statiques, un prouveur de théorèmes interactif peut inférer automatiquement la préservation des invariants qui portent sur la partie non affectée par l’opération concernée. Nous avons appliqué ces deux analyses statiques à la spécification fonctionnelle d'un micro-noyau, et obtenu des résultats non seulement d'une précision adéquate, mais qui montrent par ailleurs que notre approche peut passer à l'échelle.
|
|
Informatique
/ 17-12-2020
Andriamilanto Tompoariniaina Nampoina
Voir le résumé
Voir le résumé
L'authentification web consiste à vérifier que le visiteur d'un site web est bien le détenteur d'un compte. Pour ce faire, plusieurs informations peuvent servir de preuve de détention, dont les empreintes de navigateur. Celles-ci sont des propriétés collectées à partir d'un navigateur permettant d'en constituer une empreinte potentiellement unique. Au travers de cette thèse, nous proposons deux contributions. Nous étudions l'adéquation des empreintes de navigateur pour de l'authentification. Nous faisons le lien entre les empreintes digitales et celles des navigateurs afin d'évaluer ces dernières selon des propriétés d'informations biométriques. Nous basons notre étude sur l'analyse de quatre jeux de données d'empreintes de navigateur, dont un comprenant presque deux millions de navigateurs. Nous proposons FPSelect, un outil de sélection d'attributs tels qu'ils satisfassent un niveau de sécurité et réduisent les contraintes d'utilisation. Le niveau de sécurité est mesuré selon la proportion d'utilisateurs usurpés étant donné les attributs utilisés, une population de navigateurs, et un attaquant modélisé. Les contraintes sur l'utilisation sont mesurées selon le temps de collecte des empreintes, leur taille, et leur instabilité. Nous comparons les résultats de FPSelect avec des méthodes usuelles de sélection d'attributs sur deux jeux de données.
|
|