publications

2024

1. A*

   “These results must be false”: A usability evaluation of constant-time analysis tools

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

   In USENIX Security Symposium, 2024

   Abs Bib PDF Artifact

   Cryptography secures our online interactions, transactions, and trust. To achieve this goal, not only do the cryptographic primitives and protocols need to be secure in theory, they also need to be securely implemented by cryptographic library developers in practice. However, implementing cryptographic algorithms securely is challenging, even for skilled professionals, which can lead to vulnerable implementations, especially to side-channel attacks. For timing attacks, a severe class of side-channel attacks, there exist a multitude of tools that are supposed to help cryptographic library developers assess whether their code is vulnerable to timing attacks. Previous work has established that despite an interest in writing constant-time code, cryptographic library developers do not routinely use these tools due to their general lack of usability. However, the precise factors affecting the usability of these tools remain unexplored. While many of the tools are developed in an academic context, we believe that it is worth exploring the factors that contribute to or hinder their effective use by cryptographic library developers. To assess what contributes to and detracts from usability of tools that verify constant-timeness (CT), we conducted a two-part usability study with 24 (post) graduate student participants on 6 tools across diverse tasks that approximate real-world use cases for cryptographic library developers. We find that all studied tools are affected by similar usability issues to varying degrees, with no tool excelling in usability, and usability issues preventing their effective use. Based on our results, we recommend that effective tools for verifying CT need usable documentation, simple installation, easy to adapt examples, clear output corresponding to CT violations, and minimal noninvasive code markup. We contribute first steps to achieving these with limited academic resources, with our documentation, examples, and installation scripts

   @inproceedings{2024usec,
     author = {Fourné, Marcel and De Almeida Braga, Daniel and Jancar, Jan and Sabt, Mohamed and Schwabe, Peter and Barthe, Gilles and Fouque, Pierre{-}Alain and Acar, Yasemin},
     booktitle = {{USENIX} Security Symposium},
     title = {``These results must be false'': A usability evaluation of constant-time analysis tools},
     publisher = {{USENIX} Association},
     year = {2024},
   }

2. A

   Generic and Automated Drive-by GPU Cache Attacks from the Browser

   Giner, Lukas, Czerny, Roland, Gruber, Christoph, Rauscher, Fabian, Kogler, Andreas,  De Almeida Braga, Daniel, and Gruss, Daniel

   In AsiaCCS, 2024

   Abs Bib PDF Artifact

   In recent years, the use of GPUs for general-purpose computations has steadily increased. As security-critical computations like AES are becoming more common on GPUs, the scrutiny must also in- crease. At the same time, new technologies like WebGPU put easy access to compute shaders in every web browser. Prior work has shown that GPU caches are vulnerable to the same eviction-based attacks as CPUs, e.g., Prime+Probe, from native code. In this paper, we present the first GPU cache side-channel attack from within the browser, more specifically from the restricted WebGPU environment. The foundation for our generic and automated attacks are self-configuring primitives applicable to a wide variety of devices, which we demonstrate on a set of 11 desktop GPUs from 5 different generations and 2 vendors. We leverage features of the new WebGPU standard to create shaders that implement all building blocks needed for cache side-channel attacks, such as tech- niques to distinguish L2 cache hits from misses. Beyond the state of the art, we leverage the massive parallelism of modern GPUs to design the first parallelized eviction set construction algorithm. Based on our attack primitives, we present three case studies: First, we present an inter-keystroke timing attack with high F1-scores, i.e., 82 % to 98 % on NVIDIA. Second, we demonstrate a generic, set-agnostic, end-to-end attack on a GPU-based AES encryption service, leaking a full AES key in 6 minutes . Third, we evaluate a native-to-browser data-exfiltration scenario with a Prime+Probe covert channel that achieves transmission rates of up to 10.9 kB/s. Our attacks require no user interaction and work in a time frame that easily enables drive-by attacks while browsing the Internet. Our work emphasizes that browser vendors need to treat access to the GPU similar to other security- and privacy-related resources.

   @inproceedings{2024asiaccs,
     author = {Giner, Lukas and Czerny, Roland and Gruber, Christoph and Rauscher, Fabian and Kogler, Andreas and De Almeida Braga, Daniel and Gruss, Daniel},
     booktitle = {AsiaCCS},
     title = {Generic and Automated Drive-by GPU Cache Attacks from the Browser},
     publisher = {{ACM}},
     year = {2024},
   }

