Speculative execution attacks such as Spectre-PHT and Spectre-STL remain a critical security concern in modern processors. While software-based mitigations like Speculative Load Hardening (SLH) offer effective protection against Spectre-PHT, they are limited in scope and require software-managed speculative masks, which can be error-prone and costly. Defenses against Spectre-STL, such as the Speculative Store Bypass Disable bit (SSBD), incur additional performance overhead and lack fine-grained control. In this work, we introduce dfence, a new CPU instruction that generalizes SLH to mitigate both Spectre-PHT and Spectre-STL with minimal hardware support. dfence enables developers to annotate sensitive registers, with the hardware ensuring that these values do not leak transiently. We implement dfence in the Proteus CPU and evaluate its security and performance, demonstrating less than 1

PLAS provides a forum for exploring and evaluating the use of programming language and program analysis techniques for promoting security in the complete range of software systems, from compilers to machine-learned models and smart contracts. The workshop encourages proposals of new, speculative ideas, evaluations of new or known techniques in practical settings, and discussions of emerging threats and problems. It also hosts position papers that are radical, forward-looking, and lead to lively and insightful discussions influential to the future research at the intersection of programming languages and security. This year will mark the 19th edition of PLAS, which was first held in 2007 in San Diego. The workshop will host 2 keynote talks, by Natasha Fernandes and Binoy Ravindran, and 8 paper presentations.

The popularity of Intel SGX technology in recent years has given rise to a wide range of shielding runtimes to transparently safeguard secure enclave applications against a hostile operating system. Adequate validation of the crucial and numerous shielding runtimes is, however, a multi-faceted and fast-changing challenge, as new attack techniques against SGX enclaves are discovered regularly and commonly necessitate extensive software patches throughout the SGX ecosystem. This paper proposes Pandora, a practical, enclave-aware symbolic execution tool designed to address this challenge. In contrast to existing tools, Pandora's truthful and runtime-agnostic symbolic execution of the exact attested enclave binary for the first time allows to validate the critical enclave shielding runtime itself. Furthermore, Pandora provides principled foundations to deal with the moving-target nature of enclave software security by implementing accurate taint tracking of attacker inputs, a precise symbolic enclave memory model, and support for pluggable vulnerability detectors. We extensively evaluate Pandora on 11 different SGX shielding runtimes with 4 detection plugins for a diverse set of vulnerability types. Our experiments show that Pandora can autonomously discover 200 new and 69 known vulnerable code locations. Notably, Pandora is the first tool that allows a wide-scale ecosystem investigation of recent pointer-alignment software mitigations in real-world SGX enclave runtimes.

