Date: Friday, September 21
Place: A008
Chair: Dominique Méry
- 9h00-9h15: Coffee
- 9h15-9h30: Opening by Dominique Méry
- 9h30-11h00 : Session 1
- Cyrille Wiedling : Vérification Formelle de Protocoles : Vote Electronique et API de SécuritéCryptographic protocols are widely used around the world, often in our everyday life such as cash machines, secured navigation on internet, etc. But also in E-voting and security APIs. If E-voting allows people to vote from everywhere, it must also protect, as the paper vote, their privacy. In a context where an intruder may have a real strong power over a network, it is crucial to analyse security properties of E-voting protocols. Security APIs are interfaces used between host machines (e.g a computer) and trusted devices (e.g a smartcard). They ensure communication between the two without leaking any information about what is stored on the trusted device and should remain secret. As E-voting protocols, a security API must be analysed to ensure its efficiency. For this thesis, we study both of them using formal methods, analysing them in an abstract way in order to describe their security properties.
- Guillaume Scerri: Preuves de sécurité symboliques et computationelles pour les protocoles cryptographiques
- Faqing YANG: Using Simulation to Validate Event-B SpecificationsThis presentation addresses the validation of formal specifications in Event-B. This activity is best done through the execution of the specification and the observation of its behavior. Current tools for Event-B, animators and translators, provide users with automatic execution mechanisms of the models, but their use is hard on early, non-deterministic and abstract refinements. We propose a third technique, simulation, in which users and tools co-operate to produce an executable instance of the model.
- 11h00-11h15 : Pause
- 11h15-12h45 : Session 2
- Manamiary Bruno Andriamiarina : Revisiting Snapshot Algorithms by Refinement-based TechniquesThe snapshot problem addresses a collection of important algorithmic issues related to the distributed com- putations, which are used for debugging or recovering the distributed programs. Among the existing solutions, Chandy and Lamport propose a simple distributed algorithm. In this paper, we explore the correct-by-construction process to formalize the snapshot algorithms in distributed system. The formalization process is based on a modeling language Event B, which supports a refinement-based incremental development using RODIN platform. These refinement-based techniques help to derive a correct distributed algorithm. Moreover, we demonstrate how this class of other distributed algorithms can be revisited. A consequence is to provide a fully mechanized proof of the distributed algorithms.
- Henri Debrat: Vérification d’algorithmes répartis tolérants aux pannes dans le modèle Heard-OfConsensus is the paradigmatic problem in fault-tolerant distributed computing: it requires network nodes that communicate by message passing to agree on common value even in the presence of (benign or malicious) faults. Several algorithms for solving Consensus exist, but few of them have been rigorously verified, much less so formally. The Heard-Of model proposes a simple, unifying framework for defining distributed algorithms in the presence of communication faults. Algorithms proceed in communication-closed rounds, and assumptions on the faults tolerated by the algorithm are stated abstractly in the form of communication predicates. Extending previous work on the case of benign faults, our approach relies on the fact that properties such as Consensus can be verified over a coarse-grained, round-based representation of executions. We have encoded the Heard-Of model in the interactive proof assistant Isabelle/HOL and have used this encoding to formally verify three Consensus algorithms based on synchronous and asynchronous assumptions. Our proofs give some new insights into the correctness of the algorithms, in particular with respect to transient faults.
- Hernán Vanzetto: Automatic verification of TLA+ proof obligations with SMT solvers
- 12h45-14h00 : Lunch
- 14h00-15h30 : Session 3
- Bao Hoang: On the Polling Problem for Social Networks
- Jean-Christophe Bach: Transformation de modèles et certificationL’IDM est de plus en plus utilisée dans un contexte industriel pour le développement logiciel : d’un modèle établi par un expert, logiciel(s), documentation, et tests doivent être écrits pour respecter le modèle ou la spécification. Cela a pour conséquence une adaptation et évolution des chaînes de développement, en particulier l’utilisation d’outils de génération automatique de code. Le développement de systèmes critiques (e.g.: en aéronautique) n’échappe pas à cette tendance, ce qui soulève le problème de la fiabilité du logiciel. Outre la chaîne de développement classique qui évolue, le processus de vérification du logiciel doit lui aussi être adapté.Nous nous proposons donc, dans le cadre du projet Quarteft (http://quarteft.loria.fr) financé par la FNRAE (Fondation de la Recherche pour l’Aéronautique et l’Espace, http://www.fnrae.org/), de fournir un langage dédié (DSL) de transformation de modèles afin de faciliter l’écriture de transformations qualifiables (transformation garantissant la conservation des propriétés d’intérêt). Nous appliquons ensuite ce langage au cas d’étude fourni par Airbus qui consiste à passer d’un langage métier (AADL) à un langage utilisable par un modèle checker comme TINA ou CADP (réseaux de Petri temporisés). Notre langage de transformation doit permettre de passer d’une étape à l’autre de la chaîne de développement, tout en s’intégrant parfaitement dans dans les environnements de développement pré-existant.Ce langage s’appuie sur le langage Tom développé dans l’équipe Pareo (ex Prothéo) depuis 2000. Tom est un langage basé sur le calcul de réécriture et conçu pour étendre les langages généralistes (Java, C, Python, Caml, C#, etc.). Il permet d’ajouter des fonctionnalités intéressantes telles que le filtrage de motif ou la programmation par stratégies. Il a l’avantage de tirer partie à la fois du monde des DSL (constructions dédiées à des tâches spécifiques), et à la fois de celui des langages généralistes (outillage externe fortement développé, nombreuses bibliothèques, large communauté de développeurs, bonne intégration au cadre industriel) ; tout en s’appuyant sur des bases formelles solides.
- Hugo Férée: Complexité d’ordre supérieur
- 15h30-15h45 : Pause
- 15h45-17 h 15 : Session 4
- Thanh Dinh Ta : Algebraically modeling and verifying malwares
- Aurélien Thierry: Analyse de programmes malveillants par comparaison de graphes
- Jean-René Courtault : Ressources dynamiques : modèles et preuvesUn défi majeur pour appréhender les problèmes posés par la complexité des systèmes actuels est de proposer de nouveaux cadres formels et de nouvelles méthodes d’analyse et de conception, qui intègrent dès l’origine les liens et interactions qui existent entre les aspects statiques et dynamiques d’un système. La notion de ressource et les problématiques liées à leur gestion sont au coeur de notre approche. Nous entendons ici par ressources aussi bien des entités physiques que des entités abstraites. On s’intéresse plus particulièrement à des phénomènes de production/consommation (jetons dans un réseau de Pétri), de partage/séparation (zones de mémoire dans un ordinateur). Partant des logiques de séparation, notamment de la logique BI se focalisant sur le partage et la séparation de ressources et de la logique MBI capturant la manipulation de ressources par des processus, notre étude porte sur des extensions modales de ces logiques en vue de capturer des aspects dynamiques des ressources, avec la proposition de nouvelles logiques, de sémantiques adaptées et de systèmes de preuves adaptés à la vérification et à la preuve de propriétés.
- 17 h 15 : Closing Session
