On monday, at 2pm - UPEC CMC - Room P2-131

June 12, 2017

TBA

Yuri Gurevich (Microsoft Research)

May 22, 2017

On the chemistry of typestate-oriented actors

Silvia Crafa (Université de Padoue)

Typestate-oriented programming is an extension of the OO paradigm in which objects are modeled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object’s internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. We illustrate the approach by means of a number of examples written in Scala Akka.

May 15, 2017

TBA

Thomas Fernique (LIPN)

TBA

April 3, 2017

Non-commutative lower bounds

Guillaume Lagarde (IRIF)

No knowledge in arithmetic complexity will be assumed.
We still don’t know an explicit polynomial that requires non-commutative circuits of size at least superpolynomial.
However, the context of non commutativity seems to be convenient to get such lower bound because the rigidity of the non-commutativity implies a lot of constraints about the ways to compute.
It is in this context that Nisan, in 1991, provides an exponential lower bound against the non commutative Algebraic Branching Programs computing the permanent, the very first one in arithmetic complexity. We show that this result can be naturally seen as a particular case of a theorem about circuits with *unique parse tree*, and show some extensions to get closer to lower bounds for general NC circuits.
Two joint works: with Guillaume Malod and Sylvain Perifel; with Nutan Limaye and Srikanth Srinivasan.

March 27, 2017

TBA

Catalin Dima (LACL)

TBA

March 20, 2017

Parameterised Verification of Epistemic Properties in Security Protocols

Ioana boureanu (University of Surrey)

Abstract: Verifying certain security requirements is not even always decidable. Furthermore, properties like privacy preservation, which are not expressible as trace properties, can be verified only via few methodologies. In this talk, we will see some of these challenges and how they can be tackled, in part, by parameterised verification of temporal-epistemic logics in specialised multi-agent system semantics.

March 20, 2017

Parameterised Verification of Epistemic Properties in Security Protocols

Ioana boureanu (University of Surrey)

Abstract: Verifying certain security requirements is not even always decidable. Furthermore, properties like privacy preservation, which are not expressible as trace properties, can be verified only via few methodologies. In this talk, we will see some of these challenges and how they can be tackled, in part, by parameterised verification of temporal-epistemic logics in specialised multi-agent system semantics.

February 27, 2017

Probabilistic Disclosure: Maximisation vs. Minimisation

Serge Haddad (LSV)

We consider opacity questions where an observation function provides
to an external attacker a view of the states along executions and
secret executions are those visiting some secret state from a fixed
subset. Disclosure occurs when the observer can deduce from a finite
observation that the execution is secret. In a probabilistic and non
deterministic setting, where an internal agent can choose between
actions, there are two points of view, depending on the status of
this agent: the successive choices can either help the attacker
trying to disclose the secret, if the system has been corrupted, or
they can prevent disclosure as much as possible if these choices are
part of the system design. In the former situation, corresponding to
a worst case, the disclosure value is the supremum over the
strategies of the probability to disclose the secret (maximisation),
whereas in the latter case, the disclosure is the infimum
(minimisation). We address quantitative problems (relation between
the optimal value and a threshold) and qualitative ones (when the
threshold is zero or one) related to both forms of disclosure for a
fixed or finite horizon. For all problems, we characterise their
decidability status and their complexity. Surprisingly, while in
maximisation problems optimal strategies may be chosen among
deterministic ones, it is not the case for minimisation problems,
but more minimisation problems than maximisation ones are decidable.

February 20, 2017

Génération de tests de vulnérabilité appliquée à la vérification de code intermédiaire Java Card

Aymerick Savary (LACL)

La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n’étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG («Vulnerability Test Generation», génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d’intrusions est généré. Cette méthode s’inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d’application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L’extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d’une instruction. Cette méthode nous a permis de tester différents mécanismes d’implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d’étude, la méthode proposée est générique et a été appliquée à d’autres cas d’études.