The control flow of a program can often be observed through side-channel attacks. Hence, when control flow depends on secrets, attackers can learn information about these secrets. Widely used software-based countermeasures ensure that attacker-observable aspects of the control flow do not depend on secrets, relying on techniques like dummy execution (for balancing code) or conditional execution (for linearizing code). In the current state-of-practice, the primitives to implement these techniques have to be found in an existing instruction set architecture (ISA) that was not designed a priori to provide them, leading to performance, security, and portability issues. To counter these issues, this paper proposes lightweight hardware extensions for supporting these techniques in a principled way. We propose (1) a novel hardware mechanism (mimic execution), that executes an instruction stream only for its attacker-observable effects, and suppresses (most) architectural effects, and (2) ISA support (called AMi, for Architectural Mimicry) and programming models to effectively use mimic execution to balance or linearize code. We show the feasibility and benefits of our proposal by implementing mimic execution and AMi for a 32-bit out-of-order RISC-V core that leaks control flow in multiple ways (via e.g., the branch predictor, instruction timings, and the data cache). Our experimental evaluation shows that the hardware cost is low (most importantly, no impact on the processor's critical path), and that AMi enables significant performance improvements. In particular, AMi reduces the overhead of state-of-the-art linearized code by 60% in our benchmarks.

Control-flow leakage (CFL) attacks enable an attacker to expose control-flow decisions of a victim program via side-channel observations. Linearization (i.e., elimination) of secret-dependent control flow is the main countermeasure against these attacks, yet it comes at a non-negligible cost. Conversely, balancing secret-dependent branches often incurs a smaller overhead, but is notoriously insecure on high-end processors. Hence, linearization has been widely believed to be the only effective countermeasure against CFL attacks. In this paper, we challenge this belief and investigate an unexplored alternative: how to securely balance secret-dependent branches on higher-end processors? We propose Libra, a generic and principled hardware-software codesign to efficiently address CFL on high-end processors. We perform a systematic classification of hardware primitives leaking control flow from the literature, and provide guidelines to handle them with our design. Importantly, Libra enables secure control-flow balancing without the need to disable performance-critical hardware such as the instruction cache and the prefetcher. We formalize the semantics of Libra and propose a code transformation algorithm for securing programs, which we prove correct and secure. Finally, we implement and evaluate Libra on an out-of-order RISC-V processor, showing performance overhead on par with insecure balanced code, and outperforming state-of-the-art linearized code by 19.3

We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-time programs under a non-speculative semantics, ProSpeCT guarantees that speculative and out-of-order execution cause no microarchitectural leaks. This guarantee is achieved by tracking secrets in the processor pipeline and ensuring that they do not influence the microarchitectural state during speculative execution. Our formalization covers a broad class of speculation mechanisms, generalizing prior work. As a result, our security proof covers all known Spectre attacks, including load value injection (LVI) attacks. In addition to the formal model, we provide a prototype hardware implementation of ProSpeCT on a RISC-V processor and show evidence of its low impact on hardware cost, performance, and required software changes. In particular, the experimental evaluation confirms our expectation that for a compliant constant-time binary, enabling ProSpeCT incurs no performance overhead.

This article tackles the problem of designing efficient binary-level verification for a subset of information flow properties encompassing constant-time and secret-erasure . These properties are crucial for cryptographic implementations but are generally not preserved by compilers. Our proposal builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, Binsec/Rel , for bug-finding and bounded-verification of constant-time and secret-erasure and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach. Using Binsec/Rel , we also automate two prior manual studies on preservation of constant-time and secret-erasure by compilers for a total of 4,148 and 1,156 binaries, respectively. Interestingly, our analysis highlights incorrect usages of volatile data pointer for secret-erasure and shows that scrubbing mechanisms based on volatile function pointers can introduce additional register spilling that might break secret-erasure. We also discovered that gcc -O0 and backend passes of clang introduce violations of constant-time in implementations that were previously deemed secure by a state-of-the-art constant-time verification tool operating at LLVM level, showing the importance of reasoning at binary level.

To protect cryptographic implementations from side-channel vulnerabilities, developers must adopt constant-time programming practices. As these can be error-prone, many side-channel detection tools have been proposed. Despite this, such vulnerabilities are still manually found in cryptographic libraries. While a recent paper by Jancar et al. shows that developers rarely perform side-channel detection, it is unclear if existing detection tools could have found these vulnerabilities in the first place. To answer this question, we surveyed the literature to build a classification of 34 side-channel detection frameworks. The classification we offer compares multiple criteria, including the methods used, the scalability of the analysis or the threat model considered. We then built a unified common benchmark of representative cryptographic operations on a selection of 5 promising detection tools. This benchmark allows us to better compare the capabilities of each tool, and the scalability of their analysis. Additionally, we offer a classification of recently published side-channel vulnerabilities. We then test each of the selected tools on benchmarks reproducing a subset of these vulnerabilities as well as the context in which they appear. We find that existing tools can struggle to find vulnerabilities for a variety of reasons, mainly the lack of support for SIMD instructions, implicit flows, and internal secret generation. Based on our findings, we develop a set of recommendations for the research community and cryptographic library developers, with the goal to improve the effectiveness of side-channel detection tools.

Spectre are microarchitectural attacks which were made public in January 2018.They allow an attacker to recover secrets by exploiting speculations.Detection of Spectre is particularly important for cryptographic libraries and defenses at the software level have been proposed.Yet, defenses correctness and Spectre detection pose challenges due on one hand to the explosion of the exploration space induced by speculative paths, and on the other hand to the introduction of new Spectre vulnerabilities at different compilation stages.We propose an optimization, coined Haunted RelSE, that allows scalable detection of Spectre vulnerabilities at binary level.We prove the optimization semantically correct w.r.t. the more naive explicit speculative exploration approach used in state-of-the-art tools.We implement Haunted RelSE in a symbolic analysis tool, and extensively test it on a wellknown litmus testset for Spectre-PHT, and on a new litmus testset for Spectre-STL, which we propose.Our technique finds more violations and scales better than state-of-the-art techniques and tools, analyzing real-world cryptographic libraries and finding new violations.Thanks to our tool, we discover that indexmasking-a standard defense for Spectre-PHT-and well-known gcc options to compile position independent executables introduce Spectre-STL violations.We propose and verify a correction to index-masking to avoid the problem.

execution.A well-known analysis technique that scales well on binary code is symbolic execution (SE) [4], [5].In order to analyze speculative constant-time, it must be adapted to additionally consider transient execution introduced by the speculative semantics.However, modeling these new behaviors explicitly does not scale because it quickly leads to state explosion.Therefore, the challenge is to optimize this exploration in order to make the analysis applicable to real code.Proposal.In our paper, "Hunting the Haunter-Efficient Relational Symbolic Execution for Spectre with Haunted RelSE" [6], we proposed a novel technique, Haunted RelSE, to model speculative behaviors more efficiently, and detect Spectre-PHT and Spectre-STL vulnerabilities.We implemented it in a new static analyzer for binary-code, called BINSEC/HAUNTED and evaluated it on small examples and on real-world cryptographic code.In summary, we proposed the following contributions:• We design a dedicated technique on top of relational symbolic execution, named Haunted RelSE, which key idea is to model transient and sequential (in order) behavior at the same time; • We propose a verification tool, BINSEC/HAUNTED, implementing Haunted RelSE and perform an experimental evaluation on 1) a well-known litmus tests (small test cases) for Spectre-PHT, 2) a new set of litmus tests for Spectre-STL that we propose, 3) on real-world cryptographic code.We also compare against two state of the art tools, KLEESpectre [7] and Pitchfork [3]; • Finally, we report new Spectre-STL violations concerning index-masking-a countermeasure against Spectre-PHT, and PIC options [8] from the gcc compiler.In this paper, we detail and reflect on the experimental aspects of our work and draw general takeaways.

