Date: June 17, 2022
Place: Alice and Bob (B11-B13)
Chair: Emmanuel Jeandel
9h30-10h00 Welcome
10h00-10h30 Dylan Marinho
Guaranteeing Timed Opacity using Parametric Timed Model Checking
Information leakage can have dramatic consequences on systems security.
Among harmful information leaks, the timing information leakage occurs
whenever an attacker successfully deduces confidential internal
information depending on the system execution time. We address the
following timed opacity problem: given a timed system, a private
location and a final location, synthesize the execution times from the
initial location to the final location for which one cannot deduce
whether the system went through the private location. We also consider
the full timed opacity problem, asking whether the system is opaque for
all execution times. We show that these problems are decidable for timed
automata (TAs) but become undecidable when one adds parameters, yielding
parametric timed automata (PTAs). We then devise an algorithm for
synthesizing PTAs parameter valuations guaranteeing that the resulting
TA is opaque and finally show that our method can also apply to program
analysis.
10h30-11h00 Alexandre Clément
Graphical language(s) for quantum control
Our work is about a ZX-like graphical language, inspired by
linear optics, that can represent some simple quantum control schemes
such as the quantum switch. I will first talk about the core language
and its complete axiomatisation, then I will discuss some extensions.
11h00-11h30 Tristan Benoît
Similarités des binaires
On considère le problème de la recherche d’un clone.
Selon un programme cible et un dépôt de programmes connues (tous en format exécutable),
Le but est de retrouver un programme dans le dépôt qui est est un clone du programme cible.
Malgré le récent intérêt en la similarité des codes binaires, la plupart sont focalisés sur des similarités au niveau des fonctions.
L’état de l’art souffre d’une faible précision, de longues durées d’exécution ou d’une faible robustesse. Nous introduisons une nouvelle similarité au niveau du programme pour combler ces lacunes.
11h30-12h00 Agustin Borgna
Encoding high-level quantum programs as SZX-diagrams
The Scalable ZX-calculus is a compact graphical language used to reason about
linear maps between quantum states.These diagrams have multiple applications,
but they frequently have to be constructed in a case-by-case basis. In this talk
I will present a method to encode quantum programs implemented in a fragment of
the linear dependently typed Proto-Quipper-D language as families of
SZX-diagrams. I will define a subset of translatable Proto-Quipper-D programs
and show that our procedure is able to encode non-trivial algorithms as diagrams
that grow linearly on the size of the program.
