Date: October 20
Place: A008
Chairs: Emmanuel Jeandel
Session 1 : 9h-10h
Eric Le Morvan
Secure refinements of communication channels
It is a common practice when designing security protocols to assume that they already unspecified secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. However the protocol designer needs to be sure that any standard implementation will work properly without interfering with the core protocol. In this presentation, formal definition of authentified and secure channels are provided along with conditions under which this component-based approach is secure.
Quantitative experiments on real-life protocols like e-passport protocol or TLS will also be presented.
Hubert Godfroy
A taste of soft-linear logic for staged computation
The goal of this work is to study at high level relations between executable codes (programs) codes and readable/writeable codes (data). In low level languages like assembly, programs are not different form data, and what is called program is the set of codes executed during
the run. In higher level languages, like in C/C++, programs (C code) are mostly disjoint from data (string for instance), but it is still possible to do self-modification with function pointers. Interpreted languages like Python make it easy to execute data with instruction exec which takes strings and executes it.
Logical framework have been developed to study this phenomenon. Temporal logic use “next” operator to specify that a statement is true for the next stage. Programmatically, the stage of each term is clearly given. In this framework, it is easy determine when a piece of code will be evaluated.
On the other hand, Modal logic can be used to describe closed values which remains to be evaluated. In this framework data codes are syntactically identified: each term of the form <t> : \square A is in normal form and then is seen as a data.
In this talk we want to understand more precisely what is responsible (in term of logic) of phenomenons of self-modification like reading/writing mechanism, data execution, program freezing… Tools come form linear logic world, especially from its “soft” part. We will see interpretations of common operations like dereliction, digging…
10h30 – 14h : Soutenance de thèse de Bruno Andriamiarina
Développement d’algorithmes répartis corrects par construction
Pause café : 10h – 10h30
Session 2 : 14h-16h
Huu-Hiep Nguyen
Graph Release and Community Detection under Differential Privacy
The first part of our talk is about the problem of private publication of graph structure. The prevalence of differential privacy makes the problem more promising. However, a large body of existing works on differentially private release of graphs have not answered the question about the upper bounds of privacy budgets. In this paper, for the first time, such a bound is provided. We prove that with a privacy budget of $O(\log n)$, there exists an algorithm capable of releasing a noisy output graph with edge edit distance of $O(1)$ against the true graph. At the same time, the complexity of our algorithm Top-m Filter is linear in the number of edges $m$. This lifts the barriers of the state-of-the-art, which incur a complexity of $O(n^2)$ where $n$ is the number of nodes and runnable only on graphs having $n$ of tens of thousands. In the second part, we consider the problem of community detection under differential privacy. Complex networks usually expose community structure with groups of nodes sharing many links with the other nodes in the same group and relatively few with nodes of the rest. This feature captures valuable information about the organization and even the revolution of the network. Over the last decade, a great number of algorithms for community detection are proposed to deal with the increasingly complex networks. However, the problem of doing this in a private manner is rarely considered. In this paper, we give a big picture on differential private community detection via two categories of input and algorithm perturbations. We analyze the major challenges behind the problem and propose several schemes to tackle them. We have thoroughly evaluated our techniques on large real graphs.
Imen Sayar
Articulation between formal and semi-formal activities in the development of software
My PhD thesis is situated in the context of formal development of software and complex systems. Our aim in this PhD is to define interactions that can exist between two different worlds: formal and semi-formal worlds. The former is represented by formal methods as B and Event-B and the later is represented by clients and their requirements.
We localize our goal under two levels :
– The first one consists on validation of formal Event-B models under
development according to the informal requirements document.
– The second level is about the integration of parts formally
developed into a semi-formal development process.
We are processing with a case study of a Landing Gear System for studying the first level. To do that, we are using many tools for different activities namely : ProR for restructuring requirements document, provers in the Rodin plateform for verification, ProB and JeB for validation.
Noran Azmy
Formal Verification of Pastry Using TLA+
I will talk about my work verifying the peer-to-peer protocol Pastry using TLA+, a specification and proof language for the verification of concurrent systems. In his PhD thesis, Tianxiang Lu discovered correctness problems for Pastry and also developed a model (called LuPastry) for which he provided a partial proof of correct delivery assuming no abrupt node departures, mechanized in the TLA + Proof System. I am working on a revised proof of correct delivery for LuPastry that improves upon Lu’s work in the following respects. Firstly, I reformulated parts of the model in such a way that the reasoning complexity is confined to a small part of the proof, greatly simplifying the proof. Secondly, I refined the specification of LuPastry for a number of border cases. Finally, Lu’s proof was based on many assumptions that were not proved, partly due to the sheer size of the proof. I removed almost all of these assumptions by reformulating them as facts that I proved for the refined model.
Ludovic Robin
Automated verification of protocols using low-entropy secrets
In E-commerce protocols, such as the well known 3D-Secure protocol, there is an additional check of client authenticity using mobile phones. Confirmation codes emitted on these channels are short due to human interaction and this could benefit to an attacker that may break the security through brute-force attack. In this talk we will present new attacker models that take into account these brute-force abilities and discuss their automated verification.
Pause café : 16h – 16h30
Session 3 : 16h30 – 17h50
Souad Kherroubi
A framework to formally handle domain knowledge in system design
Pierre Kimmel
A Temporal Extension for BI
BI logic is an extension of intuitionnistic logic with multiplicative operators that allows the expression of separation and sharing of ressources, in the fashion of Linear Logic. BI has already been extended with modal operators, but we focused on the special case of temporal extension. By taking inspiration from LTL (linear temporal logic), we added temporal operators to BI, which gave birth to 2 different tableaux methods and several interesting possible uses, such as a new way to handle branching time logics.
Alicia Filipiak
Conception et validation de services de sécurité pour les plateformes mobiles.
