Chargement Évènements

« Tous les Évènements

  • Cet évènement est passé

Department 2 : PhD Day

novembre 7

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

Share on FacebookShare on Google+Tweet about this on TwitterShare on LinkedIn

Détails

Date :
novembre 7
Catégorie d’Évènement:

En ce moment

Logo du CNRS
Logo Inria
Logo Université de Lorraine