CHES 2024

Time:

9:00 — 12:30, Wednesday, September 4, 2024

Location:

Ballroom Level — 503

Speaker:

Miguel Quaresma

Abstract:

Jasmin is a programming language designed to implement low-level, high-speed, high-assurance cryptography. It provides a high degree of control over the generated assembly, allowing fine-grained optimization while still being suitable for verification and automatic analysis. It supports different target architectures, such as x86_64 and ARMVv7 (experimental), with ongoing work focused on adding support for more architectures.

Several cryptographic primitives, such as SHA3, poly1305, chacha20, salsa20, Kyber512, and Kyber768, have been implemented using Jasmin. By using the Jasmin compiler to extract EasyCrypt models of these implementations, we can formally prove security and functional correctness of the very assembly that gets executed. The Jasmin compiler includes several features that aid in developing secure cryptographic code by avoiding common pitfalls. For example, it includes a safety checker to ensure that array accesses are in bounds and that there are no divisions by zero. Additionally, it provides a cryptographic constant time checker that calculates the timing side-channel leakage of a program, even under speculative execution. Furthermore, if a program is constant time at the source (Jasmin) level, the compiler is proven not to apply any optimizations or modifications that would introduce timing side-channels. The compiler is formally verified in Coq, which means that the functional correctness properties of Jasmin programs also hold in the assembly. This tutorial will give an overview of the Jasmin environment: how the language, compiler, EasyCrypt proof assistant, and the safety and CCT checkers work together and what guarantees they provide.

To do this, we will go through examples to see how:

• the abstractions in Jasmin provide flexibility and structure to assembly programming;
• the low-level aspects of Jasmin ensure we don’t compromise on efficiency or security;
• the safety checker ensures memory safety and the absence of arithmetic errors automatically, and the compiler preserves these properties;
• the constant time checker extracts the side-channel leakage of a program, using different models of leakage (just branches, cache, operators) and execution (sequential and different variants of speculation);
• Jasmin allows applying low-level mitigations such as Selective Speculative Load Hardening cohesively and in a principled manner;
• EasyCrypt relates implementations with their abstract mathematic specifications and can check proofs of arbitrary security properties. We conclude by briefly examining Libjade, a library of cryptographic primitives written in Jasmin. Libjade contains reference and vectorized (i.e., AVX2) implementations of several cryptographic primitives.

Requirements/Prerequisites:

Attendees are expected to be familiar with the C programming language.

Additionally, in order to speed up the setup process, Docker should be installed prior to the tutorial¹ and the following (Docker) image pulled: miguelmirq/jasmin101.

¹ On ARM-based Macbooks, make sure the following options are set in the Docker settings:

• General → Use Virtualization Framework
• General → VirtioFS
• General → Use Rosetta for x86/amd64 emulation on Apple Silicon

Time:

13:30 — 17:00, Wednesday, September 4, 2024

Location:

Argyle Level — A2

Speaker:

Shahin Tajik

Abstract:

The security of ICs can be compromised by adversaries, who can gain access to these devices and mount physical attacks, such as side-channel analysis (SCA), which exploit leakages relevant to the physical characteristics of cryptographic implementations. Such leakages exist due to the inevitable impact of computation and storage on the power consumption or voltage drop on a chip. These data-dependent fluctuations reveal themselves through various measurable quantities, such as power consumption, electromagnetic emanation, acoustic waves, photon emission, and thermal radiation. Over the past decades, these quantities have been exploited in different classes of SCA attacks to compromise the security of various cryptographic implementations. At the same time, different countermeasures have been developed to defeat these passive side-channel attacks, which have proven to be effective to a certain extent. However, the physical realization of security-enabled systems is still vulnerable to a novel class of physical side-channels known as active sensing or backscattered SCAs. These techniques are known in the fields of power/signal integrity (PI/SI), electromagnetic compatibility (EMC), and failure analysis (FA). In such attacks, the adversary stimulates the target device using signals in various forms, e.g., microwave radiations, near-infrared laser beams, or even electron beams and measures the reflected/scattered signals, see Fig. 1. The state of a circuit or memory contents affects the system's physical characteristics (e.g., die's impedance, absorption coefficient and refractive index of transistors' material, etc.). Thus, the scattered signal is modulated and can be exploited by the attacker to extract secret information from the chip. Due to the higher level of signal-to-noise ratio (SNR) and spatial precisions, such attacks enable the adversary to probe and extract static signals and bits of information from the chip and render the masking countermeasures ineffective.

