Séminaire des Élèves du Département d'Informatique 2001-2002

Le séminaire des Éleves du département d'Informatique a été créé en novembre 2001. Cette page regroupe les résumés et les supports des exposés de la première année (2001-2002).

• SIDE. La nouvelle page du séminaire.

• Antoine Miné (LIENS, promo 97). Mardi 6 novembre 2001.
  Représentations de contraintes numériques simples et application à l'analyse automatique de programmes.

  Depuis longtemps, on se sert de graphes pondérés pour tester la satisfiabilité d'ensembles de contraintes d'une forme très particulière: x-y <= c (où x et y sont des variables, et c est une constante).

  Dans cet exposé, nous montrerons comment compléter cette théorie pour pouvoir l'utiliser dans le cadre de l'analyse automatique de programmes par interprétation abstraite. Il s'agit en particulier de définir des opérateurs reflétant la sémantique d'un language de programmation et d'exhiber une structure de treillis complet. C'est la construction d'un domaine numérique abstrait.

  Nous nous interesserons également aux possibilités de généralisations des graphes pondérés à d'autres classes de contraintes: +-x +-y <= c, x congru à y + b modulo a, etc. (Travail en cours.) Il semblerait que la théorie des algèbres tropicales et dioides s'applique mal ici, et qu'il faille chercher d'autres structures mathématiques.

  Cet exposé s'adresse à un public large d'informaticiens; aucune connaissance en sémantique des languages de programmations, ou en programmation par contraintes n'est requise.

  
  
  • Transparents.
  
  
• David Monniaux (LIENS). Mardi 13 novembre 2001.
  Analyse de programmes probabilistes par interprétation abstraite.

  Nous proposons un langage de formules permettant de spécifier des propriétés de traces de systèmes de transition probabilistes et non-déterministes, englobant celles spécifiables par des automates de Büchi déterministes. Ces propriétés sont en général indécidables sur des processus infinis.

  Ce langage a à la fois une sémantique concrète en termes d'ensembles de traces et une sémantique abstraite en termes de fonctions mesurables. Nous appliquons ensuite des techniques d'interprétation abstraite pour calculer un majorant de la probabilité dans le pire cas de la propriété étudiée et donnons une amélioration de cette technique lorsque l'espace d'états est partitionné, par exemple selon les points de programme. Nous proposons deux domaines abstraits convenant pour cette analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les gaussiennes étendues.

  Il est également possible d'obtenir de tels majorants par des calculs propageant les mesures de probabilité en avant. Nous donnons une méthode d'interprétation abstraite pour analyser une classe de formules de cette façon et proposons deux domaines abstraits adaptés à ce type d'analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les queues sous-exponentielles. Ce dernier permet de prouver la terminaison probabiliste de programmes.

  
  
  • Transparents.
  
  
• Augustin Chaintreau (LIENS, promo 98). Mardi 20 novembre 2001.
  Equation linéaires dans les dïoides, Utilité, Résultats et Applications.

  Le cadre (MAX,+)

  L'opération max se distribue sur l'opération +, en effet de la même manière que l'on a (a+b)c=ac+bc pour l'addition et la multiplication, on observe que l'on a max(a,b)+c=max(a+c,b+c), offrant alors la possibilité d'interpreter l'opération de maximum comme une nouvelle addition, et l'opération somme comme une nouvelle multiplication sur cette addition. Agir ainsi consiste à se placer dans l'algèbre (max,+), qui est un cas particulier de structures à deux opérations, où tous les propriétés classiques d'anneau et de corps peuvent se retrouver - il est ainsi possible de définir un nouveau zéro et une nouvelle unité, avec des propriétés semblables au cas classique - à l'exception de l'un des axiomes, à savoir que ce que l'on définit maintenant comme «addition» ne peut être inversée. En effet l'opération de maximum ne saurait donner lieu à une structure de groupe (l'appliquer induit nécessairement une «perte d'information»).

  Cette différence se développe dans des espaces de matrices vers une image assez déformée de la théorie classique de l'algèbre linéaire. En particulier il est possible d'écrire une théorie spectrale, directement inspirée des résultats de Perron-Frobenius sur les matrices à coefficients positifs, avec laquelle elle partage nombre de définitions et de formulations de résultats ; parfois même les preuves sont de même nature.

  L'intérêt d'obtenir ces résultats dans un cadre linéaire plus faible n'est pas négligeable. Une large classe de problèmes introduits dans l'étude des systèmes de décisions ou de contraintes, dans certains problèmes d'asymptotiques de physique quantique, ou dans la formalisation de la théorie des langages se factorisent dans ce nouveau cadre, ramenant cette étude aux propriétés de transformations «linéaires», où la linéarité a été redéfinie sur des critères différents.

  Présentation

  L'introduction des structures sera motivée par l'étude d'un problème simple, qui motivera aussi la description d'une nouvelle théorie spectrale dont on présentera les premiers developpements. Du temps sera ensuite consacré à la présentation d'autres domaines où ces méthodes sont utiles.

  
  
  • Transparents.
  
  
