EMSEC's research activities are organized along three axes, namely cryptography, formal methods for security, and the security of hardware and software systems.

EMSEC addresses the design of secure building blocks based on security proofs and cryptanalysis of such blocks.

The addressed topics include:

• Design of ciphers: lightweight block ciphers, authenticated encryption schemes, etc.
• Lattice-based cryptography, security proofs and advanced constructions
• Cryptanalysis of symmetric and asymmetric constructions, cryptanalytic time-memory trade-off
• Security of cryptographic implementations: side-channel attacks and countermeasures
• Design and cryptanalysis of protocols: distance bounding, SSL/TLS, multi-party contract signing protocols, and protocols for low cost device (RFID tags, smartcards, etc.)
• Fully homomorphic encryption, symmetric searchable encryption

One of the major concerns of information security is to establish security proofs. EMSEC investigates the usage of formal methods as well as the development of novel techniques for reasoning about security.

The addressed topics include:

• Formal proofs for cryptographic protocols: key establishment, RFID, distance bounding
• Models for quantitative analysis of security
• Risk analysis based on attack trees
• Cryptanalysis of block ciphers using solvers (CP, SAT, MILP)

EMSEC works on finding vulnerabilities in real-world systems, with the aim to provide the security community with valuable feedback and lead to more secure designs.

The addressed topics include:

• Micro-architectural attacks, including side-channel attacks and software-based fault attacks
• Data security & machine learning, including data desanonymisation and forensics in embedded systems
• Relay attacks against smartcard-based systems
• Smartphone security

TLS/SSL (currently version TLS 1.2) is one of the 3 essential cryptographic protocols used today (together with SSH and IPSec). Despite its central role in securing e-commerce, Internet browsing, email, VoIP, etc., despite the fact that almost every search and connection query in every browser in the world requires its use, this protocol still presents security flaws in its conception. To overcome recent attacks, such as FREAK, LogJam, 3Shake, SLOTH, or DROWN, a new version i.e. TLS 1.3 has recently been drafted. SafeTLS addresses the security both of TLS 1.3 and of TLS 1.2 as they are (expected to be) used.

Cryptography is the cornerstone for securing data and digital exchanges. The coming of a quantum computer, that relies on different physical concepts, threatens most of those applications. Henceforth, substantial technical developments change must occur over the following years. These changes must guarantee to those fields an acceptable and lasting level of security and ensure digital exchange confidentiality and user privacy. The RISQ project applies to every field of technology employing cryptographic methods. The outcome of this project will include an exhaustive encryption and transaction signature product line, as well as an adaptation of the TLS protocol. Hardware and software cryptographic solutions meeting these constraints in terms of security and embedded integration will also be included. Furthermore, documents guiding industrials on the integration of these post-quantum technologies into complex systems (defense, cloud, identity and payment markets) will be produced, as well as reports on the activities of standardization committees.

Symmetric cryptosystems are widely used because they are the only ones that can achieve some major functionalities such as high-speed or low-cost encryption, fast message authentication, and efficient hashing. But, unlike public-key cryptographic algorithms, secret-key primitives do not have satisfying security proofs. The security of those algorithms is thus empirically established by the non-discovery of attacks or weaknesses by researchers. It is obvious that this security criterion, despite its so far success, is not satisfactory, at least morally. For instance we may estimate that, for a given primitive, no more than a few dozens of researchers are actively working on breaking it. Hence, due to this weak effort, the non-discovery of an attack against a particular primitive does not mean so much. We may hope that a large class of attacks, and in particular the simplest, could be automatically discovered. The statement "we did not find any attacks of this kind" only offering a subjective guarantee could become "the audit tool X did not find any attack" which is a formal statement, giving a quantifiable objective guarantee. The ANR JCJC CryptAudit project is a proposal to address this concern and we aim to both develop new cryptanalytical techniques and provide a new set of open-source tools dedicated to symmetric primitives audit.

The main objective of the POPSTAR project is to develop foundations and practical tools to analyse modern security protocols that establish and rely on physical properties. The POPSTAR project will significantly advance the use of formal verification to contribute to the security analysis of protocols that rely on physical properties. This project is bold and ambitious, and answers the forthcoming expectation from consumers and citizens for high level of trust and confidence about contactless nomadic devices.

