- Cet évènement est passé

Le 7 novembre prochain, aura lieu la journée des doctorants du département 2, toute la journée, en salle A 008.

**PROGRAMME**

09h00 – 09h30 Accueil (café+thé+croissants+pains au chocolat)

09h30 – 10h00 Joseph Lallemand

10h00 – 10h30 Sylvain Cecchetto

10h30 – 11h00 Pause (café+thé)

11h00 – 11h30 Itsaka Rakotonirina

11h30 – 12h00 Pierre Mercuriali

12h00 – 12h30 Younes Abid

12h30 – 14h00 Pizzas

14h00 – 14h30 Margaux Duroeulx

14h30 – 15h00 Renaud Vilmart

**DETAILS DES EXPOSÉS**

—————————————————————-

Joseph Lallemand

Titre: A Type System for Privacy Properties

Abstract: Mature push button tools have emerged for checking trace

properties (e.g. secrecy or authentication) of security protocols. The

case of indistinguishability-based privacy properties (e.g. ballot

privacy or anonymity) is more complex and constitutes an active

research topic with several recent propositions of techniques and

tools.

We explore a novel approach based on type systems and provide a

(sound) type system for proving equivalence of protocols, for a

bounded or an unbounded number of sessions. The resulting prototype

implementation has been tested on various protocols of the

literature. It provides a significant speed-up (by orders of

magnitude) compared to tools for a bounded number of sessions and

complements in terms of expressiveness other state-of-the-art tools,

such as ProVerif and Tamarin: e.g., we show that our analysis

technique is the first one to handle a faithful encoding of the Helios

e-voting protocol in the context of an untrusted ballot box.

—————————————————————-

Sylvain Cecchetto

Titre : Falsification des instructions RET dans les binaires malveillants

Abstract: The classical compilation scheme to calling a function is to

use the CALL instruction to jump in the function and, at the end of

it, return to the expected return site pushed on the stack by the CALL

with the aid of the RET instruction.

This obfuscation technique alter this rule. The RET is tampered if it

does not return to the expected returnsite pushed on the stack by the

CALL.

—————————————————————-

Nicolas Schnepf:

Orchestration and verification of security functions for smart environments

The number of malicious applications targeting mobile environments

increases exponentially each year. Against this threat the preventive

mechanisms deployed on markets show their limits and need to be

completed by reactive methods deployed directly on the devices;

however this deployment is made difficult by the low battery and CPU

resources of smart environments. In this context a promising approach

could be to deploy chains of security functions in cloud

infrastructure by using the programability provided by software

defined networking (SDN); nevertheless the complexity and the dynamics

of those chains make their validation difficult, introducing the

requirement of using formal verification methods for enabling their

automated deployment.

Focusing on this research problem, we already published a first paper

describing synaptic, our framework for the verification of SDN rules

specified with the dedicated pyretic language: for enabling the

verification of such policies synaptic relies on our translation

algorithms for generating a formal model that can then be verified

either by SMT solving or by model checking. In complement to this

framework we proposed an approach for automatically generating finite

states automata capturing the networking behavior of Android

applications: these automata are used for automatically producing

corresponding pyretic policies that are then verified by our checker

and finally deployed into the network for protecting end users.

—————————————————————-

Pierre Mercuriali:

Normal form systems generated by a single connective are equivalent.

In this talk we will focus on the efficient representation of Boolean

functions using Normal Form Systems (NFS), that yield sets of terms

built using one or several connectives (taken in a specific order),

variables and negated variables, and constants. Efficiency is measured

in terms of the size (number of connectives) of the terms used to

represent a function.

The connectives chosen are those that generate Boolean clones, that

are classes of functions stable by composition and that contain all

projections. For instance, the clone of all conjunctions Λ is

generated by the binary connective ∧. It was proven that the Median

NFS associated with the ternary median connective is more efficient

than the DNF, CNF, PNF and PᵈNF.

This first study gives rise to several unaddressed questions. Are