On the positive side, these powerful side-channel methods have enabled high-confidence detection solutions for supply chain threats (e.g., tampering and hardware Trojan insertion) at various physical levels of the system (i.e., chip, package, and PCB), which has been challenging using conventional passive side-channels. Moreover, using the concepts known from PI, SI, EMC, and FA, novel anti-tamper methods (e.g., based on impedance sensing, optical sensing, etc.) have been developed to prevent, detect, and respond to physical attacks.

In this tutorial, we cover the following:

• An introduction to active sensing/backscattering measurement methods known in fields of PI, SI, EMC, and FA;
• a taxonomy of state-of-the-art side-channel attacks and verification methods based on these techniques (e.g., impedance analysis, optical probing, e-beam probing, etc.);
• the main requirements and steps to perform these side-channels on modern systems;
• a comparison with conventional passive side-channels in terms of resolution, SNR, cost and time
• potential prevention-based countermeasures;
• potential detection-based countermeasures;
• potential responses to the backscattered attacks,
• a summary of open problems and future research directions.

This tutorial, for the first time, systematizes the knowledge of the reported results on various backscattered side-channels in several papers published at high-tier security conferences in the last five years.

Time:

13:30 — 17:00, Wednesday, September 4, 2024

Location:

Argyle Level — A3

Speakers:

Łukasz Chmielewski and Ján Jančár

Abstract:

Nowadays, Side Channel Analysis (SCA) is one of the biggest threats against cryptosystems embedded in embedded devices such as smart cards. Moreover, research into SCA is particularly interesting since it poses a unique challenge as an intersection of cryptography, electronics, and statistics and affects all aspects of modern hardware security. In particular, side-channel attacks on Elliptic Curve Cryptography (ECC) implementations often assume a white-box attacker with detailed knowledge of the target implementation details. However, due to the complex and layered nature of ECC, there are many implementation choices that a developer makes to obtain a functional and interoperable implementation. These include the curve model, coordinate system, addition formulas, scalar mult ipliers, or lower-level details such as the finite-field multiplication algorithm. Moreover, the complexity further rises due to the application of various side-channel and fault-injection countermeasures. This situation creates a gap between the white-box attackers (often considered in academic and commercial evaluation contexts) and real-world attackers that usually only have black-box access to the target — i.e., have no access to the source code nor specific implementation choices used. Yet, when the gap is closed, even real-world implementations of ECC succumb to side-channel attacks.

This tutorial covers the topic of side-channel-based reverse-engineering of ECC implementations, which are used in real-world applications, such as TLS or blockchain applications, among others. Since the tutorial is hands-on, the participants will perform exercises, including reverse-engineering well-known implementations. In particular, we show how to infer details about ECC implementations, most notably the scalar multiplier, both from the general characteristic of power traces but also using more sophisticated methods, utilizing attack-based, structural, and behavioral characteristics. We will discuss various commonly used open-source ECC libraries, which show a surprisingly wide variety of implementation choices. The main goal of the tutorial is to introduce to the audience the most common ECC implementation approaches and side-channel techniques to reverse-engineer them. We concentrate on so-called passive SCA, i.e., we assume that the attacker only monitors the side channels and does not attempt to affect the device's functionality. For the majority of the practical exercises, we will be using the Python Elliptic Curve cryptography Side-Channel Analysis toolkit (pyecsca).

Requirements/Prerequisites:

To ensure a smooth tutorial please prepare your setup ahead of time. Please follow the instructions found in the repository, also consult the troubleshooting file in case of issues, and do not hesitate to contact us.

Time:

9:00 — 12:30, Wednesday, September 4, 2024

Location:

Argyle Level — A2

Speaker:

Gaëtan Cassiers

Abstract:

Side-channel security evaluations often involve complicated workflows and be computationally- intensive, in particular when protected implementations are considered. While some of this complexity is sometimes unavoidable, we will show that getting started with side-channel security evaluations can also be pretty simple and fast. In this tutorial, we analyze the security of a masked implementation. Starting from the power leakage traces collected by ANSSI (the ASCAD dataset), we will show how to implement a very powerful attack, leading to key recovery in a single trace. The implementation of the attack will be based on the speaker’s SCALib library, which provides optimized implementations of common algorithms for side-channel analysis. Its simple interfaces enable the implementation the full attack in a few lines of python code, while running in a few minutes on a laptop.

