Date: Tuesday, October 22
Place: A008
Chair: Michael Rusinowitch (morning) & Emmanuel Jeandel (afternoon)
9h30-10h : Jean-Christophe Bach (Pareo)
Langage et outil pour la transformation de modèles
10h-10h30 : 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é
11h-11h30 : 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.
11h30-12h : Hernán Vanzetto (Veridis/Mosel)
Type Reconstruction for Set Theory
12h-14h : Lunch
14h-14h30 : 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.
14h30-15h : Manamiary Andriamiarina (Veridis/Mosel)
Formal Analysis of Distributed Algorithms using Refinement
15h-15h30 : Jean-René Courtault (Types)
Dynamic resources: models and proofs
15h30-16h : Pause café
16h-16h30 : Thanh Dinh Ta (Cassis)
Efficient Program Exploration by Input Fuzzing
16h30-17h : 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.