• Gilles Peskine (project Moscova, INRIA, promo 98). Mardi 4 décembre 2001.
  Le join-calcul, un calcul pour la programmation concurrente et distribuée.

  Le join-calcul est un modèle des systèmes concurrents. Il est défini en termes de processus --- dont la structure varie au cours du temps --- qui communiquent en s'envoyant des messages et pour le reste font des pas de calcul séparément. L'originalité du join-calcul par rapport à d'autres modèles qui permettent de raisonner sur les systèmes concurrents est son adaptation naturelle à la programmation distribuée, c'est-à-dire qu'un programme du join-calcul peut être constitué de composants tournant sur des machines différentes.

  Nous présenterons le join-calcul sur des exemples, et nous donnerons sa sémantique opérationnelle (la machine chimique abstraite réflexive). Nous verrons ensuite comment l'ajout d'une notion de location permet de modéliser la distribution et la mobilité. Nous discuterons des problèmes qui apparaissent lorsqu'on implémente un langage de programmation distribué, comme le routage des messages et le traitement des pannes.

  
  
  • Transparents.
  
  
• Jerôme Feret (LIENS, promo 97). Mardi 11 décembre 2001.
  Interprétation Abstraite des Systèmes Mobiles.

  Les systèmes mobiles mettent en jeu un nombre arbitraire d'agents. Ces agents peuvent déclarer des noms qu'ils sont, dans un premier temps, les seuls à pouvoir utiliser, puis communiquer ces noms à d'autres agents qui obtiennent alors le droit de les utiliser. Ainsi la topologie des interactions entre les agents d'un système mobile varie dynamiquement au cours du temps, ce qui rend l'analyse de ses propriétés difficile.

  Nous proposons une méthode, basée sur l'Interprétation Abstraite pour calculer et prouver automatiquement des invariants vérifiés au cours de toutes les exécutions potentielles d'un système mobile qui intéragit avec un contexte inconnu et hostile. Nous travaillons plus spécifiquement sur les systèmes décrits dans le formalisme du pi-calcul. Nous nous concentrons d'une part sur les relations entres les noms qui peuvent être communiqués aux agents (les noms liées aux variables x et y sont-ils toujours égaux, différents ? Ont-ils été créés par la même instance récursive d'un agent ?) et d'autre part sur le nombre d'instances d'agents présents au cours de l'exécution du système. Nous pourrons montrer en particulier la confidentialité de certaines informations, des exclusions mutuelles entre agents, la non-épuisement des resources utilisées par le système.

  Cette première analyse permet de construire un partitionement fini de l'ensemble de toutes les configurations que peut prendre un système mobile, ce qui permet de calculer une approximation de la sémantique de trace de notre système mobile sous forme d'automate. On pourra par exemple découvrir un ensemble d'états tel que toute exécution passant par un de ses états termine.

