Previous talks




Cybersecurity of industrial systems. Open problems and some ideas.
by Stéphane Mocanu (Inria Rhône-Alpes)

Date : 7 february 2020
Room : Pétri/Turing

Research in cybersecurity of SCADA systems is a relatively recent field developed mainly into the last decade. Despite the manufacturers progress in hardening the security of device SCADA systems are still prone to severe vulnerabilities and specialized countermeasures are still incipient. This talk aims to present the open problems seen from the boundary between computer science and control systems I.e. the architectural view of system (IT/OT/process). We’ll focus mainly on system modelling and vulnerability search and intrusion detection.


Contemporary Issues in Digital Forensics
by Ben Martini (University of South Australia)

Date : 31 january 2020
Room : Pétri/Turing

The discipline of digital forensics, or as it was then known ‘forensic computing’, began with a focus on retrieving admissible evidence from computer systems (typically personal computers). However, with the increased pervasiveness of connected digital technologies in the last 20 years, a wide variety of new and complex sources of digital evidence have emerged. This has presented a range of opportunities and challenges for forensic practitioners.
In this presentation, I will discuss a selection of digital forensics research that I have conducted, with my colleagues and collaborators, in areas such as cloud forensics, mobile forensics and Internet of Things (IoT) forensics. We will look at the challenges of identifying, preserving, collecting and analysing evidence from these platforms, along with proposed solutions, and discuss the applicability of these techniques to the challenges of the next decade.



Intrusion Detection Systems over an Encrypted Traffic: Problem and Solutions
by Sébastien Canard (Orange)

Date : 6 december 2019
Room : Pétri/Turing

Privacy and data confidentiality are today at the heart of many discussions. But such data protection should not be done at the detriment of other security aspects. In the context of network traffic, intrusion detection system becomes in particular totally blind when the traffic is encrypted, making clients again vulnerable to known threats and attacks. Reconciling security and privacy is then one of the major topics for which we should find relevant and scalable solutions that can be deployed as soon as possible. In this context, several recent papers propose to perform Deep Packet Inspection over an encrypted traffic, based on different cryptographic techniques. In this talk, we introduce the main difficulties to design such solutions and give some details about two of them.


La protection des flux en télévision numérique
by Eric Desmicht (DGA)

Date : 22 november 2019
Room : Pétri/Turing

En télévision numérique, des flux numériques comportant de la vidéo sont mis à la disposition des utilisateurs via différents média (cable, satellite, TNT, IP…) et différentes techniques (broadcast, multicast, unicast, support numérique…). Pour garantir les revenus des opérateurs de télévision à péage proposant des contenus à forte valeur ajoutée, il est essentiel que seuls les consommateurs ayant payé pour accéder à ces services puissent réellement y accéder. Rien que pour la France, certains estiment la perte de revenu liée au piratage à 1,3 milliard d’euros annuels.
Dans un premier temps, le profil des attaquants sera introduit ainsi que les standards utilisés pour protéger ces données numériques tout en garantissant l’interopérabilité. Puis l’évolution des mécanismes de sécurité au cours des dernières décennies sera détaillée. D’un décodeur fourni par le diffuseur en boite noire à l’abonné, nous verrons comment le milieu a évolué vers des approches plus ouvertes avec par exemple des décodeurs AndroidTV. En détaillant les spécifications émise par le consortium MovieLabs créé par les majors de cinéma (Warner, Fox, Disney, Universal…) pour renforcer la confidentialité des flux décodés, les techniques matérielles et logicielles demandées pour les décodeurs les plus récents seront introduites. Enfin l’extension de la sécurité vers l’ensemble du système avec du watermarking, de la protection bout en bout et de la défense en profondeur concluront la présentation.


Présentation des fondamentaux du management du risque et d’EBIOS Risk Manager
by Vincent Loriot (ANSSI)

Date : 29 november 2019
Room : Aurigny

Résumé :
a. Présentation ANSSI
b. Tendances de la menace cyber et démarche pour s’en protéger
c. Fondamentaux de la méthode EBIOS Risk Manager

La présentation théorique sera complétée avec un atelier pratique couvrant les sujets suivants :
a. Les besoins et enjeux de sécurité
b. Les couples Source de Risque / Objectif Visé
c. La cartographie de menace de l’écosystème