The constant-time programming discipline (CT) is an efficient countermeasure against timing side-channel attacks, requiring the control flow and the memory accesses to be independent from the secrets. Yet, writing CT code is challenging as it demands to reason about pairs of execution traces (2- hypersafety property) and it is generally not preserved by the compiler, requiring binary-level analysis. Unfortunately, current verification tools for CT either reason at higher level (C or LLVM), or sacrifice bug-finding or bounded-verification, or do not scale. We tackle the problem of designing an efficient binary-level verification tool for CT providing both bug-finding and bounded-verification. The technique builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, Binsec/Rel, and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach in both bug-finding and bounded-verification. Using Binsec/Rel, we also automate a previous manual study of CT preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of CT in implementations that were previously deemed secure by a state-of-the-art CT verification tool operating at LLVM level, showing the importance of reasoning at binary-level.

The reliability of a security protocol is of the utmost importance but can easily be compromised by a vulnerability in the implementation. A crucial aspect of an implementation is the protocol's state machine. The state machine of an implementation can be inferred by black box testing using regular inference. These inferred state machines provide a good insight into implementations and can be used to detect any spurious behavior. We apply this technique to different implementations of OpenVPN: the standard OpenVPN and the OpenVPN-NL implementations. Although OpenVPN is a widely used TLS-based VPN solution, there is no official specification of the protocol, which makes it a particularly interesting target to analyze. We infer state machines of the server-side implementation and focus on particular phases of the protocol. Finally we analyze those state machines, show that they can reveal a lot of information about the implementation which is missing from the documentation, and discuss the possibility to include state machines in a formal specification.

