Institut de Mathématiques de Luminy

THÈSES 2007-2008


Dates soutenances Noms et titres thèmes Photos
3 juillet 2008 Olivier FAURAX
Méthodologie d'évaluation par simulation de la sécurité des circuits face aux attaques par faute
ATI Olivier Faurax
Photos
18 juin 2008 Anne CRUMIÈRE
Circuits de rétroaction dans les réseaux génétiques de régulation intercellulaires
LDP
12 juin 2008 Laurent BOBELIN
Tomographie depuis plusieurs sources vers de multiples destinations dans les réseaux de grilles informatiques hautes performances
ATI Laurent Bobelin
18 avril 2008 Paolo Di GIAMBERNARDINO
Jump from parallel to sequential proofs: on polarities and sequentiality in linear logic
LDP Paolo_Di_Giamberardino
21 février 2008 Minh-Tang KHUU
Sûreté de fonctionnement des systèmes
LPD  
28 novembre 2007 Nivaldo de GOES GRULHA Jr
Classes caractéristiques de variétés singulières
SGT
23 novembre 2007 Lionel VAUX
Lambda calcul différentiel et logique classique :
interactions calculatoires
LDP
29 octobre 2007 Axel FERRARI
Théorème de l'indice
et formule des traces d'Arthur-Selberg
RGR  
27 septembre 2007 Mathias FUCHS
K-théorie et cohomologie cyclique des produits croisés associés aux groupes de Lie
AOG
6 septembre 2007 Anis BEN ISHAK
Sélection de variables par les machines à vecteurs supports pour la discrimination binaire et multiclasse en grande dimension
MMG  
4 septembre 2007 Daniel de CARVALHO
Sémantiques de la logique linéaire
et temps de calcul
LDP




Olivier FAURAX
(thème ATI)

Titre : Méthodologie d'évaluation par simulation de la sécurité des circuits face aux attaques par faute.

Directeurs de thèse : Traian Muntean (Robert Rolland).

Rapporteurs : Jean Arlat, Jean-Jacques Quisquater.

Jury : Jean Arlat, Jean-Jacques Quisquater, Traian Muntean, Frédéric Bancel, Alexis Bonnecaze, Pierre Paradinas, Assia Tria.

Date : 3 juillet 2008

Université d'inscription : Aix-Marseille II

Résumé : Les circuits microélectroniques sécuritaires sont de plus en plus présents dans notre quotidien (carte à puce, carte SIM) et ils renferment des informations sensibles qu’il faut protéger (numéro de compte, clé de chiffrement, données personnelles).
Récemment, des attaques sur les algorithmes de cryptographie basées sur l’utilisation de fautes ont fait leur apparition. L’ajout d’une faute lors d’un calcul du circuit permet d’obtenir un résultat faux. À partir d’un certain nombre de résultats corrects et de résultats faux correspondants, il est possible d’obtenir des informations secrètes et dans certains cas des clés cryptographiques complètes.
Cependant, les perturbations physiques utilisées en pratique (impulsion laser, radiations, changement rapide de la tension d’alimentation) correspondent rarement aux types de fautes nécessaires pour réaliser ces attaques théoriques.
Dans ce travail, nous proposons une méthodologie pour tester les circuits face aux attaques par faute en utilisant de la simulation. L’utilisation de la simulation permet de tester le circuit avant la réalisation physique mais nécessite beaucoup de temps. C’est pour cela que notre méthodologie aide l’utilisateur à choisir les fautes les plus importantes pour réduire signi cativement le temps de simulation.
L’outil et la méthodologie associée ont été testés sur un circuit cryptographique (AES) en utilisant un modèle de faute utilisant des délais. Nous avons notamment montré que l’utilisation de délais pour réaliser des fautes permet de générer des fautes correspondantes à des attaques connues.

Mots clefs : DFA, attaque par faute, sécurité, informatique, cryptographie, microélectronique, simulation, AES, carte à puce.

Abstract: Microelectronic security devices are more and more present in our lives (smart-cards, SIM cards) and they contains sensitive informations that must be protected (account number, cryptographic key, personal data).
Recently, attacks on cryptographic algorithms appeared, based on the use of faults. Adding a fault during a device computation enables one to obtain a faulty result. Using a certain amount of correct results and the corresponding faulty ones, it is possible to extract secret data and, in some cases, complete cryptographic keys.
However, physical perturbations used in practice (laser, radiations, power glitch) rarely match with faults needed to successfully perform theoretical attacks.
In this work, we propose a methodology to test circuits under fault attacks, using simulation. The use of simulation enables to test the circuit before its physical realization, but needs a lot of time. That is why our methodology helps the user to choose the most important faults in order to significantly reduce the simulation time.
The tool and the corresponding methodology have been tested on a cryptographic circuit (AES) using a delay fault model. We showed that use of delays to make faults can generate faults suitable for performing known attacks.