Subject Access Request and Proof of Ownership
by Cédric Lauradoux (INRIA Rhône-Alpes)

Date : 25 october 2019
Room : Pétri/Turing

The GDPR (General Data Protection Regulation) provides rights on our data: access, rectification, objection, etc. However, this regulation is not binding on how we can exercise these rights. Data controllers have therefore deployed various methods to authenticate subject requests. We have analyzed how this authentication process can fail and examined its consequences. Our study shows that a key concept is missing in the GDPR: Proof of ownership for our data.

JUNE 2019

A Formal Analysis of 5G Authentication
by Sasa Radomirovic (University of Dundee)

Date : 3 june 2019
Room : Métivier

Mobile communication networks connect much of the world’s population. The security of users’ calls, text messages, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose.
In this talk, I will report on our formalization of the 5G standard’s AKA protocol and show how the application of symbolic protocol verification has helped us discover and repair authentication flaws inthe standard.
Joint work with David Basin, Jannik Dreier, Lucca Hirschi, Ralf Sasse, and Vincent Stettler.

MARCH 2019

Voting : You Can’t Have Privacy without Individual Verifiability
by Joseph Lallemand (Loria)

Date : 1 march 2019
Rooms : Pétri/Turing

Electronic voting typically aims at two main security goals: vote privacy and verifiability. These two goals are often seen as antagonistic and some national agencies even impose a hierarchy between them: first privacy, and then verifiability as an additional feature. Verifiability typically includes individual verifiability (a voter can check that her ballot is counted); universal verifiability (anyone can check that the result corresponds to the published ballots); and eligibility verifiability (only legitimate voters may vote). We show that actually, privacy implies individual verifiability. In other words, systems without individual verifiability cannot achieve privacy (under the same trust assumptions). To demonstrate the generality of our result, we show this implication in two different settings, namely cryptographic and symbolic models, for standard notions of privacy and individual verifiability. Our findings also highlight limitations in existing privacy definitions in cryptographic settings.


A Compositional and Complete approach to Verifying Privacy Properties using the Applied Pi-calculus
by Ross Horne (University of Luxembourg)

Date : 8 february 2019
Rooms : Pétri/Turing

The pi-calculus was introduced for verifying cryptographic protocols by Abadi and Fournet in 2001. They proposed an equivalence technique, called bisimilarity, useful for verify privacy properties. It is widely acknowledged (cf. Paige and Tarjan 1987), that bisimilarity is more efficient to check than trace equivalence; however, surprisingly, tools based on the applied pi-calculus typically still implement trace equivalence. I suggest this may be attributed to two problems:
1. Abadi and Fournet did not publish proofs following conference paper from 2001, until a journal version in 2018 with Blanchet. This perhaps reduced the confidence of the community in bisimilarity. Further to providing proofs, the journal version adjusts definitions to avoid some well known limitations in the original presentation.
2. To efficiently implement bisimulation for extensions of the pi-calculus, we typically require a bisimilarity congruence, and no bisimilarity congruence has been proposed for the applied pi-calculus.
To address the second point above I propose a bisimilarity congruence for the applied pi-calculus. I argue that the definition I provide is optimal; and show that it is sufficiently strong to verify privacy properties. The definition makes use of recent advances in concurrency theory that were not available prior to LICS 2018. Furthermore, these results lead us to the first sound and complete modal logic for the applied pi-calculus, that can specify attacks if and only if an attack exists.


Privacy in The 5G-AKA Authentication Protocol
by Adrien Koutsos (LSV)

Date : 18 january 2019
Room : Métivier

