Mohamed Sabt | Publications

2023

From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake

Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, and Karthikeyan Bhargavan

In EuroS&P, 2023.
Propose patch to hostap.

Abs

It is universally acknowledged that Wi-Fi communications are important to secure. Thus, the Wi-Fi Alliance published WPA3 in 2018 with a distinctive security feature: it leverages a Password-Authenticated Key Exchange (PAKE) protocol to protect users’ passwords from offline dictionary attacks. Unfortunately, soon after its release, several attacks were reported against its implementations, in response to which the protocol was updated in a best-effort manner. In this paper, we show that the proposed mitigations are not enough, especially for a complex protocol to implement even for savvy developers. Indeed, we present Dragondoom, a collection of side-channel vulnerabilities of varying strength allowing attackers to recover users’ passwords in widely deployed Wi-Fi daemons, such as hostap in its default settings. Our findings target both password conversion methods, namely the default probabilistic hunting-and-pecking and its newly standardized deterministic alternative based on SSWU. We successfully exploit our leakage in practice through microarchitectural mechanisms, and overcome the limited spatial resolution of Flush+Reload. Our attacks outperform previous works in terms of required measurements. Then, driven by the need to end the spiral of patch-andhack in Dragonfly implementations, we propose Dragonstar, an implementation of Dragonfly leveraging a formally verified implementation of the underlying mathematical operations, thereby removing all the related leakage vector. Our implementation relies on HACL*, a formally verified crypto library guaranteeing secret-independence. We design Dragonstar, so that its integration within hostap requires minimal modifications to the existing project. Our experiments show that the performance of HACL*-based hostap is comparable to OpenSSL-based, implying that Dragonstar is both efficient and proved to be leakage-free.

2022

WideLeak: How Over-the-Top Platforms Fail in Android

Gwendal Patat, Mohamed Sabt, and Pierre-Alain Fouque

In DSN, 2022.
Awarded by Hall of Fame of Netflix.

Abs Paper Code

Nowadays, most content providers rely on DRM (Digital Right Management) to protect media from illegal distribution. Becoming a major platform for streaming, Android provides its own DRM framework that does not comply with existing DRM standards. Thus, OTT (over-the-top) platforms need to adapt their apps to suit Android design, despite a fragmented ecosystem and little public documentation. Unfortunately, the security implications of how OTT apps leverage Widevine, the most popular Android DRM, have not been studied yet. In this paper, we report the first experimental study on the state of Widevine use in the wild. Our study explores OTT compliance with Widevine guidelines regarding asset protection and legacy phone support. With the evaluation of premium OTT apps, our experiments bring to light that most apps adopt weak and potentially vulnerable practices. We illustrate our findings by showing how to easily recover media content from many OTT apps, including Netflix.
Exploring Widevine for Fun and Profit

Gwendal Patat, Mohamed Sabt, and Pierre-Alain Fouque

In SP Workshops, 2022.
Awarded by Hall of Fame of Google.

Abs Paper Code

For years, Digital Right Management (DRM) systems have been used as the go-to solution for media content protection against piracy. With the growing consumption of content using Over-the-Top platforms, such as Netflix or Prime Video, DRMs have been deployed on numerous devices considered as potential hostile environments. In this paper, we focus on the most widespread solution, the closed-source Widevine DRM. Installed on billions of devices, Widevine relies on cryptographic operations to protect content. Our work presents a study of Widevine internals on Android, mapping its distinct components and bringing out its different cryptographic keys involved in content decryption. We provide a structural view of Widevine as a protocol with its complete key ladder. Based on our insights, we develop WideXtractor, a tool based on Frida to trace Widevine function calls and intercept messages for inspection. Using this tool, we analyze Netflix usage of Widevine as a proof-of-concept, and raised privacy concerns on user-tracking. In addition, we leverage our knowledge to bypass the obfuscation of Android Widevine software-only version, namely L3, and recover its Root-of-Trust.
“They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks

Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar

In SP, 2022.
Also presented at Real World Crypto 2022.

Abs Paper