2023

1. A

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

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

   In 2023 IEEE 8th European Symposium on Security and Privacy (EuroSP), Jul 2023

   Abs Bib PDF Artifact

   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, despite 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-and-hack 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.

   @inproceedings{braga2023dragondoom,
     author = {De Almeida Braga, Daniel and Kulatova, Natalia and Sabt, Mohamed and Fouque, Pierre{-}Alain and Bhargavan, Karthikeyan},
     booktitle = {2023 IEEE 8th European Symposium on Security and Privacy (EuroSP)},
     pages = {707-723},
     title = {From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake},
     year = {2023},
     month = jul,
   }

2022

1. A*

   “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks

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

   In IEEE Symposium on Security and Privacy (SP), May 2022

   Abs Bib PDF Artifact

   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, “these attacks are not that hard to mitigate”: 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.

   @inproceedings{IEEE:conf/sp/JancarFBSSBFA21,
     author = {Jancar, Jan and Fourné, Marcel and De Almeida Braga, Daniel and Sabt, Mohamed and Schwabe, Peter and Barthe, Gilles and Fouque, Pierre{-}Alain and Acar, Yasemin},
     booktitle = {IEEE Symposium on Security and Privacy (SP)},
     title = {“They're not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks},
     year = {2022},
     volume = {},
     issn = {2375-1207},
     pages = {755-772},
     keywords = {constant-time;timing-attacks;cryptographic-library;survey;developer-survey;expert-survey;usable-security;human-factors;cryptography},
     doi = {10.1109/SP46214.2022.00044},
     url = {https://doi.ieeecomputersociety.org/10.1109/SP46214.2022.00044},
     publisher = {IEEE Computer Society},
     address = {Los Alamitos, CA, USA},
     month = may,
   }

2021

1. A*

   PARASITE: PAssword Recovery Attack against Srp Implementations in ThE wild

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

   In CCS, May 2021

   Abs Bib PDF Artifact Slides

   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 particu- lar 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.

   @inproceedings{DBLP:conf/ccs/BragaFS21,
     author = {De Almeida Braga, Daniel and Fouque, Pierre{-}Alain and Sabt, Mohamed},
     title = {{PARASITE:} PAssword Recovery Attack against Srp Implementations in ThE wild},
     booktitle = {{CCS}},
     pages = {2497--2512},
     publisher = {{ACM}},
     year = {2021},
   }

2020

1. A

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

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

   In ACSAC, May 2020

   Abs Bib PDF Artifact Slides

   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, demon- strating 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 de- ployed 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 up- stream 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.

   @inproceedings{DBLP:conf/acsac/BragaFS20,
     author = {De Almeida Braga, Daniel and Fouque, Pierre{-}Alain and Sabt, Mohamed},
     title = {Dragonblood is Still Leaking: Practical Cache-based Side-Channel in the Wild},
     booktitle = {{ACSAC}},
     pages = {291--303},
     publisher = {{ACM}},
     year = {2020},
   }

2. A

   The Long and Winding Path to Secure Implementation of GlobalPlatform SCP10

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

   IACR Trans. Cryptogr. Hardw. Embed. Syst., May 2020

   Abs Bib PDF Artifact Slides

   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.

   @article{DBLP:journals/tches/BragaFS20,
     author = {De Almeida Braga, Daniel and Fouque, Pierre{-}Alain and Sabt, Mohamed},
     title = {The Long and Winding Path to Secure Implementation of GlobalPlatform {SCP10}},
     journal = {{IACR} Trans. Cryptogr. Hardw. Embed. Syst.},
     volume = {2020},
     number = {3},
     pages = {196--218},
     year = {2020},
   }