Cybersecurity is an important but also unpopular aspect of our online experience. Guidance provided to users tends to be complicated or even contradictory. The effect is that people become weary of cybersecurity and give up trying. Introduced in the 70s, scripts are what telemarketers and scammers have been using successfully in order to achieve their goals. In this project we aim at extending scripts to cybersecurity, with the goal of providing simple and efficient cybersecurity guidance to users. The objective is to define attack scripts and the corresponding counter-scripts that people can follow to stay secure in cyberspace. We will develop a formal language for scripts. It will allow us to unambiguously reason about adversarial and defensive actions, and it will be the basis to generate the guidelines for end users. In order to select the best possible counter-scripts for a given attack script, we will employ quantitative analysis techniques for security, based on attack-defense trees. "Foundations of Cybersecurity Scripts" is a three-year project funded by the CNRS PICS program, involving the EMSEC group from IRISA and the School of Mathematical and Computer Sciences, Department of Computer Science, at Heriot-Watt University, Edinburg in Scotland.

PROMETHEUS is a Horizon 2020 project funded for four years by the European Union (under grant agreement No 780701). The project gathers twelve partners from seven countries: seven of the partners are universities and/or research institutes, one is a SME partner and four are industrials. PROMETHEUS aims to provide post-quantum signature schemes, encryption schemes and privacy-preserving protocols relying on lattice.

Formal methods have been shown successful in proving security of cryptographic protocols and finding flaws. However manually proving the security of cryptographic protocols is hard and error-prone. Hence, a large variety of automated verification tools have been developed to prove or find attacks on protocols. These tools differ in their scope, degree of automation and attacker models. Despite the large number of automated verification tools, several cryptographic protocols still represent a real challenge for these tools and reveal their limitations. The aim of this project is to get the best of all these tools, meaning, on the one hand, to improve the theory and implementations of each individual tool towards the strengths of the others and, on the other hand, build bridges that allow the cooperations of the methods/tools.

This project aims to propose a declarative language dedicated to cryptanalytic problems in symmetric key cryptography using constraint programming (CP) to simplify the representation of attacks, to improve existing attacks and to build new cryptographic primitives that withstand these attacks. We also want to compare the different tools that can be used to solve these problems: SAT and MILP where the constraints are homogeneous and CP where the heterogeneous constraints can allow a more complex treatment. One of the challenges of this project will be to define global constraints dedicated to the case of symmetric cryptography. Concerning constraint programming, this project will define new dedicated global constraints, will improve the underlying filtering and solution search algorithms and will propose dedicated explanations generated automatically.

Attacks exploiting micro-architectural vulnerabilities, such as Meltdown, Spectre, Rowhammer etc, are on the rise. Modern day SoCs see an increase in complex design features, such as Branch Prediction, Out-of-Order execution, Cache coherency protocols, integrated GPUs/FPGAs, new non volatile memories. The security aspect of these new architectures and technologies remain under-studied. This project aims at modeling the architectural problems with a virtual platform based on gem5. It will be used for penetration testing, evaluate the performance cost of countermeasures, anticipate new attacks and propose protections. These latter are validated on platforms based on ARM and RISC-V processors. The major impact of this project will be through the creation of a community around our virtual platform.

For 20 years, 3G and 4G mobile networks have allowed users to receive service anywhere, at any time. The dawning, visionary 5th generation mobile network (5G) aims to make telecommunications ubiquitous by using a decentralized architecture, including a massive Internet of Things (mIoT) and a non-federated core network. An important difference between current and future mobile architectures is the variety of devices for which security solutions must be found. Current mobile phones are vulnerable to many attacks, such as malware, Denial-of-Service (DoS), tracking, and cryptographic attacks. Future networks will include IoT devices, which are even more attack-prone, and can be used as “tools” in cyber-attacks. The transition to 5G networks is expected to not only combine, but to compound risks to all types of devices. MobiS5 aims to counter security threats in 5G architectures by providing a provably-secure cryptographic toolbox for 5G networks, validated formally and experimentally, addressing 5G architectures at 3 levels: (1) Infrastructure and physical end-point security, (2) Cryptographic primitives and protocols, and (3) Mobile applications.

Hardware is often considered as an abstract layer that behaves correctly, executing instructions and giving an output. However, side effects due to software implementation and its execution on actual hardware can cause information leakage from side channels, resulting in critical vulnerabilities impacting both the security and privacy of these systems. The MIAOUS project targets in particular information leakage that does not require any physical proximity to devices and that is due to processor microarchitecture, as well as the constructions of novel countermeasures. The main goal of this project is to propose a generic framework that provides a better understanding of the attack surface for microarchitectural attacks, both on the hardware and on the software side, and tools to close the attack surface.