Keywords : DFA, fault attack, security, computer science, cryptography, microelectronics, simulation, AES, smartcard.

Fichier / File

( 4,13 Mo)

Page personnelle (homepage) : http://ofaurax.free.fr/



Anne CRUMIÈRE
(thème LPD)

Titre : Circuits de rétroaction dans les réseaux génétiques de régulation intercellulaires.

Directeurs de thèse : Alain GUÉNOCHE, Paul RUET.

Rapporteurs : Alexander Bockmayr, Vincent Danos.

Jury : Alexander Bockmayr, Jean-Luc Gouze, Alain Guénoche, Marcelle Kaufman, Paul Ruet, Denis Thieffry.

Date : 18 juin 2008

Université d'inscription : Aix-Marseille II

Introduction : L’organisation et le développement des organismes multicellulaires dépendent en partie de l’expression différentielle des gènes. Des protéines régulatrices activent des gènes particuliers à chaque cellule et à chaque stade du développement. Ainsi l’expression des gènes est régulée par des protéines issues de l’expression d’autres gènes. L’ensemble de ces interactions génétiques est appelé réseau génétique.
La modélisation de ces réseaux et l’étude de leur dynamique seront le thème fondamental de cette thèse. Avant d’en aborder la formalisation mathématique, commençons par une brève introduction au fonctionnement d’une cellule, destinée principalement aux néophytes de la biologie cellulaire [...]

Fichier / File

( 895 Ko)

Page personnelle (homepage) : http://iml.univ-mrs.fr/~crumiere/



Laurent BOBELIN
(thème ATI)

Titre : Tomographie depuis plusieurs sources vers de multiples destinations dans les réseaux de grilles informatiques hautes performances.

Directeurs de thèse : Traian Muntean, François Touchard (A. Bonnecaze).

Rapporteurs : Emmanuel Jeannot, Ibrahima Sakho.

Jury : Emmanuel Jeannot, Ibrahima Sakho, Frédéric Desprez, Remi Morin, Traian Muntean, François Touchard.

Date : 12 juin 2008

Université d'inscription : Aix-Marseille II

Introduction : Identifier et déduire les performances et la topologie d'un réseau est une problématique classique. Résoudre ce problème en utilisant uniquement des tests de niveau applicatif, une méthode appelée tomographie réseau, a été souvent proposé pour déterminer les performances du réseau d'un point de vue client/serveur. Quand la déduction de topologie est basée sur les valeurs d'une métrique, on parle de Metric Induced Network Topology (MINT).
Les grilles actuelles peuvent connecter des milliers de ressources communicantes qui peuvent interagir de manière partiellement ou totalement coordonnée lors d'échanges de données massifs. De fait, ces communications impliquent de façon concomitante plusieurs sources et plusieurs destinations, rendant caduc le modèle client/serveur.
Dans cette thèse, j'introduis de nouvelles représentations de la connaissance du réseau obtenues au cas d'un paradigme de communication comprenant de multiples sources et de multiples destinations, des algorithmes pour reconstruire de telles représentations à partir d'un jeu de données initial, ainsi que des méthodes pour obtenir à partir de mesures de bout en bout ce jeu de données.
Je décris aussi l'outil M.I.N.T.C.A.R. que j'ai conçu et développé pendant cette thèse pour implémenter l'ensemble de ces algorithmes et méthodes ainsi que les expériences menées pour valider ces méthodes et algorithmes.

Mots clefs : tomographie, réseau, grille, EGEE.

Fichier / File

( 3 Mo)

Page personnelle (homepage) :http://graal.ens-lyon.fr/~lbobelin/



Paolo Di GIAMBERNARDINO
(thème LPD)

Titre : Jump from parallel to sequential proofs: on polarities and sequentiality in linear logic.

Directeurs de thèse : Thomas EHRHARD, Jean-yves GIRARD, Michele ABRUSCI.

Date : 18 avril 2008

Université d'inscription : Aix-Marseille 2 / Roma 1

Introduction : The topic of the present thesis is the relation between parallelism and sequentiality in proofs. More precisely, in the framework of linear logic, we study the connection between two of its most crucial discoveries: proof nets and polarities.
Let us try to explain better the point. When we write down a proof of a formula A, we may choose to depict it as a chain of inferences, ending with an inference which concludes A; or rather, more finely, we could represent the proof as a tree of inference rules, for instance in sequent calculus. However, such a style of representation does not seem to properly capture the intrinsic nature of a proof, since it makes distinctions between proofs which are “morally” the same : consider for example, two proofs of the same formula differing only for some inessential variations in the order of application of rules.
Following such an intuition, a proof does not appear to be intrinsically tied to some specific succession of its inferences, but it resembles rather a parallel process: as a matter of fact, if two inference rules in a proof are mutually independent (that is, if we can permute them), we could imagine of applying each of them separately, in parallel.
In other words, a proof is more than a plain, ordered sequence of logical rules ; linear logic provides mathematical substance to this claim, introducing the notion of proof net.