Concretely, the goal of the tutorial is to implement an attack using SCALib and evaluate it, in a worst-case security setting. That is, we assume that the evaluator as extensive knowledge of the implementation and has complete access to a sample device to profile the leakage, including knowledge of the masks used. The attack will be implemented end-to-end, from the selection of the points-of-interest (POIs) for the leakage, to the computation of the correct key rank after the attack. The attack is based on the profiling of many intermediate variables in the computation, using the signal-to-noise ratio (SNR) to select the POIs and linear discriminant analysis (LDA) to infer posterior distributions for the targeted values. The information on all the intermediate values is then combined to infer the key, using a soft analytical side-channel attack (SASCA). This step produces a probability distribution for each of the key bytes, from which a key enumeration can be attempted. In an evaluation context, we propose instead to use a key rank estimation algorithm, which sidesteps the computationally expensive enumeration and provides an equivalent result for the evaluator. The tutorial will discuss the methods and metrics for the selection of the hyperparameters in the method. A well-tuned attack is able to recover the key in a single trace with a high success rate. Finally, we will discuss leakage assessment with the TVLA methodology, including higher-order and multivariate tests. The tutorial will alternate short talks explaining the working principles of the attack steps and hands-on sessions for the implementation of these attack by the participants. The tutorial will be concluded by a discussion of the links between the tutorial’s attack and the state of the art, as well as a brief summary of the various open-source side-channel evaluation libraries.

Requirements/Prerequisites:

Attendees are expected to have basic knowledge of the python programming language.

Additionally, in order to speed up the setup process, JupyterLab should be installed prior to the tutorial and the side-channel traces file should be downloaded from here.

It will also be possible to run the code online through Google colab (requires a Google account), but it is not the recommended solution.

Time:

9:00 — 12:30, Wednesday, September 4, 2024

Location:

Argyle Level — A3

Speaker:

Vedad Hadži

Abstract:

Embedded devices often work with security-critical data while simultaneously being exposed to uncontrolled environments, making them the prime target for physical side-channel attacks such as differential power analysis. The most reliable and theoretically sound countermeasure against such attacks is masking, where secrets and data processed by the device are split into multiple random shares, all of which are necessary to recover the original. Although the idea of masking is simple, implementing it properly in either hardware or software is challenging and littered with pitfalls. Moreover, practically evaluating the security of masked designs is time-consuming and requires elaborate measurement setups. However, formal verification of masked designs has recently gained traction because it provides formal guarantees of side-channel security and simultaneously speeds up the iterative process of designing secure implementations. This tutorial aims to familiarize the audience with practical masking and especially its formal verification through dedicated tools. We first give a short overview of masking and how it works, as well as several masking schemes such as DOM (domain-oriented masking), TI (threshold implementation) and HPC (hardware private circuits). Similarly, we present the security notions masked implementations strive to achieve and give the formal definitions of probing security and probe-isolating non-interference. Afterwards, the attendees should have an intuition of how to use the provided building blocks and successfully mask the hardware implementation of small S-boxes.

In the main part of the tutorial, we introduce the masking verification tool called Coco, which can verify that a design is indeed secure according to a given security notion. We first give a brief overview of Coco’s workflow and explain the individual components necessary for running the tool. Next, we give an interactive demonstration of designing and formally verifying a masked design with the help of Coco. The attendees are expected to follow along with the presenter in applying masking to small S-boxes (e.g., the Ascon S-box or the PRESENT S-box) and subsequently verifying them with Coco. Here, we show off all the steps of the design and verification process. Importantly, the participants will encounter some of the common pitfalls when implementing masked designs, and Coco will tell them what went wrong and where. The provided debug information is then leveraged to fix the mistakes and quickly iterate the design process. Afterwards, the attendees should be comfortable with the practical aspects of masking, and especially its formal verification through tools like Coco. The takeaway should be that getting masking right immediately is not what usually happens, and that formal verification tools greatly speed up the iteration process, while also giving the designer confidence that the design will likely also pass a costly practical evaluation.