Timing attacks are among the most devastating side-channel attacks, allowing remote attackers to retrieve secret material, including cryptographic keys, with relative ease. In principle, \lq\lq these attacks are not that hard to mitigate\rq\rq : the basic intuition, captured by the constant-time criterion, is that control-flow and memory accesses should be independent from secrets. Furthermore, there is a broad range of tools for automatically checking adherence to this intuition. Yet, these attacks still plague popular cryptographic libraries twenty-five years after their discovery, reflecting a dangerous gap between academic research and cryptographic engineering. This gap can potentially undermine the emerging shift towards high-assurance, formally verified cryptographic libraries. However, the causes for this gap remain uninvestigated. To understand the causes of this gap, we conducted a survey with 44 developers of 27 prominent open-source cryptographic libraries. The goal of the survey was to analyze if and how the developers ensure that their code executes in constant time. Our main findings are that developers are aware of timing attacks and of their potentially dramatic consequences and yet often prioritize other issues over the perceived huge investment of time and resources currently needed to make their code resistant to timing attacks. Based on the survey, we identify several shortcomings in existing analysis tools for constant-time, and issue recommendations that can make writing constant-time libraries less difficult. Our recommendations can inform future development of analysis tools, security-aware compilers, and cryptographic libraries, not only for constant-timeness, but in the broader context of side-channel attacks, in particular for micro-architectural side-channel attacks, which are a younger topic and too recent as focus for this survey.

2021

Implementation of Lattice Trapdoors on Modules and Applications

Pauline Bert, Gautier Eberhart, Lucas Prabel, Adeline Roux-Langlois, and Mohamed Sabt

In PQCrypto, 2021.

Abs Paper Code

We develop and implement efficient Gaussian preimage sampling techniques on module lattices, which rely on the works of Micciancio and Peikert in 2012, and Micciancio and Genise in 2018. The main advantage of our implementation is its modularity, which makes it practical to use for signature schemes, but also for more advanced constructions using trapdoors such as identity-based encryption. In particular, it is easy to use in the ring or module setting, and to modify the arithmetic on Rq (as different schemes have different conditions on q). Relying on these tools, we also present two instantiations and implementations of proven trapdoor-based signature schemes in the module setting: GPV in the random oracle model and a variant of it in the standard model presented in Bert et al. in 2018. For that last scheme, we address a security issue and correct obsolescence problems in their implementation by building ours from scratch. To the best of our knowledge, this is the first efficient implementation of a lattice-based signature scheme in the standard model. Relying on that last signature, we also present the implementation of a standard model IBE in the module setting. We show that while the resulting schemes may not be competitive with the most efficient NIST candidates, they are practical and run on a standard laptop in acceptable time, which paves the way for practical advanced trapdoor-based constructions.
PARASITE: PAssword Recovery Attack against Srp Implementations in ThE wild

Daniel De Almeida Braga, Pierre-Alain Fouque, and Mohamed Sabt

In CCS, 2021.
OpenSSL Contributor, and ProtonMail Bug Bounty Program.

Abs Paper Code

Protocols for password-based authenticated key exchange (PAKE) allow two users sharing only a short, low-entropy password to establish a secure session with a cryptographically strong key. The challenge in designing such protocols is that they must resist offline dictionary attacks in which an attacker exhaustively enumerates the dictionary of likely passwords in an attempt to match the used password. In this paper, we study the resilience of one particular PAKE against these attacks. Indeed, we focus on the Secure Remote Password (SRP) protocol that was designed by T. Wu in 1998. Despite its lack of formal security proof, SRP has become a de-facto standard. For more than 20 years, many projects have turned towards SRP for their authentication solution, thanks to the availability of open-source implementations with no restrictive licenses. Of particular interest, we mention the Stanford reference implementation (in C and Java) and the OpenSSL one (in C). In this paper, we analyze the security of the SRP implementation inside the OpenSSL library. In particular, we identify that this implementation is vulnerable to offline dictionary attacks. Indeed, we exploit a call for a function computing modular exponentiation of big numbers in OpenSSL. In the SRP protocol, this function leads to the call of a non-constant time function, thereby leaking some information about the used password when leveraging cache-based Flush+Reload timing attack. Then, we show that our attack is practical, since it only requires one single trace, despite the noise of cache measurements. In addition, the attack is quite efficient as the reduction of some common dictionaries is very fast using modern resources at negligible cost. We also prove that the scope of our vulnerability is not only limited to OpenSSL, since many other projects, including Stanford’s, ProtonMail and Apple Homekit, rely on OpenSSL, which makes them vulnerable. We find that our flaw might also impact projects written in Python, Erlang, JavaScript and Ruby, as long as they load the OpenSSL dynamic library for their big number operations. We disclosed our attack to OpenSSL who acknowledged the attack and timely fixed the vulnerability.

2020

Dragonblood is Still Leaking: Practical Cache-based Side-Channel in the Wild

Daniel De Almeida Braga, Pierre-Alain Fouque, and Mohamed Sabt

In ACSAC, 2020.
Second place at the CSAW Europe applied research competition 2020.

Abs Paper Code Slides Video Podcast