Fichier / File

( 779 Mo)

Page personnelle (homepage) : http://w3.uniroma1.it/digiamberardino/homepage_1.htm



Minh-Tang KHUU
(thème LPD)

Titre : Sûreté de fonctionnement des systèmes.

Directeur de thèse : Antoine RAUZY.

Rapporteurs : .

Jury : .

Date : 21 février 2008

Université d'inscription : Aix-Marseille II

Résumé :

Fichier / File

( Mo)

Page personnelle (homepage) :



Nivaldo de GOES GRULHA Jr
(thème SGT)

Titre : Classes caractéristiques de variétés singulières.

Directeurs de thèse : Maria Aparecida SOARES RUAS, Jean-Paul BRASSELET.

Rapporteurs : .

Jury : .

Date : 28 novembre 2007

Université d'inscription : Aix-Marseille II

Résumé :

Fichier / File

( Mo)

Page personnelle (homepage) : http://www.icmc.usp.br/~njunior/



Lionel VAUX
(thème LDP)

Titre : Lambda calcul différentiel et logique classique : interactions calculatoires.

Directeurs de thèse : Laurent REGNIER et Thomas EHRHARD.

Rapporteurs : Pierre-Louis Curien, Philip Scott.

Jury : Pierre-Louis Curien, Philip Scott, Jean-Yves Girard, Hugo Herbelin, Thomas Ehrhard Laurent Regnier.

Date : 23 novembre 2007

Université d'inscription : Aix-Marseille II

Fichier / File

(1,33 Mo)

Page personnelle (homepage) : http://iml.univ-mrs.fr/~vaux/these/



Axel FERRARI
(thème RGR)

Titre : Théorème de l'indice et formule des traces d'Arthur-Selberg.

Directeurs de thèse : Jean-Pierre LABESSE et Patrick DELORME.

Rapporteurs : .

Jury : .

Date : 29 octobre 2007

Université d'inscription : Aix-Marseille II

Résumé :

Fichier / File

( Mo)

Page personnelle (homepage) :



Mathias FUCHS
(thème AOG)

Titre : K-théorie et cohomologie cyclique des produits croisés associés aux groupes de Lie.

Directeur de thèse : Michael PUSCHNIGG.

Rapporteurs : Joachim Cuntz, Christian Kassel.

Jury : Joachim Cuntz, Pierre Julg, Christian Kassel, Christophe Pittet, Michael Puschnigg, Antony Wassermann.

Date : 27 septembre 2007

Université d'inscription : Aix-Marseille II

Résumé :

Mots-clés : K-théorie, coholomogie cyclique, groupes de Lie.

Title : K-theory and cyclic cohomology .

Abstract:

Keywords : K-theory, cyclic cohomology, Lie group.

Fichier / File

(1 Mo)

Page personnelle (homepage) : http://iml.univ-mrs.fr/~fuchs/



Anis BEN ISHAK
(thème MMG)

Titre : Sélection de variables par les machines à vecteurs supports pour la discrimination binaire et multiclasse en grande dimension.

Directeurs de thèse : Badih GHATTAS, Abdelwahed TRABELSI.

Rapporteurs : Khaled Mellouli, Jean-Michel Poggi.

Jury : Claude Deniau, Khaled Mellouli, Jean-Michel Poggi, Denys Pommeret, Abdelwaheb Rebai.

Date : 6 septembre 2007

Université d'inscription : Aix-Marseille II

Résumé : Cette thèse est consacrée à la sélection de variables pour la discrimination binaire et multiclasse en grande dimension.
Dans les deux premiers chapitres, nous introduisons brièvement les concepts de base de la théorie de l’apprentissage statistique et des machines à vecteurs supports (SVM).
Dans le troisième chapitre, nous proposons une nouvelle méthode de sélection de variables basée sur des scores d’importance dérivés des SVM. Les variables sont introduites dans le modèle selon l’ordre d’importance décroissant.
Dans le chapitre quatre, nous comparons différentes méthodes récentes de sélection de variables basées sur les SVM, les GLM sous contrainte de type L1 et les forêts aléatoires.
Le dernier chapitre traite de la généralisation de notre travail au cas multiclasse.
Nous illustrons l’efficacité de nos approches sur des données simulées et sur des données de biopuces. Les résultats montrent une amélioration significative des performances de prédictives en utilisant peu de variables.

