The PhD Day of the Department Formal Methods at LORIA#

Tuesday, October 14, Room B013#

Chair: Emmanuel Jeandel


Hubert Godfroy (Carte) - Self Modifying Machines

We describe a new framework for self-modifying programs. Our goal is to show how to extract program abstraction focusing on self-modifications. On the first hand, we use a abstract machine which makes explicit some typical behavior, such as turning data into executable code and vice versa. Moreover memory is also separated between data (what we can read and write) and code (what we can execute). On the other hand, we add another level of granularity in memory location, in order to build a more static program abstraction.


Hiep Nguyen Huu (Cassis) - Anonymizing Social Graphs via Uncertainty Semantics

Rather than anonymizing social graphs by generalizing them to super nodes/edges or adding/removing nodes and edges to satisfy given privacy parameters, recent methods exploit the semantics of uncertain graphs to achieve privacy protection of participating entities and their relationship. These techniques anonymize a deterministic graph by converting it into an uncertain form. In this paper, we propose a generalized obfuscation model based on uncertain adjacency matrices that keep expected node degrees equal to those in the unanonymized graph. We analyze two recently proposed schemes and show their fitting into the model. We also point out disadvantages in each method and present several elegant techniques to fill the gap between them. Finally, to support fair comparisons, we develop a new tradeoff quantifying framework by leveraging the concept of incorrectness in location privacy research. Experiments on large social graphs demonstrate the effectiveness of our schemes.


Éric Le-Morvan (Cassis) - Composition sûre de protocoles cryptographiques

La vérification de protocoles cryptographiques est essentielle à la sécurisation des communications effectuées sur un réseau public. En effet si la cryptographie est la brique de base utilisée pour empêcher un attaquant de lire des messages qui ne lui sont pas destinés, il est nécessaire de s'assurer que la cryptographie est bien utilisée. Cependant il est difficile algorithmiquement de garantir l'absence de faille logique dans un protocole. La tâche s'avère de plus impraticable lorsque l'on cherche à vérifier ensemble plusieurs protocoles à plus forte raison s'ils partagent des données, or ce cas est très fréquent (différentes versions d'un protocole, protocole utilisé comme sous routine d'un autre protocole). Le but de mes travaux est d'établir un critère syntaxique simple à vérifier dès le stade de la conception et qui garantisse que l'on peut étudier des protocoles séparément sans risquer d'interférences lorsqu'on les utilisera conjointement. Le critère étudié est principalement l'adjonction de tags dans chaque fonction cryptographique qui indique le protocole utilisé. Sous cette hypothèse et d'autres relevant des bonnes pratiques de conception on montre l'absence d'interférence vis-à-vis de la préservation du secret.

15h-16h Goûter

Tuesday, October 22, Room A008#

Chair: Michael Rusinowitch


Jean-Christophe Bach (Pareo) - Langage et outil pour la transformation de modèles


Houari Mahfoud (Cassis) - Secure and Valid Manipulation of XML Data

It is increasingly common to find XML views used to enforce access control as found in many applications and commercial database systems. To overcome the overhead of view materialization and maintenance, XML views are necessarily virtual. With this comes the need for answering XML queries posed over virtual views, by rewriting them into equivalent queries on the underlying documents. A major concern here is that query rewriting for recursive XML views is still an open problem, and proposed approaches deal only with non-recursive XML views. Moreover, a small number of works have studied the access rights for updates. In this talk, we present SVMAX (Secure and Valid MAnipulation of XML), the first system that supports specification and enforcement of both read and update access policies over arbitrary XML views (recursive or non). SVMAX defines general and expressive models for controlling access to XML data using significant class of XPath queries and in the presence of the update primitives of W3C XQuery Update Facility. Furthermore, SVMAX features an additional module enabling efficient validation of XML documents after primitive updates of XQuery. The wide use of W3C standards makes of SVMAX a useful system that can be easily integrated within commercial database systems as we will show. We give extensive experimental results, based on real-life DTDs, that show the efficiency and scalability of our system.

10h30-11h Pause café


Hugo Férée (Carte) - Analyse récursive et complexité

En analyse récursive, les objets mathématiques (typiquement les nombres ou les fonctions réels) sont représentés par des objets symboliques (les entiers ou les suites d'entiers), ce qui permet d'exporter les notions de calculabilité et de complexité du discret au continu. Nous verrons dans cet exposé des exemples de l'influence de la complexité sur les propriétés analytiques des objets représentés.


Hernán Vanzetto (Veridis/Mosel) - Type Reconstruction for Set Theory

12h-14h Lunch

Chair: Emmanuel Jeandel


Hoang Bao-Thien (Cassis) - On Constrained Adding Friends in Social Networks

Online social networks are currently experiencing a peak and they resemble real platforms of social conversion and content delivery. Indeed, they are exploited in many ways: from conducting public opinion polls about any political issue to planning big social events for a large public. To securely perform these large-scale computations, current protocols use a simple secret sharing scheme which enables users to obfuscate their inputs. However, these protocols require a minimum number of friends, i.e. the minimum degree of the social graph should be not smaller than a given threshold. Often this condition is not satisfied by all social graphs. Yet we can reuse these graphs after some structural modifications consisting in adding new friendship relations. In this paper, we provide the first definition and theoretical analysis of the adding friends problem. We formally describe this problem that, given a graph G and parameter c, asks for the graph satisfying the threshold c that results from G with the minimum of edge-addition operations. We present algorithms for solving this problem in centralized social networks. An experimental evaluation on real-world social graphs demonstrates that our protocols are accurate and inside the theoretical bounds.

Manamiary Andriamiarina (Veridis/Mosel) - Formal Analysis of Distributed Algorithms using Refinement


Jean-René Courtault (Types) - Dynamic resources: models and proofs

15h30-16h Pause café


Thanh Dinh Ta (Cassis) - Efficient Program Exploration by Input Fuzzing


Cyrille Wiedling (Cassis) - Design & Analysis of a Revocation API

Embedded systems deployed in hostile environments often employ some dedicated tamper-resistant secure hardware to handle cryptographic operations and keep keys secure. Examples include mobile phones (SIM cards), smart utility meters (smartcard-like chip for cryptography), on-vehicle cryptographic devices to support vehicle-to-vehicle networking et cetera. Connexion with the secure hardware is made through a security API that is an Application Program Interface allowing untrusted code to access sensitive resources in a secure way. I presented an API for symmetric key management that supports revocation, a functionnality that has been relatively few adressed, and prove security properties design in the symbolic model of cryptography. I am now implementing this device to test its performance on real smartcards and also trying to improve the revocation method to ensure even better security properties, especially in terms of usability. In the last part of my talk, I also will briefly survey the last results obtained in e-voting and more precisely on the Norwegian e-voting protocol.

Friday, September 21#

Room A008#

PhD Students of the Department Formal Methods will give a talk on their ongoing works. The programme is starting at 9H00 and is organised as follows:

  • 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é

Abstract :

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 Specifications`
Abstract :

This 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 Techniques


The 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-Of


Consensus 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 certification

L'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 ( financé par la FNRAE (Fondation de la Recherche pour l'Aéronautique et l'Espace,, 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 preuves

Abstract : Un 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

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-43) was last changed on 14-oct.-2014 14:50 by cortier