The 5G mobile communications standards are being finalized, and drafts are now available. This standard describes the 5G-AKA authentication and key exchange protocol. The previous version of AKA (3G and 4G) are well-known for their lack of privacy against an active adversary (e.g. a user can be massively tracked using IMSI-catcher). This new version of AKA tries to offer more privacy, notably through the use of asymmetric randomized encryption of the users permanent identities. Our first contribution is to show that, while this prevents the mass surveillance coming from IMSI-catchers, this is not sufficient for privacy. In particular, all the other known privacy attacks against 3G and 4G-AKA carry over to 5G-AKA. We also found a new type of vulnerabilities of stateful authentication protocols.
Our main contribution is the following: we modify the 5G-AKA protocol to prevent all known privacy attacks. We do this while keeping the cost and efficiency constraints under which the 5G-AKA protocol was designed. In particular, we have a limited use of randomness, relying on a sequence number whenever 5G-AKA does. This sequence number has to be maintained by the user and the network, making the protocol stateful. Because of this statefulness, our modified 5G-AKA protocol is not unlinkable. Still, we show that our protocol satisfies a weaker notion of unlinkability called $\sigma$-unlinkability. This is a new security notion, which allows for a finer-grained quantification of the privacy provided by a protocol. The security proof is carried out in the Bana-Comon indistinguishability logic, which is well-suited for stateful complex protocols. We also prove mutual authentication between the user and the network as a secondary result.


Splitting the Linux Kernel for Fun and Profit
by Chris Dalton (HP, Bristol, UK)

Date : 7 december 2018
Room : Aurigny

This talk looks at a pragmatic attempt at strengthening the security properties of Linux by introducing a degree of intra-kernel protection into the Linux kernel (supported by CPU Virtualization silicon features). Consider it, if you like, an attempt at retrofitting a ‘micro-kernel’ interface into traditionally monolithic Linux whilst maintaining a single linux code base (yes it’s still Linux), no need for a hypervisor and with reasonable performance characteristics. The motivation for the work was the frightening increase in reliance on the security properties of the Linux kernel driven by trends away from full-virtualization solutions such as VMWare and KVM and towards lighter weight containment approaches led by Docker, et al for application hosting, deployment and consolidation.



Machine Learning for Computer Security Detection Systems: Practical Feedback and Solutions
by Anaël Beaugnon (ANSSI)

Date : 30 november 2018
Room : Métivier

Machine learning based detection models can strengthen detection, but there remain some significant barriers to the widespread deployment of such techniques in operational detection systems. In this presentation, we identify the main challenges to overcome and we provide both methodological guidance and practical solutions to address them. The solutions we present are completely generic to be beneficial to any detection problem on any data type and are freely available in SecuML.
The content of the presentation is mostly based on my PhD thesis “Expert-in-the-Loop Supervised Learning for Computer Security Detection Systems”.


Binary Edwards Curves for intrinsically secure ECC implementations for the IoT
by Antoine Loiseau (CEA)

Date: 7 september 2018
Room: Petri/Turing

Even if recent advances in public key cryptography tend to focus on algorithms able to survive the post quantum era, at present, there is a urgent need to propose fast, low power and securely implemented cryptography to address the immediate security challenges of the IoT. In this talk, we present a new set of Binary Edwards Curves which have been defined to achieve the highest security levels (up to 284-bit security level) and whose parameters have been defined to fit IoT devices embedding 32-bit general purpose processors. We optimized the choice of the point generator with the w-coordinate to save a multiplication in the addition and doubling formulae. We manage to compute one step of the Montgomery Ladder in 4 multiplications and 4 squares. On top of the performance benefits, cryptography over such curves have some intrinsic security properties against physical attacks.


JULY 2018

How to decrypt without keys with GlobalPlatform SCP02 protocol
by Loic Ferreira (Orange Labs, IRISA)

Date: 6 july 2018
Room: Petri/Turing

The GlobalPlatform SCP02 protocol is a security protocol implemented in smart cards, and used by transport companies, in the banking world and by mobile network operators (UICC/SIM cards). We describe how to perform a padding oracle attack against SCP02. The attack allows an adversary to efficiently retrieve plaintext bytes from an encrypted data field. We provide results of our experiments done with 10 smart cards from six different card manufacturers, and show that, in our experimental setting, the attack is fully practical. Given that billions SIM cards are produced every year, the number of affected cards, although difficult to estimate, is potentially high. To the best of our knowledge, this is the first practical attack against SCP02.

JUNE 2018

A theory of assertions for Dolev-Yao models
by Vaishnavi Sundararajan (Chennai Mathematical Institute, India)

Date: 8 june 2018
Room: Amphitheather – Inria Convention center

