EMSEC performs research on the security of embedded devices, with a special focus on security primitives, schemes, and protocols. The team studies and develops tools, processes, and methods of security engineering that enable security assessment of ubiquitous computing systems and objects. The activities are organized along four axes.
One of the major concerns of information security is to establish security proofs. EMSEC considers computational proofs and formal methods for the verification of communication protocols.
The addressed topics include:
- Computational proofs
- Symbolic proofs
- NP-hard problems
- Security proofs on cryptographic protocols
Design and analysis of primitives, schemes, and protocols
EMSEC addresses the design of secure building blocks based on security proofs and cryptanalysis of such blocks.
The addressed topics include:
- Distance-bounding protocols
- Design of ciphers (lightweight block ciphers, authenticated encryption schemes, etc.)
- Fully homomorphic encryption, symmetric searchable encryption
- Lattice-based cryptosystems
- Cryptanalytic time-memory trade-off
- Cryptographic protocols for low-cost devices (RFID tags, smartcards, etc.)
- Multi-party contract signing protocols
Hardware and software security.
EMSEC exploits reverse-engineering techniques to analyze primitives, schemes, and protocols implemented in embedded systems. This includes (but is not limited to) side-channel analysis and forensics.
The addressed topics include:
- Side-channel attacks and countermeasures
- Forensics in embedded systems
- Browser fingerprinting
- Relay attack against smartcard-based systems
Security analysis of real-world ubiquitous systems
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:
- Risk analysis based on attack-defense trees.
- Analysis of access control systems
- Security of SSL/TLS
- Smartphone security
EMSEC is strongly involved in the scientific community through national and international research projects and structures. In particular, Gildas Avoine chairs the H2020 COST Action IC1403 Cryptacus about cryptanalysis in ubiquitous computing systems, and Pierre-Alain Fouque is the head of the French ANR project Brutus addressing authenticated ciphers and the resistance against side-channel attacks. Gildas Avoine is also the head of the CNRS GDR Security, which is an operational structure of the CNRS gathering French researchers working in the field of computer security.
The Cryptacus project is a H2020 COST Action (IC1403) that aims to improve and adapt the existent cryptanalysis methodologies and tools to the ubiquitous computing framework. Cryptanalysis, which is the assessment of theoretical and practical cryptographic mechanisms designed to ensure security and privacy, will be implemented along four axes: cryptographic models, cryptanalysis of building blocks, hardware and software security engineering, and security assessment of real-world systems. Twenty-nine European states and neighboring countries are so far members of Cryptacus.
The Brutus project aims at investigating the security of authenticated encryption systems. It aims to evaluate carefully the security of the most promising candidates, by trying to attack the underlying primitives or to build security proofs of modes of operation. It targets the traditional black-box setting, but also more "hostile" environments, including the hardware platforms where some side-channel information is available. It also aims at quantifying the impact of not respecting implementation hypotheses such as not reusing a nonce. Finally, a more constructive goal of the Brutus project is to advise solutions in each of these scenarios, including the choice of a cryptosystem and implementation aspects. This constructive task will be extended to the field of white box cryptography, which aims at hiding the key even if the full implementation is available, including any secret data.
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.
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.
Post-quantum security has been pointed out as a crucial issue by the NIST. Several tracks have been derived to address this issue, among which Euclidean lattices is particularly promising. Moreover, this mathematical structure provides efficient encryption schemes which enable to process data in a non trivial way while it is encrypted. These schemes are called Fully Homomorphic Encryption (FHE) schemes, and in practice, several issues have still to be addressed to propose practical solutions, but things evolve quickly. Hence, anyone that would like to use this technology will be interested by new results on the security analysis of these schemes. To reach these results, the core of this collaboration will be to study in details the hardness of lattice problems in ideal lattices.
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.
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.
CNRS-PICS Foundations of Cybersecurity Scripts
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 Computing, School of Science and Engineering from the University of Dundee in Scotland.