Recently, the Dragonblood attacks have attracted new interests on the security of WPA-3 implementation and in particular on the Dragonfly code deployed on many open-source libraries. One attack concerns the protection of users passwords during authentication. In the Password Authentication Key Exchange (PAKE) protocol called Dragonfly, the secret, namely the password, is mapped to an elliptic curve point. This operation is sensitive, as it involves the secret password, and therefore its resistance against side-channel attacks is of utmost importance. Following the initial disclosure of Dragonblood, we notice that this particular attack has been partially patched by only a few implementations. In this work, we show that the patches implemented after the disclosure of Dragonblood are insufficient. We took advantage of state-of-the-art techniques to extend the original attack, demonstrating that we are able to recover the password with only a third of the measurements needed in Dragonblood attack. We mainly apply our attack on two open-source projects: iwd (iNet Wireless Daemon) and FreeRADIUS, in order underline the practicability of our attack. Indeed, the iwd package, written by Intel, is already deployed in the Arch Linux distribution, which is well-known among security experts, and aims to offer an alternative to wpa_supplicant. As for FreeRADIUS, it is widely deployed and well-maintained upstream open-source project. We publish a full Proof of Concept of our attack, and actively participated in the process of patching the vulnerable code. Here, in a backward compatibility perspective, we advise the use of a branch-free implementation as a mitigation technique, as what was used in hostapd, due to its quite simplicity and its negligible incurred overhead.
The Long and Winding Path to Secure Implementation of GlobalPlatform SCP10

Daniel De Almeida Braga, Pierre-Alain Fouque, and Mohamed Sabt

IACR TCHES, 2020.
SCP10 was fixed by GP (amendment).

Abs Paper Code Slides Video

GlobalPlatform (GP) card specifications are defined for smart cards regarding rigorous security requirements. The increasingly more powerful cards within an open ecosystem of multiple players stipulate that asymmetric-key protocols become necessary. In this paper, we analyze SCP10, which is the Secure Channel Protocol (SCP) that relies on RSA for key exchange and authentication. Our findings are twofold. First, we demonstrate several flaws in the design of SCP10. We discuss the scope of the identified flaws by presenting several attack scenarios in which a malicious attacker can recover all the messages protected by SCP10. We provide a full implementation of these attacks. For instance, an attacker can get the freshly generated session keys in less than three hours. Second, we propose a secure implementation of SCP10 and discuss how it can mitigate the discovered flaws. Finally, we measure the overhead incurred by the implemented countermeasures.
Please Remember Me: Security Analysis of U2F Remember Me Implementations in The Wild

Gwendal Patat, and Mohamed Sabt

In SSTIC, 2020.

Abs Paper Slides Video

Users and service providers are increasingly aware of the security issues that arise because of password breaches. Recent studies show that password authentication can be made more secure by relying on second-factor authentication (2FA). Supported by leading web service providers, the FIDO Alliance defines the Universal 2nd Factor (U2F) protocols, an industrial standard that proposes a challenge-response 2FAsolution. The U2F protocols have been thoughtfully designed to ensure high security. In particular, U2F solutions using dedicated hardware tokens fare well in term of security compared to other 2FA authentication systems. Thus, numerous service providers propose U2F in their authentication settings. Although much attention was paid to make U2F easy to use, many users express inconvenience because of the repeated extra step that it would take to log in. In order to address this, several service providers offer a remember me feature that removes the need for 2FA login on trusted devices. In this paper, we present the first systematic analysis of this undocumented feature, and we show that its security implications are not well understood. After introducing the corresponding threat models, we provide an experimental study of existing implementations of remember me. Here, we consider all the supporting websites considered by Yubico. The findings are worrisome: our analyses indicate how bad implementations can make U2F solutions vulnerable to multiple attacks. Moreover, we show that existing implementations do not correspond to the initial security analysis provided by U2F. We also implement two attacks using the identified design flaws. Finally, we discuss several countermeasures that make the remember me feature more secure. We end this work by disclosing a practical attack against Facebook in which an attacker can permanently deactivate the enabled 2FA options of a targeted victim without knowing their authentication credentials.

2019

Patent. Method for Securing Contactless Transactions

Mohamed Sabt, Mouhannad Alattar, and Mohammed Achemlal

In EPO: European Patent Office 2019.
European publication number: EP/3238474.

Abs Patent Website

