!!The PhD Day of the Department Formal Methods  at LORIA


!Tuesday, October 14, Room B013
''Chair: Emmanuel Jeandel''

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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.

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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.

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
É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''

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
Jean-Christophe Bach (Pareo) - __Langage et outil pour la transformation de modèles__

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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é__

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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.

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
Hernán Vanzetto (Veridis/Mosel) - __Type Reconstruction for Set Theory__

__12h-14h Lunch__

''Chair: Emmanuel Jeandel''

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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.

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
Manamiary Andriamiarina (Veridis/Mosel) - __Formal Analysis of Distributed Algorithms using Refinement__

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
Jean-René Courtault (Types) - __Dynamic resources: models and proofs__

__15h30-16h Pause café__

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
Thanh Dinh Ta (Cassis) - __Efficient Program Exploration by Input Fuzzing__

%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
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


!Friday, September 21
%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
!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
(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 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