Analyse symbolique de code binaire pour la sécurité. Application à la détection d’attaques microarchitecturales dans les implémentations cryptographiques Les logiciels informatiques manipulent fréquemment des données secrètes, garantissant généralement leur confidentialité à l’aide de programmes cryptographiques. Dans ce contexte, il est crucial de s’assurer que ces programmes cryptographiques ne peuvent être exploités par un attaquant pour en extraire les données secrètes. Malheureusement, même si les algorithmes cryptographiques sont basés sur des fondations mathématiques solides, leur exécution dans le monde physique produit des effets secondaires pouvant être exploités par un attaquant. En particulier, un attaquant peut exploiter le temps d’exécution d’un programme pour inférer des informations sur ses entrées secrètes, ou pour extraire des données secrètes encodées dans la microarchitecture grâce aux attaques microarchitecturales. Plus récemment, les attaques Spectre ont montré qu’il est aussi possible d’exploiter les optimisations des processeurs — en particulier les mécanismes de spéculation — pour extraire des données secrètes.Dans cette thèse, nous développons des outils d’analyse automatique de programme permettant de vérifier la confidentialité des données secrètes dans les logiciels cryptographiques. En particulier, nous ciblons trois propriétés cruciales pour les programmes cryptographiques : (1) secret-erasure, qui s’assure que les données secrètes sont effacées de la mémoire à la fin d’un programme, (2) constant-time, qui protège des attaques microarchitecturales, (3) speculative constant-time, qui protège contre les attaques Spectre. Ces propriétés ont en commun deux caractéristiques qui les rendent difficiles à analyser. Premièrement, il s’agit de propriétés de paires d’exécution (c’est-à-dire de 2-hypersûreté), ce qui les rend incompatibles avec les outils de vérification habituels (conçus pour la sûreté). Deuxièmement, elles ne sont généralement pas préservées par les compilateurs.Dans cette thèse, notre objectif est de concevoir des outils d’analyse symbolique automatiques, modélisant des paires d’exécution, fonctionnant au niveau du code binaire, incluant les mécanismes de spéculation des processeurs, et passant à l’échelle sur des logiciels cryptographiques existants. Nos analyses sont basées sur l’exécution symbolique relationnelle — une adaptation de l’exécution symbolique à la 2-hypersûreté — que nous complétons avec des optimisations permettant de : (1) la rendre efficace au niveau binaire, et (2) de modéliser de manière efficace la sémantique spéculative des programmes. Nous proposons deux outils open source : Binsec/Rel, un outil pour la recherche de bugs et la vérification bornée de constant-time et secret-erasure ; et Binsec/Haunted, un outil pour détecter des vulnérabilités aux attaques Spectre. Notre évaluation expérimentale montre que nos optimisations permettent une amélioration drastique des performances en comparaison aux approches antérieures : elles diminuent le temps d’analyse, trouvent plus de bugs, et permettent la vérification de primitives cryptographiques jusqu’alors hors de portée des approches antérieures.Nous analysons, grâce à nos outils, un large éventail de primitives cryptographiques et de fonctions utilitaires de bibliothèques open source (telles que Libsodium, OpenSSL, BearSSL and HACL*) pour constant-time (338 binaires), secret-erasure (680 binaires), et Spectre (45 binaires). Au cours de ces travaux, nous découvrons quelques bugs nouveaux, ainsi que des faiblesses dans certaines protections logicielles.