The invention relates to a method for securing a contactless service transaction, said service being stored in the mobile terminal, said transaction involving the mobile terminal, a contactless reader and a remote server, said server storing at least one piece of data and/or sensitive function of the service, said terminal comprising a security module (14), said method being characterised in that the terminal also stores a contactless security application and that it comprises: receiving a first value for determining a session key; receiving a second value for determining a session key and a first one-time password (OTPin); sending the second value for determining a session key and a message (MAC) for authenticating at least the first password, intended for being verified by the reader, said first and second determination values being used to calculate a session key (Ksess) intended for being used to secure the exchanges.

2018

Practical Implementation of Ring-SIS/LWE Based Signature and IBE

Pauline Bert, Pierre-Alain Fouque, Adeline Roux-Langlois, and Mohamed Sabt

In PQCrypto, 2018.

Abs Paper Slides

Lattice-based signature and Identity-Based Encryption are well-known cryptographic schemes, and having both efficient and provable secure schemes in the standard model is still a challenging task in light of the current NIST post-quantum competition. We address this problem in this paper by mixing standard IBE scheme, _a la ABB (EUROCRYPT 2010) on Ring-SIS/LWE assumptions with the efficient trapdoor of Peikert and Micciancio (EUROCRYPT 2012) and we provide an efficient implementation. Our IBE scheme is more efficient than the IBE scheme of Ducas, Lyubashevsky and Prest based on NTRU assumption and is based on more standard assumptions. We also describe and implement the underlying signature scheme, which is provably secure in the standard model and efficient.

2017

BlindIDS: Market-Compliant and Privacy-Friendly Intrusion Detection System over Encrypted Traffic

Sébastien Canard, Aı̈da Diop, Nizar Kheir, Marie Paindavoine, and Mohamed Sabt

In AsiaCCS, 2017.
Associated patents: WO/2018/065707 and US/10812506.

Abs Paper

The goal of network intrusion detection is to inspect network traffic in order to identify threats and known attack patterns. One of its key features is Deep Packet Inspection (DPI), that extracts the content of network packets and compares it against a set of detection signatures. While DPI is commonly used to protect networks and information systems, it requires direct access to the traffic content, which makes it blinded against encrypted network protocols such as HTTPS. So far, a difficult choice was to be made between the privacy of network users and security through the inspection of their traffic content to detect attacks or malicious activities. This paper presents a novel approach that bridges the gap between network security and privacy. It makes possible to perform DPI directly on encrypted traffic, without knowing neither the traffic content, nor the patterns of detection signatures. The relevance of our work is that it preserves the delicate balance in the security market ecosystem. Indeed, security editors will be able to protect their distinctive detection signatures and supply service providers only with encrypted attack patterns. In addition, service providers will be able to integrate the encrypted signatures in their architectures and perform DPI without compromising the privacy of network communications. Finally, users will be able to preserve their privacy through traffic encryption, while also benefiting from network security services. The extensive experiments conducted in this paper prove that, compared to existing encryption schemes, our solution reduces by 3 orders of magnitude the connection setup time for new users, and by 6 orders of magnitude the consumed memory space on the DPI appliance.

2016

Cryptanalysis of GlobalPlatform Secure Channel Protocols

Mohamed Sabt, and Jacques Traoré

In SSR, 2016.

Abs Paper Slides

GlobalPlatform (GP) card specifications are the de facto standards for the industry of smart cards. Being highly sensitive, GP specifications were defined regarding stringent security requirements. In this paper, we analyze the cryptographic core of these requirements; i.e. the family of Secure Channel Protocols (SCP). Our main results are twofold. First, we demonstrate a theoretical attack against SCP02, which is the most popular protocol in the SCP family. We discuss the scope of our attack by presenting an actual scenario in which a malicious entity can exploit it in order to recover encrypted messages. Second, we investigate the security of SCP03 that was introduced as an amendment in 2009. We find that it provably satisfies strong notions of security. Of particular interest, we prove that SCP03 withstands algorithm substitution attacks (ASAs) defined by Bellare et al. that may lead to secret mass surveillance. Our findings highlight the great value of the paradigm of provable security for standards and certification, since unlike extensive evaluation, it formally guarantees the absence of security flaws.
Breaking into the KeyStore: A Practical Forgery Attack Against Android KeyStore

Mohamed Sabt, and Jacques Traoré

In ESORICS, 2016.
Public Outreach: ThreatPost Article.

Abs Paper Slides

