Tri :
Date
Titre
Auteur
|
|
Informatique
/ 15-12-2023
Patat Gwendal
Voir le résumé
Voir le résumé
Les systèmes opaques présentent un défi unique pour la gestion des droits numériques, ou Digital Right Management (DRM), Widevine en étant une illustration clé. Malgré son utilisation répandue, ce système DRM a révélé des vulnérabilités importantes dans la protection du contenu propriétaire. Dans cette thèse, nous disséquons le fonctionnement interne de Widevine et analysons comment cette opacité entrave la sécurité tant pour les fournisseurs de contenu, appelés platforme Over-the-Top (OTT), que pour les utilisateurs. Nous explorons sa mise en utilisation sur les plateformes OTT, identifiant les obstacles qui empêchent son utilisation complète. Les préoccupations en matière de confidentialité sont également abordées, alors que nous enquêtons sur des problèmes d'implémentation au sein des navigateurs internet lors de la standardisation des systèmes DRM par la W3C avec la recommandation Encrypted Media Extension (EME). Ces résultats ne dévoilent pas seulement des problèmes liés à Widevine, mais signalent également des voies de recherche futures dans le paysage DRM plus large, soulignant la nécessité de transparence, de sécurité et de conception centrée autour des utilisateurs.
|
|
Informatique
/ 22-02-2018
Nguyen Viet Anh
Voir le résumé
Voir le résumé
Les temps avancent et les applications temps-réel deviennent de plus en plus gourmandes en ressources. Les plate-formes multi-cœurs sont apparues dans le but de satisfaire les demandes des applications en ressources, tout en réduisant la taille, le poids, et la consommation énergétique. Le challenge le plus pertinent, lors du déploiement d'un système temps-réel sur une plate-forme multi-cœur, est de garantir les contraintes temporelles des applications temps réel strict s'exécutant sur de telles plate-formes. La difficulté de ce challenge provient d'une interdépendance entre les analyses de prédictabilité temporelle. Cette interdépendance peut être figurativement liée au problème philosophique de l'œuf et de la poule, et expliqué comme suit. L'un des pré-requis des algorithmes d'ordonnancement est le Pire Temps d'Exécution (PTE) des tâches pour déterminer leur placement et leur ordre d'exécution. Mais ce PTE est lui aussi influencé par les décisions de l'ordonnanceur qui va déterminer quelles sont les tâches co-localisées ou concurrentes propageant des effets sur les caches locaux et les ressources physiquement partagées et donc le PTE. La plupart des méthodes d'analyse pour les architectures multi-cœurs supputent un seul PTE par tâche, lequel est valide pour toutes conditions d'exécutions confondues. Cette hypothèse est beaucoup trop pessimiste pour entrevoir un gain de performance sur des architectures dotées de caches locaux. Pour de telles architectures, le PTE d'une tâche est dépendant du contenu du cache au début de l'exécution de la dite tâche, qui est lui-même dépendant de la tâche exécutée avant et ainsi de suite. Dans cette thèse, nous proposons de prendre en compte des PTEs incluant les effets des caches privés sur le contexte d’exécution de chaque tâche. Nous proposons dans cette thèse deux techniques d'ordonnancement ciblant des architectures multi-cœurs équipées de caches locaux. Ces deux techniques ordonnancent une application parallèle modélisée par un graphe de tâches, et génèrent un planning statique partitionné et non-préemptif. Nous proposons une méthode optimale à base de Programmation Linéaire en Nombre Entier (PLNE), ainsi qu'une méthode de résolution par heuristique basée sur de l'ordonnancement par liste. Les résultats expérimentaux montrent que la prise en compte des effets des caches privés sur les PTE des tâches réduit significativement la longueur des ordonnancements générés, ce comparé à leur homologue ignorant les caches locaux. Afin de parfaire les résultats ainsi obtenus, nous avons réalisé l'implémentation de nos ordonnancements dirigés par le temps et conscients du cache pour un déploiement sur une machine Kalray MPPA-256, une plate-forme multi-cœur en grappes (clusters). En premier lieu, nous avons identifié les challenges réels survenant lors de ce type d'implémentation, tel que la pollution des caches, la contention induite par le partage du bus, les délais de lancement d'une tâche introduits par la présence de l'ordonnanceur, et l'absence de cohérence des caches de données. En second lieu, nous proposons des stratégies adaptées et incluant, dans la formulation PLNE, les contraintes matérielles ; ainsi qu'une méthode permettant de générer le code final de l'application. Enfin, l'évaluation expérimentale valide la correction fonctionnelle et temporelle de notre implémentation pendant laquelle nous avons pu observé le facteur le plus impactant la longueur de l'ordonnancement: la contention.
|
|
Informatique
/ 25-03-2016
Arouk Osama
Voir le résumé
Voir le résumé
Les réseaux actuels et la prochaine génération des réseaux sans fil cellulaires (5G) doivent garantir, non seulement, les communications entre les gens (aussi connu sous le nom d'humain à humain - H2H), mais aussi à un déploiement massif de communication de type machine (MTC). MTC, ou encore Machine à Machine (M2M), peut être considérée comme des appareils qui peuvent établir des communications avec d’autres appareils sans aucune intervention humaine. M2M est aussi vue comme la pierre angulaire de la vision des objets connectés (IoT). Elle attire beaucoup d'attention, car elle peut être considérée comme une nouvelle opportunité pour les opérateurs de réseau et service IoT. Il existe aujourd’hui plusieurs types d’applications se basant sur MTC couvrant plusieurs domaines. On peut citer comme exemples les applications suivantes: la santé, les systèmes de transport intelligents (ITS), les compteurs intelligents et les réseaux intelligents, et la sécurité publique (PS). Le déploiement de ce type d'applications dans les réseaux mobiles cellulaires actuels, particulièrement Long Term Evolution (LTE) et LTE-Advanced (LTE-A) , ne peut être effectif sans surmonter les challenges posés par le déploiement d’un grand nombre d’équipement MTC dans la même cellule. En effet, le déploiement d'une myriade d'appareils MTC causera une congestion et une surcharge du système des réseaux d'accès radio (RAN) et du cœur de réseau (CN). Comme les appareils MTC sont équipés d'une batterie non rechargeable, la consommation d'énergie est aussi un défi. Dans cette thèse, nous allons étudier les problèmes de congestion et de consommation d'énergie dans le contexte des réseaux LTE et LTE-A en présence des appareils M2M. En ce qui concerne la congestion et la surcharge de système, nous nous concentrons sur la partie RAN, puisqu'elle peut être considérée comme la première ligne de défense pour le réseau cellulaire. Les contributions de cette thèse sont organisées sous les axes suivants: 1) Proposition d'un algorithme générique pour prédire le trafic entrant, de sorte que la congestion dans le réseau peut être facilement résolue, 2) Étude et proposition d'un modèle analytique générique de la procédure d'accès aléatoire au canal (RACH). Le modèle a pour but l’évaluation des méthodes de contrôle de congestion ciblant la partie RAN, 3) Approfondissement et proposition des méthodes permettant d'améliorer la méthode Pagination de Groupe (GP) approuvée par le 3GPP pour contrôler la congestion.
|
|
Informatique
/ 17-06-2014
Oliveira Maroneze André
Voir le résumé
Voir le résumé
Les systèmes informatiques critiques - tels que les commandes de vol électroniques et le contrôle des centrales nucléaires - doivent répondre à des exigences strictes en termes de sûreté de fonctionnement. Nous nous intéressons ici à l'application de méthodes formelles - ancrées sur de solides bases mathématiques - pour la vérification du comportement des logiciels critiques. Plus particulièrement, nous spécifions formellement nos algorithmes et nous les prouvons corrects, à l'aide de l'assistant à la preuve Coq - un logiciel qui vérifie mécaniquement la correction des preuves effectuées et qui apporte un degré de confiance très élevé. Nous appliquons ici des méthodes formelles à l'estimation du Temps d'Exécution au Pire Cas (plus connu par son abréviation en anglais, WCET) de programmes C. Le WCET est une propriété importante pour la sûreté de fonctionnement des systèmes critiques, mais son estimation exige des analyses sophistiquées. Pour garantir l'absence d'erreurs lors de ces analyses, nous avons formellement vérifié une méthode d'estimation du WCET fondée sur la combinaison de deux techniques principales: une estimation de bornes de boucles et une estimation du WCET via la méthode IPET (Implicit Path Enumeration Technique). L'estimation de bornes de boucles est elle-même décomposée en trois étapes : un découpage de programmes, une analyse de valeurs opérant par interprétation abstraite, et une méthode de calcul de bornes. Chacune de ces étapes est formellement vérifiée dans un chapitre qui lui est dédiée. Le développement a été intégré au compilateur C formellement vérifié CompCert. Nous prouvons que le résultat de l'estimation est correct et nous évaluons ses performances dans des ensembles de benchmarks de référence dans le domaine. Les contributions de cette thèse incluent la formalisation des techniques utilisées pour estimer le WCET, l'outil d'estimation lui-même (obtenu à partir de la formalisation), et l'évaluation expérimentale des résultats. Nous concluons que le développement fondé sur les méthodes formelles permet d'obtenir des résultats intéressants en termes de précision, mais il exige des précautions particulières pour s'assurer que l'effort de preuve reste maîtrisable. Le développement en parallèle des spécifications et des preuves est essentiel à cette fin. Les travaux futurs incluent la formalisation de modèles de coût matériel, ainsi que le développement d'analyses plus sophistiquées pour augmenter la précision du WCET estimé.
|
|
Informatique
/ 25-11-2016
Bodin Martin
Voir le résumé
Voir le résumé
JavaScript est un langage de programmation maintenant très utilisé - y compris dans des domaines où la sécurité est importante. Il est donc important de permettre de vérifier la qualité des logiciels écrit en JavaScript. Cette thèse explore l'approche de la preuve formelle, visant à donner une preuve mathématique qu'un programme donné se comporte comme prévu. Pour construire cette preuve, nous utilisons un assistant de preuve tel que Coq - un programme de confiance permettant de vérifier nos preuves formelles. Pour pouvoir énoncer qu'un programme JavaScript se comporte correctement, nous avons tout d'abord besoin d'une sémantique du langage JavaScript. Cette thèse s'est donc inscrite dans le projet JSCert visant à produire une sémantique formelle pour le langage JavaScript. Devant la taille de la sémantique de JavaScript, il est important de savoir comment on peut lui faire confiance : une faute de frappe peut compromettre toute la sémantique. Pour pouvoir faire confiance à JSCert, nous nous sommes appuyés sur deux sources de confiance. D'une part, JSCert a été conçue pour être très similaire à la spécification officielle de JavaScript, le standard ECMAScript : ils utilisent les mêmes structures de donnée, et il est possible d'associer chaque règle de réduction dans JSCert à une ligne d'ECMAScript. D'autre part, nous avons défini et prouvé relativement à JSCert un interpréteur nommé JSRef. Nous avons aussi pu lancer JSRef sur les suites de test de JavaScript. La sémantique de JSCert n'est pas la première sémantique formelle pour le JavaScript, mais c'est la première à proposer deux manières distinctes pour relier la sémantique formelle au langage JavaScript : en ayant une sémantique très similaire à la spécification officielle, et en ayant testé cette sémantique pour la comparer aux autres interpréteurs. Plutôt que de prouver indépendamment que chaque programme JavaScript s'exécute comme prévu, nous analysons ses programmes par interprétation abstraite. Cela consiste à interpréter la sémantique d'un langage avec des domaines abstraits. Par exemple la valeur concrète 1 pourra être remplacée par la valeur abstraite +. L'interprétation abstraite se compose en deux étapes : d'abord une sémantique abstraite est construite et prouvée correcte vis à vis de sa sémantique concrète, puis des analyseurs sont construits selon cette sémantique abstraite. Nous ne nous intéresserons qu'à la première étape dans cette thèse. La sémantique de JSCert est immense - plus de huit cent règles de réduction. La construction d'une sémantique abstraite traditionnelle ne passent pas à l'échelle face à de telles tailles. Nous avons donc conçu une nouvelle manière de construire des sémantiques abstraites à partir de sémantiques concrètes. Notre méthode se base sur une analyse précise de la structure des règles de réduction et vise à minimiser l'effort de preuve. Nous avons appliqué cette méthode sur plusieurs langages. Dans le but d'appliquer notre approche sur JavaScript, nous avons construit un domaine basé sur la logique de séparation. Cette logique requiert de nombreuses adaptations pour pouvoir s'appliquer dans le cadre de l'interprétation abstraite. Cette thèse en étudie les interactions et propose une nouvelle approche pour les solutionner dans le cadre construit précédemment. Nos domaines, bien qu'assez simple par rapport au modèle mémoire de JavaScript, semblent permettre la preuve d'analyseurs déjà existant. Les contributions de cette thèse sont donc triples : une sémantique formelle de confiance pour le langage JavaScript, un formalisme générique pour construire des sémantiques abstraites, et un domaine non trivial pour ce formalisme.
|
|
Informatique
/ 10-12-2020
Graux Pierre
Voir le résumé
Voir le résumé
Android est le système d'exploitation le plus utilisé et donc, assurer la sécurité des applications est essentiel. Sécuriser une application consiste à empêcher les attaquants potentiels de corrompre le comportement attendu de l'application. En particulier, l'attaquant peut s'appuyer sur des vulnérabilités laissées dans le code par le développeur, mais aussi voler la propriété intellectuelle d'une application existante. Pour ralentir le travail de l'attaquant qui essaie de reverser la logique applicative, le développeur est incité à chercher les vulnérabilités potentielles et à introduire des contremesures dans le code. Parmi les contremesures possibles, l'obfuscation de code est une technique qui cache l'intention réelle du développeur en faisant en sorte de rendre le code non disponible à l'adversaire qui utilise des outils de reverser. Avec l'augmentation des applications soit malveillantes, soit manipulant des informations sensibles, obfusquer le code et chercher ses vulnérabilités devient essentiel. Cette thèse présente l'impact du code natif sur, à la fois le reversing et la recherche de vulnérabilités, appliqué à des applications Android. Premièrement, en listant les interférences possibles entre l'assembleur et le bytecode, nous mettons en évidence des nouvelles techniques d'obfuscation et vulnérabilités logicielles. Ensuite, nous proposons de nouvelles techniques d'analyse combinant des blocs d'analyse statiques et dynamiques, tels que la propagation de teintes ou la surveillance du système, afin d'observer le comportement du code qui a été obfusqué ou de révéler de nouvelles vulnérabilités. Ces deux objectifs nous ont menés à développer deux nouveaux outils. Le premier cible une vulnérabilité spécifique due à l'interaction du natif et des données Java. Le second extrait le comportement d'une application au niveau objet, que l'application contienne du code natif d'obfuscation ou non. Enfin, nous avons implémenté ces nouvelles méthodes et les avons évaluées expérimentalement. En particulier, nous avons trouvé automatiquement une vulnérabilité dans la librairie SSL d'Android et nous avons analysé plusieurs firmware Android pour détecter l'usage d'une classe spécifique d'obfuscation.
|
|
Informatique
/ 28-03-2013
Obrovac Marko
Voir le résumé
Voir le résumé
Avec l’émergence de plates-formes distribuées très hétérogènes, dynamiques et à large-échelle, la nécessité d’un moyen de les programmer efficacement et de les gérer a surgi. Le concept de l’informatique autonomique propose de créer des systèmes autogérables — des systèmes qui sont conscients de leurs composants et de leur environnement, et peuvent se configurer, s’optimiser, se guérir et se protéger. Dans le cadre de la réalisation de tels systèmes, la programmation déclarative, dont l’objectif est de faciliter la tâche du programmeur en séparant le contrôle de la logique du calcul, a retrouvé beaucoup d’intérêt ce dernier temps. En particulier, la programmation à base de des règles est considérée comme un modèle prometteur dans cette quête pour des abstractions de programmation adéquates pour ces plates-formes. Cependant, bien que ces modèles gagnent beaucoup d’attention, ils créent une demande pour des outils génériques capables de les exécuter à large échelle. Le modèle de programmation chimique, qui a été conçu suite à la métaphore chimique, est un modéle de programmation à bas de règles et d’ordre supérieur, avec une exécution non-déterministe modèle, où les règles sont appliquées simultanément sur un multi-ensemble de données. Dans cette thèse, nous proposons la conception, le développement et l’expérimentation d’un intergiciel distribué pour l’exécution de programmes chimique sur des plates-formes à large échelle et génériques. L’architecture proposée combine une couche de communication pair-à-pair avec un protocole de capture atomique d’objets sur lesquels les règles doivent être appliquées, et un système efficace de détection de terminaison. Nous décrivons le prototype d’intergiciel mettant en œuvre cette architecture. Basé sur son déploiement dans un banc d’essai réel, nous présentons les résultats de performance, qui confirment les complexités analytiques obtenues et montrons expérimentalement la viabilité d’un tel modèle de programmation.
|
|
Informatique
/ 28-04-2016
Chamaret Christel
Voir le résumé
Voir le résumé
Comme la consommation de médias numériques a explosé ces dernières années, faire des photos esthétiques, avec ou sans expertise artistique, est plus que jamais un sujet de recherche. Plusieurs axes peuvent être explorés: la haute définition, la luminance ou contraste étendue, les gamut couleur étendus. En plus de ces propriétés intrinsèques de l'image, des connaissances perceptuelles et/ou artistiques seraient de grande valeur pour tout utilisateur manipulant le contenu des images. Cette thèse propose d'aborder le thème de l'harmonie des couleurs. La littérature en lien avec ce sujet se retrouve à travers diverses disciplines : la science des couleurs, le traitement d'image, la psychologie… Ces expériences menées en science des couleurs privilégient la mesure de patchs combinant deux ou trois couleurs, rendant l'extrapolation à des images naturelles impossibles. D'autres approches ont défini des lois empiriques dictant l'arrangement des couleurs sur la roue des teintes. Le cadre applicatif de ces modèles géométriques manque de rigueur quant à leur utilisation. Malgré cela, des algorithmes en traitement d'image employant ces modèles ont vus le jour. Si les résultats semblent qualitativement agréables, ces algorithmes méritent une validation plus quantitative et objective, faisant intervenir une base de données appropriée. Dans cette thèse, deux approches sont mises en perspective: un travail expérimental et une partie algorithmique. Une expérience a été menée à l'aide d'un oculomètre avec une tâche dédiée à l'analyse de l'harmonie des couleurs, permettant de mesurer des effets dans le déploiement de l'attention visuelle. A partir de ces données, une vérité terrain a été extrapolée, permettant la validation des méthodes algorithmiques ensuite proposées. En premier, nous avons amélioré l'état de l'art sur l'harmonisation automatique des images au travers de diverses contributions et avons démontré de façon exhaustive le gain de notre approche. En deuxième contribution algorithmique, nous avons introduit une nouvelle sorte de métrique de qualité qui combine les concepts de masquage visuel et d'harmonie des couleurs. Ainsi, nous pouvons prédire quelles zones de l'image seront perçues harmonieuses, au vue de leur voisinage et donc des effets de masquages potentiels. Enfin, une dernière contribution, nous a amené à dériver deux outils d'édition incorporant les deux techniques précédentes, permettant de rendre accessible les concepts d'harmonie des couleurs à travers une formulation cachée et intuitive.
|
|
Informatique
/ 28-09-2020
Li Na
Voir le résumé
Voir le résumé
La couverture terrestre se rapporte à la couverture biophysique de la surface terrestre de la Terre, identifiant ainsi la végétation, l’eau, le sol nu ou les surfaces imperméables, etc. L’identification de la couverture terrestre est essentielle pour la planification et la gestion des ressources naturelles (e.g. d développement, protection), la compréhension de la répartition des habitats ainsi que la modélisation des variables environnementales. L’identification des types de couverture terrestre fournit des informations de base pour la production d’autres cartes thématiques et établit une base de référence pour les activités de surveillance. Par conséquent, la classification de la couverture terrestre à l’aide de données satellitaires est l’une des applications les plus importantes de la télédétection. Une grande quantité d’informations au sol est généralement nécessaire pour générer une classification de la couverture terrestre de haute qualité. Toutefois, dans les zones naturelles complexes, la collecte d’informations au sol peut-être longue et extrêmement coûteuse. De nos jours, les technologies à capteurs multiples font l’objet d’une grande attention dans la classification de la couverture terrestre. Elles apportent des informations différentes et complémentaires des caractéristiques spectrales qui peuvent aider à surmonter les limitations causées par une information au sol inadéquate. Un autre problème causé par le manque d’informations au sol est l’ambiguïté des relations entre les cartes de la couverture des terres et les cartes d’utilisation des terres. Les cartes de l’occupation des sols fournissent des informations sur les caractéristiques naturelles qui peuvent-être directement observées à la surface de la Terre. Elle font également référence à la manière dont les gens utilisent les informations sur les paysages à fins différentes. Sans informations adéquates sur le terrain, il est difficile de produire des cartes d’utilisation des sols à partir des cartes de l’occupation des sols pour des zones complexes. Par conséquent, lorsque l’on combine plusieurs cartes hétérogènes de la couverture des sols, il faut envisager comment permettre aux utilisateurs de synthétiser le schéma des cartes d’utilisation des sols. Dans notre recherche, nous nous concentrons sur la fusion d’informations hétérogènes provenant de différentes sources. Le système de combinaison vise à résoudre les problèmes causés par le nombre limité d’ échantillon étiquetés et peut-être donc utilisé dans la classification de la couverture des terres pour les zones difficiles d’accès. Les étiquettes sémantiques pour la classification de l’occupation des sols provenant de chaque capteur peuvent être différentes et peuvent ne pas correspondre au schéma final d'étiquettes que les utilisateurs attendent. Par conséquent, un autre objectif de la combinaison est de fournir une interface avec un schéma final probablement diffèrent des cartes de l’occupation des sols d’entrée.
|
|
Informatique
/ 21-10-2022
Belcour Arnaud
Voir le résumé
Voir le résumé
Le métabolisme peut être modélisé et étudié à plusieurs niveaux. Un premier niveau étudié est celui des voies métaboliques qui correspondent à des enchaînements de transformations chimiques amenant à la production de composés d'intérêt. Et c'est au travers d'une formalisation de la dérive métabolique en programmation par contraintes, que des voies métaboliques alternatives ont pu être proposées chez une algue. Un second niveau du métabolisme rassemble l'ensemble des centaines de voies métaboliques contenu dans le métabolisme d'un organisme. Une méthode visant à créer des réseaux métaboliques homogènes à partir de données publiques hétérogènes est présentée et est appliquée sur trois jeux de données bactériens et eucaryotes. Le troisième niveau est le métabolisme d'un groupe d'organisme et permet d'étudier le fonctionnement d'un organisme non spécifiquement identifié. Pour cela, une méthode reposant sur l’ingénierie des connaissances et la comparaison des séquences a été développée et a permis d'étudier le métabolisme d'une communauté bactérienne. Le dernier niveau correspond au métabolisme d'une communauté et vise à comprendre les possibles interactions métaboliques entre ces organismes. Une méthode a été développée permettant l'identification d'espèces clés au travers de la complémentarité métabolique.
|
|