Séminaires 2008-09
- 20 octobre 2008
- Abdelhamid Mellouk (LISSI)
- Des approches adaptatives pour une meilleure garantie de
service dans les réseaux à trafic irrégulier
- Résumé :
La nature des flux circulant sur le réseau, la constante progression des besoins
des utilisateurs et l'utilisation des nouvelles générations de réseau dans le cadre
d'applications multimédia induisent de manière intrinsèque un trafic très variable
se caractérisant de plus en plus par des anomalies ayant pour conséquence des changements
d'états imprévisibles dans le réseau.
L'intégration de ce nouveau phénomène dans les
politiques de décision afin de répondre au mieux aux aspects
liés à la qualité de service
constitue un vaste sujet de recherche et a fait l'objet de nombreuses techniques proposées
dans la littérature. L'objectif de ce séminaire est de faire le point sur les approches
réactives, parfois appelées autonomes, développées dans le cadre d'une garantie de service
bout en bout (intra et inter domaines) incluant différents paramètres : délai, bande passante,
fiabilité, sécurité, etc. Nous nous focaliserons en particulier sur les fonctions liées au
routage et présenterons un système développé au sein du laboratoire permettant de faire un
routage sous contraintes, statiques et dynamiques, et basé sur des techniques d'apprentissage.
L'objectif est celui d'optimiser le niveau de service offert par le réseau en rendant ses
mécanismes de routage capables, d'une part, de s'adapter aux conditions et à la nature du trafic
et, d'autre part, à l'utilisation des ressources du réseau.
- 3 novembre 2008
- Sylvie Boldo (LRI)
- Preuves de programmes numériques
- Résumé :
Dans cet exposé, je présenterai tout d'abord l'arithmétique à
virgule flottante et ses limites. Je présenterai ensuite comment, en utilisant la
plate-forme Why et l'outil Caduceus, on peut spécifier précisément un
programme numérique. Ces spécifications ont pour but d'être transformées
en obligations de preuves qui seront ensuite formellement prouvées à la main ou
automatiquement. Je décrirai la syntaxe des annotations flottantes et je montrerai quelques
applications de programmes numériques formellement prouvés.
- 17 novembre 2008 exposé à 14h
- Florian Kerschbaum
- A Privacy-Preserving Benchmarking Platform
- Résumé :
Benchmarking is an important process for companies to stay competitive in today's markets and
is the comparison of one company's key performance indicators (KPI) to the statistics of the same
KPIs of its peer group. In this talk I will present the design, implementation and evaluation of
a privacy-preserving benchmarking platform that allows its participants to securely and privately
compare its KPIs to the statistics, i.e. without revealing them to each other. We cover three
important aspects of such a platform: the design of an efficient secure multi-party computation
protocol, the system's architecture forming profitable peer groups and the implementation and its
evaluation optimizing the system's performance.
- 24 novembre 2008
- Joel Falcou (LRI)
- Programmation Générative et Méta-programmation -- Application à la programmation parallèle
- Résumé :
Les besoins croissants en puissance de calcul exprimés par de nombreux domaines scientifiques exercent une pression très forte sur les architectures émergentes, les rendant toujours plus performantes mais toujours plus complexes à maîtriser. Dans ce cadre, le développement d'outils tirant parti des spécificités de ces architectures (quadri- et bientôt octo-coeurs, processeurs Cell ou GPU par exemple) devient une gageure car allier expressivité et efficacité est une tâche ardue. Les travaux exposés ici montrent comment l'utilisation de la programmation générative, et en particulier de la méta-programmation tant en C++ qu'en OCaml permet de répondre au problème de performances et d'abstractions. Nous montrerons comment ces techniques ont permis de développer Quaff, un outil de placement automatique d'applications data-flow sur des cibles variées comme les clusters, les multi-coeurs ou le processeur Cell.
- 1er décembre 2008
- Sophie Robert (LIFO)
- FlowVR un environnement de programmation pour la visualisation scientifique interactive haute performance
- Résumé :
Après une présentation générale des thèmes de recherche en Réalité Virtuelle de l'équipe PRV (Parallélisme Réalité virtuelle et Vérification) du LIFO, ce séminaire aura pour premier objectif de présenter FlowVR un intergiciel basé sur un modèle de programmation orienté composants. Ensuite nous verrons dans quelles mesures il peut répondre aux besoins spécifiques des applications de visualisation interactive. Cet axe d'étude mène à des extensions de FlowVR et nous détaillerons un cas particulier, FlowVR-VRPN, qui concerne l'utilisation de différents périphériques de RV et l'intégration de leurs événements dans toute application de ce type avec les difficultés de synchronisation que cette intégration induit.
- 8 décembre 2008
- Sandrine Blazy (ENSIIE)
- Un parcours de la compilation certifiée à la preuve de programmes
- Résumé :
Dans cet exposé, je présenterai succinctement un compilateur optimisant du langage C appelé CompCert, ayant été formellement vérifié avec l'assistant à la preuve Coq. Je détaillerai en particulier la sémantique du principal langage intermédiaire du compilateur, qui a été définie selon différents styles de sémantique, ainsi que le modèle mémoire du compilateur. Enfin, j'expliquerai comment ces travaux ont été réutilisés pour construire un environnement dédié à la preuve de programmes en logique de séparation.
- 15 décembre 2008
- Mathieu Jaume (LIP6 - SPI)
- Un cadre formel pour le contrôle d'accès
- Résumé :
Un des aspects de la sécurité en informatique concerne le
contrôle des accès aux données d'un système pour lequel différentes
politiques de sécurité peuvent être mises en application. Cet exposé
porte sur la définition d'un ``cadre sémantique'' dans lequel il est possible
de spécifier et d'implanter des politiques de contrôle d'accès. Ce cadre permet
de définir des mécanismes de comparaison de modèles et
d'analyser ces modèles en termes de flots d'information qu'ils autorisent.
- 12 janvier 2009
- Marc Frappier (Université de Sherbrooke)
- Diagrammes état-transition algébriques
- Résumé :
Les statecharts de David Harel sont largement utilisés pour la modélisation et la conception de systèmes. Toutefois, il est très difficile d'exprimer complètement le comportement d'un système d'information à l'aide de statecharts. Cette notation ne permet pas d'exprimer facilement le comportement de plusieurs instances d'une entité qui interagissent. Nous présenterons une extension des statecharts qui permet de les combiner avec des opérateurs d'une algèbre de processus. Le résultat est donc une fusion des notions de diagrammes état-transition hiérarchiques et d'algèbre de processus, qui allie l'expressivité des notations graphiques avec le pouvoir d'abstraction d'une algèbre. Les opérateurs considérés sont la séquence, le choix, la synchronisation, la garde, la fermeture de Kleene, ainsi que des quantifications sur les opérateurs de choix et de synchronisation, afin de spécifier facilement le comportement d'un nombre arbitraire d'instances. La notation proposée est très générale: un automate hiérarchique est une expression de processus élémentaire; un état d'un automate hiérarchique peut être une expression de processus. La notation est entièrement graphique. La sémantique est définie de manière opérationnelle, grâce à des règles d'inférence définissant un système de transition étiquetée.
- 19 janvier 2009
- Serghei Verlan (LACL)
- Les ordinateurs biologiques: fiction ou réalité ?
- Résumé :
Le calcul bio-moléculaire (DNA computing) se situe à la rencontre de la biologie, chimie et informatique. Il essaie d'utiliser les moyens bio-chimiques pour effectuer des calculs. L'ordre de grandeur des ingrédients et le parallélisme massif donnent l'espérance que certains problèmes difficiles, en particulier les problèmes NP-complets, pourront être résolus plus facilement. Dans la présentation on donnera un aperçu du domaine en présentant les modèles principaux et les expériences importantes.
- 26 janvier 2009
- Konrad Hinsen
- BSP en Python: applications pour le calcul scientifique
- Résumé :
eaucoup d'applications scientifiques nécessitent des moyens de calcul importants et pourraient bénéficier du calcul parallèle. Souvent le plus grand obstacle à la parallélisation n'est pas dans les algorithmes, mais dans l'implémentation: la programmation avec MPI est trop difficile pour la majorité des chercheurs qui ne sont pas experts en programmation. Le modèle BSP propose une approche bien plus simple à la parallélisation. A l'exemple d'une bibliothèque BSP pour le langage Python, je montrerai comment BSP peut aider un physicien à résoudre ses problèmes numériques en parallèle.
- 2 février 2009
- Olivier Heen
(IRISA)
- Vérification de protocoles cryptographiques
- Résumé :
Ce cours de trois heures donne une idée de certaines méthodes de construction et de vérification des protocoles cryptographiques.
Nous faisons tout d'abord quelques rappels d'ingénierie des protocoles et de cryptographie. Nous introduisons en particulier une notation simplifiée pour les opérations cryptographiques, et nous donnons une description de « l'intrus réseau ».
Dans une deuxième partie nous étudions des exemples de protocoles pour l'échange de secret et l'échange de clés. Nous montrons comment des attaques contre ces protocoles peuvent être trouvées et exprimées.
La dernière partie est consacrée à la vérification proprement dite : vérification « à la main » puis vérification automatisée de certaines propriétés. Nous montrons le fonctionnement de deux outils de vérification et donnons une idée de la théorie sous jacente.
Ce cours ne nécessite aucun pré-requis.
- 9 février 2009
- Florian Kammüller
(TU Berlin)
- ASPfun: Un Calcul des Objets Actifs pour la Sécurité
- Résumé :
La programmation d'un grand réseau d' ordinateurs distribués,
tel que l'Internet, pose de nouveaux problèmes de sécurité.
Je présente dans cet exposé le langage formel ASPfun pour les
objets distribués asynchrones. ASPfun élargit la théorie des objets par une communication requêtes-réponse basée sur des futurs. Un futur représente le résultat encore attendu d'une requêtes donnée; la réponse exprime le résultat d'une requêtes à l'objet qui contient le futur.
Ma présentation introduit le calcul ASPfun et sa sémantique.
Je résume nos résultats sur les systèmes de typage et la
sûreté des types d'ASPfun. Finalement, j'illustre nos idées sur la sécurité par un exemple.
ASPfun et toutes ses propriétés sont entiérement formalisées est demontrées avec l'assistant de preuve Isabelle/HOL.
- 2 mars 2009
- David Michel
(LACL)
- Logiques pédagogiques propositionnelles
- Résumé :
Il est fréquent dans l'enseignement des mathématiques d'illustrer
les définitions d'objets à l'aide d'exemples les motivant, dans le
but de faciliter la compréhensions de notions parfois très abstraites.
Les logiques pédagogiques sont des systèmes de déduction naturelle
formalisant l'utilisation systématique de définitions motivées par des
exemples. Elles sont par essence exemptes de négation. Lors de cet exposé
seront présentées différentes logiques pédagogiques propositionnelles
ainsi que leurs liens avec les lambda-calculs typés, dans lesquels
l'absence de négation au niveau des types garantit que toute fonction
typable satisfait la propriété dite d'utilité: une fonction est utile
quand elle peut être appliquée à un argument.
- 16 mars 2009
- Radu Calinescu
()
- Online quantitative verification: capabilities and challenges
- Résumé :
Quantitative verification represents a formal technique for the modelling and analysis of systems that exhibit probabilistic or real-time behaviour. Boosted by the development of effective model checking algorithms and tools, the quantitative verification of real-world systems has become increasingly popular in recent years. This talk explores the benefits and limitations of extending quantitative verification to the online configuration of adaptive IT systems. I will present a framework for the development of self-managing systems whose components can be modelled as Markov chains, and describe how the systems developed within this framework use online quantitative analysis to dynamically adjust their parameters in line with their state, environment and objectives. The challenges associated with this approach and possible ways to overcome them will be discussed during the presentation.
- 23 mars 2009
- Jean-Baptiste Yunès
(LIAFA)
- Calculs sur automates cellulaires
- Résumé :
Nous montrerons comment l'étude de calculs sur lignes d'automates conduit naturellement au concept de grilles d'automates et que celles-ci se révèlent être de bien pratiques supports permettant de concevoir une implémentation de schémas de calculs basée sur des automates cellulaires. Ceci conduisant, nous pensons, à une implémentation parallèle de programmes séquentiels.
- 11 mai 2009
- Dimitar P. Guelev (Institute of Mathematics and Informatics)
- A Course of Temporal Logic for B.Sc and M.Sc. Students at Sofia
- Résumé :
This talk is about a course of temporal logic which I compiled for students of mathematics and computer science at the Faculty of Mathematics and Informatics at Sofia University. The talk will cover the systems of TL and the main results about them which are included in the course, some detail on the proof techniques for those results which were chosen in order to enable a self-contained and proof-complete presentation, and the relation with other elective courses for students who specialise in theoretical computer science at Sofia.
- 18 mai 2009
- Mark Ryan (Université de Birmingham)
- Attacks on the Trusted Platform Module, and solutions
- Résumé :
The Trusted Platform Module (TPM) is a hardware chip designed to enable computers achieve greater security. Proof of possession of values known as authData is required by user processes in order to use TPM keys. We demonstrate two attacks relating to the way authData is handled, and explain their consequences. By using the attacks, an attacker can circumvent some crucial operations of the TPM, and impersonate a TPM user to the TPM, or impersonate the TPM to its user. We describe modifications to the TPM protocols that avoid these attacks, and use protocol verification techniques to prove their security.
- 25 mai 2009
- 15 juin 2009
- 22 juin 2009
- Catalin Dima (LACL)
- Model checking epistemic extensions of CTL
- Résumé :
We show that CTL with knowledge modalities has an undecidable satisfiability problem, but decidable model-checking. We then show that, over continuous time, model-checking is undecidable, and becomes decidable only if the agents are able to fully observe clock values. We also give some ideas of the utility of CTL with knowledge operators in the verification of security properties.