We analyze the security of Android KeyStore, a system service whose purpose is to shield users credentials and cryptographic keys. The KeyStore protects the integrity and the confidentiality of keys by using a particular encryption scheme. Our main results are twofold. First, we formally prove that the used encryption scheme does not provide integrity, which means that an attacker is able to undetectably modify the stored keys. Second, we exploit this aw to define a forgery attack breaching the security guaranteed by the KeyStore. In particular, our attack allows a malicious application to make mobile apps to unwittingly perform secure protocols using weak keys. The threat is concrete: the attacker goes undetected while compromising the security of users. Our findings highlight an important fact: intuition often goes wrong when security is concerned. Unfortunately, system designers still tend to choose cryptographic schemes not for their proved security but for their apparent simplicity. We show, once again, that this is not a good choice, since it usually results in severe consequences for the whole underlying system.
Patent. Method of Protecting a Mobile Terminal Against Attacks

Mohamed Sabt, and Mohammed Achemlal

In WIPO: World Intellectual Property Organization, 2016.
International publication number: WO/2016/051059.

Abs Patent Website

The invention relates to a method of detecting an attack aimed at a mobile terminal, the terminal comprising a security element, a contactless controller suitable for dialoguing with a contactless reader and a secure execution environment, in which: - any command (C-APDU) originating from the contactless reader and received by the contactless controller is dispatched to the secure execution environment and to the security module, and - any command (C-APDU) received by the security element is dispatched to the secure execution environment, the method comprising a step of verification, implemented by the secure execution environment, in the course of which it is verified that to a command (C-APDU) received from the contactless controller there corresponds a same command (C-APDU) received from the security element, in the converse case a software attack of relay type is detected.

2015

Trusted Execution Environment: What It is, and What It is Not

Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah

In TrustCom/BigDataSE/ISPA, 2015.

Abs Paper Slides

Nowadays, there is a trend to design complex, yet secure systems. In this context, the Trusted Execution Environment (TEE) was designed to enrich the previously defined trusted platforms. TEE is commonly known as an isolated processing environment in which applications can be securely executed irrespective of the rest of the system. However, TEE still lacks a precise definition as well as representative building blocks that systematize its design. Existing definitions of TEE are largely inconsistent and unspecific, which leads to confusion in the use of the term and its differentiation from related concepts, such as secure execution environment (SEE). In this paper, we propose a precise definition of TEE and analyze its core properties. Furthermore, we discuss important concepts related to TEE, such as trust and formal verification. We give a short survey on the existing academic and industrial ARM TrustZone-based TEE, and compare them using our proposed definition. Finally, we discuss some known attacks on deployed TEE as well as its wide use to guarantee security in diverse applications.
The Dual-Execution-Environment Approach: Analysis and Comparative Evaluation

Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah

In IFIP SEC, 2015.

Abs Paper Slides

The dual-execution-environment approach (dual-EE) is a trusted model that was defined to allow mobile smart devices to guarantee tamper-resistant execution for highly sensitive applications. Although various solutions implementing dual-EE have been proposed in the literature, this model has not been formalized yet. In this paper, we revisit the dual-EE approach and propose a theoretical framework to systematize the design of dual-EE solutions regarding well-established primitives defined in the Multiple Independent Levels of Security (MILS) architecture. We provide a general classification of the different dual-EE proposals based on their isolation properties. We introduce a comparative framework allowing dual-EE solutions to be evaluated across a common set of criteria. The relevance of our framework is examined by applying it on three technologies, each one represents one category in our classification. Results are consistent and explain some hidden and unexpected properties of each technology. For instance, we find that bare-metal hypervisors are ill-adapted to provide high assurance security even though they might improve the overall security level of the system.
Towards Integrating Trusted Execution Environment into Embedded Autonomic Systems

Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah

In ICAC, 2015.

Abs Paper Poster

Nowadays, there is a trend to integrate trusted computing concepts into autonomic systems. In this context, the Trusted Execution Environment (TEE) was designed to enrich the previously defined trusted platforms. TEE is commonly known as an isolated processing environment in which applications can be securely executed irrespective of the rest of the system. In this work, we propose an architecture in which embedded autonomic systems rely on the properties of TEE to guarantee both their self-protection and self-healing.
Over-the-Internet: Efficient Remote Content Management for Secure Elements in Mobile Devices

Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah

In MOBISECSERV, 2015.

Abs Paper Slides

We propose Over-the-Internet (OTI), a novel system that manages secure element based applications. We demonstrate our solution in the context of NFC ecosystem and show that it can be effectively used for transmitting big applications to the secure element. Our system leverages the GlobalPlatform card specification as well as the GlobalPlatform user-centric ownership model. Our solution integrates the different actors of the NFC ecosystem in its architecture. We propose to leverage the concept of security domain, so that service providers can manage their applications independently from the SE issuer. We implement our solution within available platforms and show that it is secure, fast, reliable and easily deployable.