Date: November 7
Place: A008
Chairs: Emmanuel Jeandel
09h00 – 09h30
Welcome
09h30 – 10h00 : Joseph Lallemand
A Type System for Privacy Properties
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.
10h00 – 10h30 : Sylvain Cecchetto
Falsification des instructions RET dans les binaires malveillants
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.
10h30 – 11h00 : Pause
11h00 – 11h30 : Itsaka Rakotonirina
Verifying equivalence of finite processes
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.
11h30 – 12h00 : 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.
12h00 – 12h30 : Younes Abid
Dans ce travail nous montrons comment déduire les préférences des utilisateurs des réseaux sociaux par des marches aléatoires dans un graphe social représentant simultanément des attributs et des liens d’amitiés. Dans une première phase, nous réduisons l’espace des valeurs d’attribut par partition en grappes (clusters) homogènes équilibrées. Suivant l’approche Deepwalk, les marches aléatoires sont considérées comme des phrases. Ainsi, déduire un lien caché est équivalent à déduire un mot qui manque dans une phrase. En deuxième phase, nous appliquons des techniques d’apprentissage non supervisées de traitement des langues naturelles (word2vec) pour déduire des valeurs des attributs sensibles (politiciens, santé, divertissement pour adultes…) préférées par les utilisateurs cibles. Nous menons des expériences sur des jeux de données réels (Facebook) pour évaluer notre approche.
12h30 – 14h00 : Déjeuner
14h00 – 14h30 : 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é.
14h30 – 15h00 : 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.