there other such efficient NFS? Which clones/generators yield the

most efficient representations? For instance, does the efficiency

improve when taking a 5-ary median instead of the ternary one? During

this talk we will answer these and several other questions related to

the efficiency of NFSs.

—————————————————————-

Itsaka Rakotonirina

Verifying equivalence of finite processes

Abstract:

Careless design choices in security protocols may lead to a user being

able to usurp the identity of honest entities, obtain sensible

data… How to be sure that the structure of a protocol really

prevents sensible data from ending up in unauthorised hands? How to

guarantee that malicious users cannot impersonate others? Designing

protocols verifying such properties is notoriously hard and humans

have proven rather bad at analyzing them by hand.

In this work we propose an automated analysis of (in)security. We

provide a procedure deciding whether a given security property,

formalised by an equivalence statement, is verified by a finite number

of sessions of a protocol. The approach is implemented in an automated

tool called DEEPSEC, whose applicability has been demonstrated on

several case studies.

—————————————————————-

Margaux Duroeulx

Modélisation, vérification formelle symbolique et évaluation

probabiliste du niveau de confiance des systèmes sécuritaires

numériques.

Ma thèse traite des systèmes critiques comme les trains ou les

centrales nucléaires. Elle vise à calculer la fiabilité des systèmes

critiques afin d’anticiper leurs défaillances et qu’elles soient

évitées. On évoque parfois la sûreté, qui consiste en la prévention

des défaillances dangereuses pour les biens, les personnes et

l’environnement du système qui est etudié.

La probabilité d’apparition d’une défaillance et sa criticité (faible,

normale, catastrophique) sont les deux paramètres essentiels pour

savoir si une défaillance est dangereuse ou non, car elle peut être

peu critique mais très fréquente, et vice versa. C’est la raison pour

laquelle j’étudie la fiabilité des systèmes, afin de calculer la

probabilité d’occurence de chaque défaillance possible.

J’utilise des techniques informatiques comme la satisfiabilité, pour

modéliser les systèmes critiques et estimer leur fiabilité.

—————————————————————-

Renaud Vilmart

ZX-Calculus: A Graphical Language for Quantum Reasoning and Computing

The quantum computer is a promising model of

computation. With a quantum computer the size of our current

computers, one could theoretically compute the prime decomposition of

a number in polynomial time with respect to the size of the number;

which is a problem considered hard enough – for classical computers –

to have cryptosystems based on it.

Whether or not such a computer is achievable is an open question, even

though small ones already exist, and some companies (D-Wave, IBM, Atos

…) are willing to spend millions to build powerful ones.

In the meantime, engineers and researchers have turned to quantum

circuitry (a language similar the classical circuitry) in order to

build algorithms. However, two different circuits may represent the

same quantum evolution – or algorithm. For instance, as for the

classical case, two consecutive NOT gates are equivalent to the

identity. One might then want to equip circuits with a set of

transformation rules, that change the circuit, but not the overall

result.

ZX-Calculus is another diagrammatic language well-fitted for quantum

computation. Even though it is closely related to circuits, it is

laxer, which simplifies the research for transformation rules. Indeed,

here, some non-unitary operations are allowed, and the wires can be

bent at will, which greatly changes our conception of the mathematical

objects we handle, and that we call here diagrams.

ZX-Calculus can be used for reasoning on quantum circuits: these can

easily be transformed into ZX-diagrams, and there exists a method that

characterises “circuit-like” diagrams. ZX-Calculus can hence be used

to simplify a circuit, or check if two circuits are equivalent. The

applications of the language are not limited to circuitry. For

instance the generators of the ZX-Calculus match exactly the

operations of lattice surgery, a promising model designed for error

correction.

I will present the language ZX-Calculus and a few of its properties,

most importantly, results about completeness: the ability to

transform, using the rewrite rules only, any two diagrams that

represent the same evolution.

—————————————————————-

Younes Abid – TBA

TBA