Mots-clés : machines à vecteurs supports (SVM), élimination récursive des variables (SVM-RFE), forêts aléatoires, modèles linéaires généralisés et régularisés (GLMpath), hiérarchies de variables, sélection de variables, biopuces, bootstrap, biais de sélection, stepwise, multiclasse.

Title : problem of feature selection for binary and multiclass discrimination in high dimension.

Abstract: This dissertation is dedicated to the problem of feature selection for binary and multiclass discrimination in high dimension.
In the first two chapters we briefly introduce the basic concepts of statistical learning theory and support vector machines (SVM).
In the third chapter we suggest a new method of feature selection based on ranking scores derived from SVM. Our feature selection algorithm consists in a forward selection strategy according to the decreasing order of the variable importance.
In chapter four we compare several recent feature selection methods based on SVM, L1 constrained Generalized Linear Models and Random Forests.
The last chapter deals with the generalization of our work to the multiclass classification case.
We illustrate the effectiveness of our approaches on synthetic data and some challenging benchmark problems based on microarray data. Results demonstrate a significant improvement of generalization performance using a few variables.

Keywords : support vector machines (SVM), recursive feature elimination (SVM-RFE), random forests, generalized linear models with regularization (GLMpath), variables hierarchy, variable selection, microarray, bootstrap, selection bias, stepwise, multiclass.

Fichier / File

( 2,23 Mo)



Daniel de CARVALHO
(thème LDP)

Titre : Sémantiques de la logique linéaire et temps de calcul.

Directeur de thèse : Thomas EHRHARD.

Rapporteurs : Martin Hyland, Lorenzo Tortora de Falco.

Jury : Patrick Baillot, Pierre-Louis Curien, Thomas Ehrhard, Martin Hyland, François Lamarche, Kazushige Terui, Lorenzo Tortora de Falco.

Date : 4 septembre 2007

Université d'inscription : Aix-Marseille II

Résumé : Cette thèse étudie les exponentielles de la logique linéaire sous différents aspects.
Des exponentielles hétérodoxes avec un travail sur une variante du lambda-calcul proposée par Terui (le lambda-calcul “light”) qui permet de représenter toutes les fonctions calculables en temps polynomial, et seulement elles. Ce calcul s’inspire du système LLL de Girard et contrôle le temps de calcul en décomposant la beta-réduction en étapes correspondant à des étapes de réduction de logique linéaire, au moyen d’un mécanisme de pattern-matching. Nous développons pour ce langage un système de types avec intersection garantissant l’absence de deadlocks durant la réduction.
Nous intéressant toujours aux types avec intersection, nous avons travaillé ensuite sur le lambda-calcul usuel, cherchant à établir des liens plus généraux entre temps de calcul et types. Dans ce but, nous avons considéré un système de types avec intersections non idempotentes, basé sur le modèle relationnel multiensembliste du lambda-calcul. Ce système est essentiellement identique à un système de types introduit en 1980 par Coppo, Dezani et Venneri, que nous situons ainsi dans son environnement naturel : une catégorie de co-Kleisli au-dessus de la catégorie des ensembles et des relations. Nous avons établi un lien étroit entre la taille des dérivations de types des termes dans ce système et leur temps d’exécution dans la machine de Krivine, un modèle d’évaluation des lambda-termes proche des machines à environnement utilisées en pratique pour l’évaluation des langages de programmation fonctionnels. Notre résultat peut être vu comme un raffinement quantitatif du théorème bien connu qui énonce qu’un lambda-terme est normalisable si et seulement si il est typable dans les types avec intersection.
Enfin, nous étudions la sémantique de la logique linéaire différentielle, un formalisme que Ehrhard a introduit il y a quelques années avec Régnier et dont il a récemment montré avec Laurent qu’il fournit un nouveau modèle du calcul concurrent et mobile. Nous avons considéré des modèles du fragment finitaire de cette logique (sans promotion) et montré comment on pouvait définir la promotion en utilisant une version catégorique de la formule de Taylor. Nous avons obtenu ainsi des semi-foncteurs pour interpréter les exponentielles de la logique linéaire et en avons étudié les propriétés, en fonction des propriétés algébriques (commutativité et cocommutativité) de l’interprétation finitaire sous-jacente. Nous avons obtenu de cette façon de nouveaux modèles, où les exponentielles (orthodoxes) ont des interprétations non standard, ainsi que des interprétations non invariantes par réduction, qui ont sûrement un grand intérêt pour l’étude de l’élimination des coupures.

Mots-clés : sémantique dénotationnelle, lambda-calcul, logique linéaire, types avec intersection, réseaux différentiels, temps de calcul, complexité implicite.

Fichier / File

(723 Ko)

Page personnelle (homepage) : http://www.loria.fr/~decarvad/


Last update : september 24, 2009, EL.