Summer School Tutorials

CryptoVerif is a proof assistant for game-based cryptographic proofs used for analyses in the asymptotic and the concrete security framework. It formalizes code-based proofs by sequences of games (“game hopping”), and has a high degree of automation which allows treating complex protocols. The tool has been used to write proofs for SSH, TLS, the Signal protocol, the WireGuard VPN protocol, and during the development of the HPKE standard.

CryptoVerif only requires users to specify the initial game and the proof goals (secrecy, authentication, or indistinguishability) and will then try to carry out the proof automatically through its built-in strategy. Users can alternatively guide the proof by manually specifying some proof steps. The tool comes with a predefined set of cryptographic assumptions, and users can also specify their own using CryptoVerif’s input language.

This tutorial will teach participants to read and understand the security notions expressed in most existing CryptoVerif models. We will guide them through multiple examples, first covering some classical cryptographic assumptions (DDH, ROM, EUF-CMA) applied to constructions like Encrypt-Then-Mac, and then looking at small protocols like a signed Diffie-Hellman key exchange. The tutorial will include a gentle reintroduction to provable security and game-based/code-based/game hopping proofs. Participants should bring a laptop.

The Arm Cortex-M4 presents an interesting target for a tutorial not only due to the vast number of deployed chips, but also because it is powerful enough to run the majority of cryptography (including most post-quantum cryptography), but simple enough to allow understanding the performance impact of each instruction. Additionally, the Cortex-M4 is the default microcontroller target for the NIST PQC competition resulting in a vast number of open-source Cortex-M4 implementations and literature.

The tutorial starts from scratch introducing the Armv7E-M instruction-set architecture and the basics of getting software to run on a Cortex-M4 board. Students will learn how to write constant-time implementations on the Cortex-M4 and the pitfalls to avoid. It then covers the state-of-the-art tricks for speeding up cryptography including pre-quantum schemes (focussing on Chacha20) and post-quantum schemes (mostly Kyber and Dilithium). It will include examples that show how features of the Arm Cortex-M4 like the barrel-shifter and conditional execution can be used to make cryptography fast and constant time. Additionally, students will learn about word-sized modular arithmetic using Barrett, Montgomery, and Plantard multiplication. At the end of the tutorial, students should be able to write, test, debug, and benchmark their own implementations of cryptographic schemes and reason about their performance. Additionally, students will be able to judge the quality of implementations of any of the covered schemes.

In the practical parts of this tutorial, participants will be able to get some hands-on experience implementing cryptography on the Arm Cortex-M4. The assignment will cover the stream cipher Chacha20, (parts of) the post-quantum key-encapsulation mechanism Kyber, and parts of the post-quantum signature scheme Dilithium. Participants will be provided with Cortex-M4 development boards (to be returned after the tutorial) allowing them to develop, test, and benchmark their own implementations. Additionally, we will provide a framework that allows testing using qemu.

While ECDSA is very popular, one of its main pitfalls is that it requires a unique, fully random, nonce per signed message. Its fragility with regard to this requirement about nonces is well-known. Any reuse of the nonce for a different message trivially leads to key recovery, as was the case in the PlayStation 3 game console, which utilized a fixed value for signing its binaries. While nonce reuse problems are, to a large extent, mitigated by using deterministic nonce generation (as in EdDSA, for example), other potential issues can prove fatal. Knowing the nonce used for a single known message - or being able to brute-force it, as was the case for the Chromebook H1 chip used for U2F authentication - leads to private key recovery as well. Even worse, ECDSA features a linear relation between the nonce and the private key, and therefore, even partial information about the random nonces (such as knowledge of certain bits) might be sufficient to recover the private key, often via the use of lattice reduction techniques. The partial information can originate from implementation issues (such as a faulty random number generator, for example), or it might be observed via SCA.

SCA is a relatively new research area in applied cryptography that has continuously gained prominence since the late nineties. In SCA, attackers closely monitor so-called side channels, like the power consumption or electromagnetic emission, of a cryptographic device, and they are able to extract the secret key using statistical techniques. This field is particularly interesting since SCA poses a unique challenge as an intersection of cryptography, electronics, and statistics and affects all aspects of modern hardware security. The goal of the tutorial is to present to the audience the most common side-channel techniques that can break ECDSA security. 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 functionality of the device by affecting the power consumption.