We undertake an abstract study of certification in security protocols, concentrating on the logical properties and derivability of certificates. Specifically, we extend the Dolev-Yao model with a new class of objects called ‘assertions’, along with an associated algebra for deriving new assertions from old ones. We obtain complexity results for the derivability problem and active intruder problem for this model, and provide a case study via the FOO e-voting protocol.


MARCH 2018

Anonymous Server-Aided Verification
by Elena Pagnin (Chalmers University of Technology, Sweden)

Date: 30 march 2018
Room: Métivier

Server-Aided Verification (SAV) is a method that can be employed to speed up the process of verifying signatures by letting the verifier outsource part of its computation load to a third party. Achieving fast and reliable verification under the presence of an untrusted server is an attractive goal in cloud computing and internet of things scenarios.
In this talk I will describe a simple and powerful framework for SAV and present a security model that refines existing while covering the new notions of SAV-anonymity and extended unforgeability. In addition, I will present the first generic transformation from any signature scheme to a single-round SAV scheme that incorporates verifiable computation.

“Automated verification of privacy-type properties for security protocols”
by Ivan Gazeau (LORIA, Inria Nancy)

Date: 16 march 2018
Room: Petri/Turing

The applied pi-calculus is a powerful framework to model protocols and to define security properties. In this symbolic model, it is possible to verify automatically complex security properties such as strong secrecy, anonymity and unlinkability properties which are based on equivalence of processes.
In this talk, we will see an overview of a verification method used by a tool, Akiss. The tool is able to handle 
- a wide range of cryptographic primitives (in particular AKISS is the only tool able to verify equivalence properties for protocols that use xor); 
- protocols with else branches (the treatment of disequalities is often complicated). 
We will also provide some insights on how interleaving due to concurrency can be effectively handled.

The Internet of Backdoors
by Sam L. Thomas (University of Birmingham, UK)

Date: 7 march 2018
Room: Petri/Turing

Complex embedded devices are becoming ever prevalent in our everyday lives, yet only a tiny amount of people consider the potential security and privacy implications of attaching such devices to our home, business and government networks. As demonstrated through recent publications from academia and blog posts from numerous industry figures, these devices are plagued by poor design choices concerning end-user security. What’s even more worrying, are reports of manufacturers inserting backdoor-like functionality into the production firmware of those devices.
This talk will provide a precise definition of the term backdoor and outline a framework we have devised for reasoning about such constructs. We will discuss the main challenges in backdoor detection, and present two tools we have developed to perform backdoor detection in a semi-automated manner. We will demonstrate the effectiveness of our methods through a number of case-studies of real-world backdoors.


When Good Components Go Bad: Formally Secure CompilationDespite Dynamic Compromise” by Catalin Hritcu (Inria Paris)

Date: 5 february 2018
Room: Petri/Turing

We propose a new formal criterion for secure compilation, providing strong end-to-end security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others until it becomes compromised by exhibiting undefined behavior, opening the door for an attacker to take control over the component and to use the component’s privileges to attack the remaining uncompromised components. More precisely, we ensure that dynamically compromised components cannot break the safety properties of the system at the target level any more than equally privileged components without undefined behavior already could in the source language. To illustrate this model, we build a secure compilation chain for an unsafe language with buffers, procedures, and components. We compile this to a simple RISC abstract machine with built-in compartmentalization and provide machine-checked proofs in Coq showing that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or tag-based reference monitoring.

Breaking and fixing HB+DB: A Short Tale of Provable vs Experimental Security and Lightweight Designs
by Ioana Boureanu (University of Surrey)

Date: 2 february 2018
Room: Petri/Turing

HB+ is a well-know authentication scheme purposely designed to be lightweight. However, HB+ is vulnerable to a key-recovery, man-in-the-middle (MiM) attack dubbed GRS. To this end, at WiSec2015, the HB+DB protocol added a distance-bounding dimension to HB+, which was experimentally shown to counteract the GRS attack.
In this talk, we will exhibit however a number of security flaws in the HB+DB protocol. Some attacks are authentication-driven, others relate to distance-bounding. What is more, we will show that a small refinement on the GRS-strategy still leads to key-recovery in HB+DB, un-deterred by its distance-bounding dimension. We will also propose a new distance-bounding protocol called BLOG, which is based on HB+DB but which is provably secure, enjoys better (asymptotical) security and is more lightweight.

Comments are closed.