• Yves Verhoeven (promo 99). Mardi 18 décembre 2001.
  Sécurité prouvée des schémas de chiffrement basés sur RSA.

  Obtenir des schémas de chiffrement «~sûrs~» constitue un des objectifs principaux de la cryptographie. Mais les problèmes sont nombreux pour obtenir une solution intéressante, la difficulté majeure résidant dans l'optimisation du rapport entre la sécurité du schéma, et la restriction du modèle considéré.

  Nous nous intéresserons essentiellement à la sécurité des schémas de chiffrement utilisant RSA comme primitive cryptographique de base.

  Nous verrons dans un premier temps, au travers de deux exemples de cryptanalyses pourquoi l'utilisation d'une telle primitive ne va pas sans poser de problèmes. Nous présenterons notamment une cryptanalyse sous oracle de PKCS #1 (norme utilisée dans SSL) due à Bleichenbacher.

  Nous verrons ensuite certaines méthodes qui ont été proposées pour y apporter des solutions satisfaisantes au niveau de leur efficacité calculatoire, et possédant des arguments de sécurité en leur faveur (=pour lesquelles on dispose d'une preuve de sécurité dans un modèle idéalisé).

  
  
  • Transparents.
  
  
• Éric Colin de Verdière (promo 97, LIENS). Mardi 8 janvier 2002.
  Méthode barycentrique de Tutte et isotopies : de la 2D à la 3D ?

  Dans cet exposé, on s'intéressera aux plongements de graphes (dans le plan) ou de complexes simpliciaux (en dimension trois), ainsi qu'aux déformations continues de ces plongements. Ces questions de déformations sont au coeur des problèmes rencontrés notamment dans la construction de métamorphoses entre deux images (morphing).

  Considérons un graphe T=(V,E) triangulé, c'est-à-dire admettant un plongement Γ dans le plan, à arêtes rectilignes, tel que chaque face, y compris la face non bornée, soit incidente à trois sommets et trois arêtes.

  Dans un tel plongement Γ, il est clair que chaque sommet intérieur est barycentre à coefficients strictement positifs de ses voisins. Le théorème barycentrique de Tutte fournit une réciproque : soit T=(V,E) triangulé ; pour qu'une application Γ: V → R^2 soit un plongement, il faut et il suffit que les sommets extérieurs ne soient pas alignés et que chaque sommet intérieur soit barycentre à coefficients strictement positifs de ses voisins.

  On expliquera comment ce théorème donne un moyen de construire des isotopies (familles continues de plongements de graphes). La généralisation de ces méthodes en dimension supérieure constitue aussi un enjeu important : on montrera que l'analogue naturel au théorème de Tutte en trois dimensions est faux. En fait, contrairement au cas bidimensionnel, on verra qu'il existe deux plongements d'un même complexe simplicial de dimension trois, la frontière étant le bord d'un tétraèdre fixé, entre lesquels il n'existe pas d'isotopie.

  Travail réalisé avec Michel Pocchiola et Gert Vegter.

  
  
• Benjamin Leperchey (promo 99). Mardi 22 janvier 2002.
  Programmation orientée aspects : concepts et mise en oeuvre.

  La programmation orientée aspects est un paradigme récent (Gregor Kiczales, 1997), qui complète la programmation orientée objet : que faire quand on doit programmer des structures qui «croisent» la hiérarchie des classes? On les regroupe en aspects, en morceaux de code séparés de leur contexte, avec un «mode d'emploi» qui indique à quels moments les appliquer.

  Le principal problème réside alors dans la compilation des programmes : il s'agira de les éxécuter rapidement (sans augmentation de complexité), puis de les récrire sans aspects, pour pouvoir les compiler.

  
  
• Francesco Zappa Nardelli (LIENS). Mardi 5 fevrier 2002.
  Processus et équivalences : un petit plongement dans la sémantique de la concurrence.

  Depuis longtemps, on sait que la question ``ces deux systèmes sont-ils équivalents ?'' admet plusieurs réponses, toutes raisonnables.

  Dans cet exposé, on s'intéressera à des résultats classiques en sémantique de la concurrence, avec l'espoir de comprendre l'origine et les motivations des différentes notions d'équivalence. Aucune connaissance en sémantique de la concurrence est requise ; par contre, il sera utile d'avoir déjà interagi avec une machine à café.

  
  
• Vincent Simonet (INRIA, projet Cristal). Mardi 9 avril 2002.
  Inférence de flots d'information pour ML.

  L'analyse de flots d'information consiste à déterminer si un programme satisfait certaines propriétés de confidentialité ou d'intégrité vis-à-vis des données qu'il manipule, en analysant les dépendances entre ses entrées et ses sorties : par exemple, si une entrée est considérée "secrète", on souhaitera généralement que des sorties "publiques" n'en dépendent pas. Une solution naturelle consiste à effectuer cette analyse à l'aide d'un système de types annotés par des niveaux d'information, afin de pouvoir s'assurer du bon comportement d'un programme avant son exécution.

  Lors de l'exposé, nous présenterons un tel système pour un lambda-calcul en appel par valeur doté d'un "let" polymorphe, de traits impératifs (références, exceptions) et de "primitives" (opérations arithmétiques, hachage, marshalling...). Il s'agit d'un système de types "à la ML" avec contraintes et doté de sous-typage. Sa correction, exprimée par un énoncé de "non-interférence", est ramenée à la preuve d'une propriété de "subject-reduction" pour un langage non standard dans lequel on peut raisonner sur les points communs entre deux exécutions distinctes d'un programme.

  Enfin, l'inférence de types est décidable dans ce système. On peut ainsi envisager son intégration en tant qu'extension d'un langage de programmation réaliste, tel que le langage Caml.