In the first theoretical part of the tutorial, we introduce how Elliptic Curve Cryptography works and which assumptions need to be fulfilled for the ECDSA to be secure. Then we describe how classical side-channel attacks (for example, Simple Power Analysis and Correlation Power Analysis) work against ECDSA. In particular, we describe attacks that exploit nonce reuse, nonce bias, nonce bit-length leak, and recent real-world attacks like Minerva and TPM-FAIL. We also explain the limitations of the presented attacks and possible countermeasures. All concepts are given in a historical context and illustrated by practical examples.

In the second practical part of the tutorial, we give practical exercises to be executed by the participants. In particular, the participants will execute nonce reuse and nonce bit-length leak attacks. The exercises involve combining a simple power analysis on an unprotected ECDSA implementation with lattice-based techniques.

Ensuring the security of modern cryptographic implementations is challenging due to their complexity, aggressive time-to-market demands, and the variety of known attacks. Leakage assessment seeks evidence of sensitive data dependencies (leaks) in the traces measured from the physical device. Detecting side-channel leaks is of considerable interest to developers of secure cryptographic implementations and several methods such as correlation analysis, F-statistics or mutual information have gained popularity. Among these, Test Vector Leakage Assessment (TVLA) is one of the most popular methods for leakage assessment due to its simplicity and relative effectiveness. Based on hypothesis testing it is the most common nonspecific test. However, ensuring a meaningful interpretation or drawing appropriate conclusions of the test outcome is less intuitive.

The goal of this tutorial is to give participants a solid technical understanding of what hypothesis testing is and how it is used for leakage assessment. Participants will perform hands-on leakage detection tests and draw appropriate conclusions from the data. We will discuss common pitfalls and strategies such as bootstrapping to improve the accuracy of our results and unravel the mystery of the magic number of 4.5 and learn how to interpret p-values. The tutorial is rich in hands-on exercises via interactive Jupiter notebooks and data sets. We start with some simple examples using simulated data such that participants grasp the mechanics of hypothesis testing and move from there to real power traces. As an example of the type of materials presented in the tutorial, participants can check some of the blog posts available at https://ileanabuhan.github.io/.

The aim of this tutorial is to introduce a fully open-source ASIC design flow using cryptographic hardware design examples. Tutorial attendees will learn about and gain hands-on experience with the following hardware design concepts:

• Open-source Hardware Description Languages.
• Open-source Hardware Target Technologies, including standard cells and module generators.
• Open-source Logic Synthesis and Optimization of Timing and Area.
• Open-source Backend Design Flow and Place-and-Route.
• Open-source Hardware Security Analysis Tools.

Attendees should have a good understanding of hardware design concepts, such as register-transfer level hardware description and synchronous logic design. The ideal candidate would have some experience with Field Programmable Gate Array Design and/or have taken an undergraduate-level course in logic design. During the hands-on part, attendees will have access to a design server in the cloud and will receive instructions to replicate the setup on their home machine.

Using hands-on experiments on real-world datasets and deep neural networks, we further study different privacy-preserving methods in more detail. Particularly, we focus on various privacy-preserving techniques including (fully) homomorphic encryption, multi-party computing, hardware-based methods based on trusted execution environments (TEE), and methods based on encoding such as adversarial representation learning (ARL). We conclude the tutorial by summarizing various existing tradeoffs for achieving privacy on machine learning applications in IoT devices and explore different potential solutions to further improve the state-of-the-art. A link to a GitHub repository (a Jupyter notebook) will be provided for experiments. The tutorial is based on our upcoming Mobicomm 2023 paper.

The tutorial is centered around the examination of privacy and security threats in federated learning systems, with more focus on security attacks which fall into two main categories, targeted and untargeted attacks. Targeted (backdoor) poisoning attacks involve the insertion of a backdoor trigger into the global model through the inclusion of malicious data in local datasets or manipulation of training process hyperparameters, should the adversary possess control over malicious clients. On the other hand, untargeted attacks aim to impede the convergence of the global model. The primary objective of this tutorial is to investigate various types of backdoor attacks and the defense solutions that can be employed to mitigate their impact.

The tutorial is accompanied by a practical hands-on exercises where the participants learn how to launch backdoor attacks and implement a defense mechanism that are sufficiently robust and resilient to security attacks that compromise the integrity of the FL model.

Tamarin uses multiset rewriting to specify the protocol to be analyzed and uses a subset of first order logic to specify properties. It supports not only trace properties but also observational equivalence. We have taught classes to master and Ph.D. level students who were then able to complete projects based on analyzing passport authentication (PACE) and key agreement (SIGMA). In this tutorial we will explain the underlying principles, motivate the design choices, and show how to use the tool. Tamarin is open-source software and further information, including the manual, the source code, and scientific papers are available at tamarin-prover.github.io. For some examples of its real-world use, see this article.