- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
Les séminaires du LIFO
Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021
Sauf exception, les séminaires se déroulent le lundi de 14h à 15h, Salle de réunion 1, bâtiment IIIA (voir plan du campus).
14/10/2021 : [Séminaire SDS] E-voting protocols - how to analyse the security of these (real-world) systems?
Alexandre Debant (Inria Nancy)
Résumé
Attention : Les informations de connexion sont disponibles dans le canal Séminaires du groupe Teams / Débute à 13 h 40. Lieu : Zoom
23/09/2021 : [Séminaire SDS] Sécurité des dispositifs médicaux connectés : une première étude des communications sans fil
Matthieu Bannwarth ()
Résumé
Attention : Les informations de connexion sont disponibles dans le canal Séminaires du groupe Teams / Débute à 13 h 40. Lieu : Zoom
13/09/2021 : Abundant Extensions
Henning Fernau (Université de Trèves, Allemagne)
Résumé
17/05/2021 : L'Inclusion-Exclusion pour l'ordonnancement
Olivier Ploton (Université de Tours, LIFAT)
Résumé
Attention : Lieu : En ligne
22/03/2021 : Algorithmes distribués pour la détection de sous-graphes
Ioan Todinca (Université d'Orléans, LIFO)
Résumé
Attention : Lieu : En ligne
15/03/2021 : Specification and Verification of High-Level Properties with MetAcsl
Nikolai Kosmatov (Thales Research & Technology (TRT))
Résumé
Attention : Lieu : En ligne
08/03/2021 : Online Testing of Dynamic Reconfigurations w.r.t. Adaptation Policies
Frédéric Dadeau & Olga Kouchnarenko (Univ. Bourgogne Franche-Comté, CNRS, FEMTO-ST Institute)
Résumé
Attention : Lieu : En ligne
22/02/2021 : Learning Sparse Penalties for Change-point Detection using Max Margin Interval Regression
Toby Hocking (Northern Arizona University)
Résumé
Attention : Débute à 16 h 05. Lieu : En ligne
15/02/2021 : Systèmes auto-adaptatifs: introduction et modélisation formelle par des systèmes de réécriture de graphe
Cédric Eichler (INSA Centre Val de Loire, LIFO)
Résumé
Attention : Lieu : En ligne
08/02/2021 : A calculus of Branching Processes
Jean Krivine (IRIF)
Résumé
Attention : Lieu :
01/02/2021 : Categorifying Non-Idempotent Intersection Types
Federico Olimpieri (LIPN)
Résumé
Attention : Lieu : En ligne
18/01/2021 : Toward Safe and Efficient Reconfiguration with Concerto
Simon Robillard et Hélène Coullon (IMT Atlantique)
Résumé
Attention : Débute à 13 h 45. Lieu : En ligne
Résumés des séminaires
[Séminaire SDS] E-voting protocols - how to analyse the security of these (real-world) systems? Alexandre Debant, Inria Nancy
For many years, e-voting protocols have been designed and formal methods (computational or symbolic) have been developed to prove the main properties that such systems must satisfy, e.g. vote secrecy and verifiability. Based on these security proofs, e-voting systems are now used (or ready to be) in our daily life for association elections, company elections, or even political elections (e.g. in Switzerland, Estonia, Australia…).
In this talk I will first introduce the topic of e-voting and how symbolic models can be used to provide security proofs. Then, I will discuss the accuracy of the models with respect to the real-world constraints that arise when these protocols are deployed in practice. To this aim, I will present new attacks we discovered. Finally, I will talk about some properties (e.g. cast-as-intended, accountability) which are at the limit of the state-of-the-art in symbolic analysis.
[Séminaire SDS] Sécurité des dispositifs médicaux connectés : une première étude des communications sans fil Matthieu Bannwarth,
Durant son stage, Mathieu a mis en place une plateforme de pentesting sans fil (RF) dans le but d'étudier certains aspects sécuritaires des communications non filaires des implants médicaux connectés (IOMT). Cette plateforme a vocation à identifier/reproduire des vulnérabilités existantes/nouvelles.
Après une rapide revue de littérature des vulnérabilités déjà connues sur certains implants, potentiellement capable de faire courir un risque médical ou pour les données personnelles du patient, Mathieu présentera les premières analyses et résultats qu'il a pu obtenir. Après une prise en main de la plateforme sur du matériel IOT non médical, Mathieu a pu entreprendre des tests sur un implant médical donné. Mathieu présentera les premiers résultats obtenus, et les limites de diverses natures qui ont freiné l'avancée des travaux.
Mots clés : Pentesting, RF (Radio Fréquence), Objets connectés, Implants, Médical, Données personnelles, Vulnérabilités, Failles de sécurité.
Abundant Extensions Henning Fernau, Université de Trèves, Allemagne
Most algorithmic techniques dealing with constructing solutions to combinatorial problems build solutions in an incremental fashion.
Often, the whole procedure could be visualized by means of a search tree.
To the leaves of such a search tree, we can associate solutions, while to the inner nodes, only pre-solutions can be associated.
By looking at all leaves of the search tree, an optimum solution can be found if desired.
In particular for reasons of speed, it is crucial to prune off potential branches of the search tree by deciding at an early stage if a certain pre-solution
can be ever extended to a solution that is optimal. But, how easy is it to tell if such pruning is possible?
In this survey, we first present a motivating example as an introduction, followed by a general framework for extension problems. Then we show that such problems are really abundant, and these examples also prove that the complexity of these extension problems can be the same as or different from that of the original combinatorial question.
L'Inclusion-Exclusion pour l'ordonnancement Olivier Ploton, Université de Tours, LIFAT
Cette présentation est consacrée à l'application de l'Inclusion-Exclusion aux problèmes d'ordonnancement NP-difficiles. Ce sont des problèmes d'optimisation dans lesquels on alloue dans le temps des ressources à des travaux, sous contraintes et en minimisant un critère. L'Inclusion-Exclusion est une technique combinatoire permettant de dénombrer les solutions d'un problème sans les énumérer explicitement. On peut l'utiliser pour compter le nombre de solutions du problème de décision associé à tout problème d'optimisation, et en déduire un algorithme exact pour résoudre le problème d'optimisation avec une complexité pire cas modérément exponentielle en temps et pseudo-polynomiale en espace. Dans cette présentation, nous passons en revue l'Inclusion-Exclusion et certaines de ses extensions, et nous montrons comment l'appliquer pour concevoir des algorithmes exponentiels de pointe en matière d'ordonnancement.
Mots-clefs: Ordonnancement; Algorithmes exponentiels; Inclusion-Exclusion.
Algorithmes distribués pour la détection de sous-graphes Ioan Todinca, Université d'Orléans, LIFO
Basé principalement sur des travaux réalisés avec Pierre Fraigniaud (IRIF, CNRS/Univ de Paris), Pedro Montealegre (Univ. Adolfo Ibañez, Santiago, Chili), Denis Olivetti (Univ. Freiburg) et Ivan Rapaport (Universidad de Chile), présentés à DISC 2017 (International Symposium on Distributed Computing).
Un cadre classique pour le calcul distribué est le modèle LOCAL, formé d’un réseau de noeuds ayant chacun un identifiant unique et possédant ses propres données. La communication se fait de façon synchrone, lors d'une ronde de communication chaque noeud échange des messages avec ses voisins. Nous nous intéressons particulièrement au modèle CONGEST, ayant une faible bande passante : la taille des messages est d’ordre logarithmique par rapport au nombre de noeuds du réseau. L’objectif est de résoudre un problème -- par exemple de vérifier une propriété du réseau -- en un faible nombre de rondes, si possible en temps constant.
Je commencerai par une introduction au modèle CONGEST, avec ses possibilités et ses limites. Nous verrons qu’il est difficile de vérifier certaines propriétés pourtant très locales, comme la détection d’un cycle à quatre sommets, et ce même avec des protocoles probabilistes.
En revanche nous verrons qu’il est possible de vérifier en un nombre constant de rondes si le réseau possède comme sous-graphe un arbre donné. Je présenterai en détails le protocole probabiliste pour la détection d’un chemin de longueur k, étonnamment simple. J’évoquerai ensuite la façon de l’étendre à un arbre, de le rendre déterministe, et quelques autres conséquences. A travers cet exemple je m’efforcerai d’illustrer certaines problématiques et outils du calcul distribué.
Specification and Verification of High-Level Properties with MetAcsl Nikolai Kosmatov, Thales Research & Technology (TRT)
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult
to assess them. To address this issue, we propose a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in several case studies. This talk gives an overview of various contributions related to MetAcsl.
The corresponding results were published at TACAS 2019, TAP 2019 and FormaliSE 2021 (to appear). This work is a joint work with Virgile Robles, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies. Adaptation policies are seen as artifacts that describe desirable behavior of the system without enforcing a specific one. An adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their respective utility. The adaptation policy has to be faithfully implemented by the system, especially w.r.t. the priority occurring in the rules, which are generally specified for optimizing some extra-functional properties (e.g. minimizing resource consumption).
In this context, this presentation will present a model-based testing approach which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. In the end, the relative frequencies of the reconfigurations are measured in order to determine if the adaptation policy is faithfully implemented. We will illustrate our approach by simulations for a platoon of autonomous vehicles.
Joint work by Frédéric Dadeau, Jean-Philippe Gros and Olga Kouchnarenko
Learning Sparse Penalties for Change-point Detection using Max Margin Interval Regression Toby Hocking, Northern Arizona University
In segmentation models, the number of change-points is typically chosen using a penalized cost function. In this work, we propose to learn the penalty and its constants in databases of signals with weak change-point annotations. We propose a convex relaxation for the resulting interval regression problem, and solve it using accelerated proximal gradient methods. We show that this method achieves state-of-the-art change-point detection in a database of annotated DNA copy number profiles from neuroblastoma tumors.
The paper.
Systèmes auto-adaptatifs: introduction et modélisation formelle par des systèmes de réécriture de graphe Cédric Eichler, INSA Centre Val de Loire, LIFO
Les systèmes distribués modernes évoluent dans des contextes soumis à évolutions auxquelles ils doivent s'adapter. Ils doivent ainsi faire face à l'arrivée ou au départ de composants, aux pannes, aux évolutions des besoins... L'informatique autonome fournit un cadre pour la délégation de la gestion de ces (auto-)adaptations au système lui-même, limitant ou éliminant les interventions humaines.
Ce séminaire introductif présentera dans un premier temps l'informatique autonome, son inception, ses objectifs, sa mise en œuvre au travers de la boucle de contrôle MAPE-K, ainsi que quelques unes des problématiques qui lui sont associées.
Dans un second temps, nous présenterons une approche de modélisation formelle de systèmes auto-adaptatifs basée sur la réécriture de graphe. Cette approche permet de représenter l'état d'un système, ses états acceptables et ses adaptations. Finalement, nous verrons comment cette approche permet de spécifier des adaptations préservant nécessairement la correction d'un système.
A calculus of Branching Processes Jean Krivine, IRIF
(joint work with Thomas Ehrhard (CNRS, IRIF) and Ying Jiang (ISCAS, China)
CCS-like calculi can be viewed as an extension of classical automata with communication primitives. In this talk I will show what we obtained when we applied this principle to tree-automata: a calculus of branching processes (termed CBP), where the continuations of communications are allowed to branch according to the arity of the communication channel. I will show that CBP can be “implemented” by a fully compositional LTS semantics. I will argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology à la CCS and calculi with dynamic connectivity such as the π-calculus.
Reference: A Calculus of Branching Processes. Ehrhard, Krivine and Jiang. TCS 807(6) pp 169–184.
Categorifying Non-Idempotent Intersection Types Federico Olimpieri, LIPN
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
Toward Safe and Efficient Reconfiguration with Concerto Simon Robillard et Hélène Coullon, IMT Atlantique
For large-scale distributed systems that need to adapt to a changing environment, conducting a reconfiguration is a challenging task. In particular, efficient reconfigurations require the coordination of multiple tasks with complex dependencies. We present Concerto, a model used to manage the lifecycle of software components and coordinate their reconfiguration operations. Concerto promotes efficiency with a fine-grained representation of dependencies and parallel execution of reconfiguration actions, both within components and between them. In this paper, the elements of the model are described as well as their formal semantics. In addition, we outline a performance model that can be used to estimate the time required by reconfigurations, and we describe an implementation of the model. The evaluation demonstrates the accuracy of the performance estimations, and illustrates the performance gains provided by the execution model of Concerto compared to state-of-the-art systems.
Keywords: reconfiguration, component-based models, coordination, parallelism, distributed software
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 