format des présentations : 30mn

14h00 - 14h30 : Ludovic Henrio
Equipe Projet Oasis - INRIA Sophia Antipolis
"Functional Active Objects: Typing and Formalisation"

ASPfun provides a sound foundation for autonomous objects communicating by remote method invocations and futures. As a distributed extension of sigma-calculus, we define ASPfun, a calculus of functional objects, behaving autonomously and communicating by a request-reply mechanism: requests are method calls handled asynchronously and futures represent awaited results for requests. This results in a well structured distributed object language enabling a concise representation of asynchronous method invocations. We will also present the properties of this calculus formalized in the Isabelle theorem prover.

14h30 - 15h00 : Gustavo Petri
Equipe Indes
"Relaxed Memory Models: an Operational Approach"

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.

15h00 - 15h15 : Discussion

15h15 - 15h30 : Pause café

15h30 - 16h00 : Muhammad Kant
Equipe Projet Oasis - INRIA Sophia Antipolis
"Update strategies for Transparent First Class futures "

In the context of distributed programming, several different notions have been defined to make parallel or concurrent programming more efficient and more intuitive. Futures represent an example of such notions to improve concurrency in a natural and transparent way. A future is a temporary object that is used as a place holder for a result of a concurrent computation. Once the computation is complete and a value for the result (called future value) is available, the future is updated with the computed value. Access to an unresolved future is a blocking operation. As results are only awaited when they are really needed, computation is parallelised in a somehow optimal way. This work focusses on the various strategies that can be employed to update futures in a somewhat optimal manner. We present three different future update strategies using semi-formal notation, a simple cost analysis model backed by experimental evaluation.

16h00 - 16h30 : Tamara Rezk
Equipe Indes
"A Compiler for Security "

It is common knowledge that cryptographic schemes are constructed to resist attacks guided by malicious attempts to deviate some intended functionality. However, very little is known about the level of security that we get by using cryptographic schemes in different environments, since security depends on the strength of the adversary. How much can we assume about an unknown adversary without compromising security? On one hand, many works that aim at proving that programs which use cryptography are secure assume specific strategies that the adversary may or may not use when attacking the system. Unfortunately, experience shows that limitations to the power of the adversary are not always realistic. On the other hand, the area of provable or computational cryptography that started to develop since the early 90s proposes that the only assumptions on the adversary that can be justified are his/her computational abilities.
Reasoning with arbitrary adversaries involves the handling of polynomial and probabilistic hypotheses on complex programs. Can we let the programmer specify security policies at an abstract level and let the compiler implement them using provable cryptography?
This presentation will describe work in progress with Cédric Fournet and Gurvan Le Guernic on programming language abstractions for provable cryptography, and a compiler that implements it.

16h30 - 16h45 : Discussion

16h45 : Fin du séminaire