- Please fill out the registration form for the tutorials, indicating your preferences.
Here are the currently confirmed tutorial talks!
Lecturers: Benjamin Lipp, Charlie Jacomme
Abstract: Provable security provides the strongest assurance of cryptographic security on the specification level of a cryptosystem. However, writing and verifying proofs is a delicate task. Automated tools can help reduce errors and reviewing load.
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.
Lecturers: Matthias J. Kannwischer, Bo-Yin Yang
Abstract: In this tutorial, we will cover the basics of implementing cryptography on embedded microcontrollers with a focus on the widely used Arm Cortex-M4 microcontroller.
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.
Lecturers: Ján Jančár, Łukasz Chmielewski
Abstract: This tutorial covers the topic of the side-channel analysis (SCA) on implementations of one of the most commonly-used nowadays digital signature schemes, namely, Elliptic Curve Digital Signature Algorithm (ECDSA), which is used in the TLS protocol, document signing, and blockchain applications (e.g., the Bitcoin protocol), among others. Since the tutorial is hands-on we provide the participants with exercises, including a side-channel attack on ECDSA running on a simple embedded target.
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.
Lecturer: Ileana Buhan
Abstract: While the current standard cryptographic algorithms are secure against known mathematical attacks, practice shows that hardware and software implementations are susceptible to physical attacks. A significant number of studies show how to recover secrets by monitoring the algorithm's execution using side channel attacks.
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/.
Lecturer: Patrick Schaumont
Abstract: Hardware design is increasingly embracing open-source practices, a trend as significant for hardware as the open-source movement has been for software. Open-source plays a crucial role in the cryptographic field, where it is used in cryptographic standard development and for secure connectivity through standard libraries. Open-source electronic design automation (EDA) tools now cover all aspects of Application-Specific Integrated Circuit (ASIC) design, from design capture to tape-out. Additionally, open-source libraries and process design kits (PDKs) offer a fully open-source option for prototyping chips.
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:
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.
Lecturer: Nader Sehatbakhsh
Abstract: Privacy-preserving methods, ranging from complex encryption-based methods to pure encoding techniques have gained significant popularity in recent years. The goal of this tutorial is to explore state-of-the-art methods for privacy-preserving machine learning. This is achieved by first providing a brief background on existing methods and then reviewing the state-of-the-art for each method. To further explore the existing solutions, we then systematically compare them using different important metrics such as privacy and accuracy. A particular focus will be put on the applicability of these techniques to resource-constrained IoT devices by analyzing various additional metrics such as power and memory overhead incurred on an IoT device to achieve privacy.
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.
Lecturer: Ahmad-Reza Sadeghi
Abstract: The widespread and increasing deployment of Artificial Intelligence (AI), also enlarges the attack surface and requires new security and privacy-enhancing methodologies and technologies. One approach that has been gaining significant growth in recent years is Federated Learning (FL), which enables multiple parties to collaborate in training a neural network model while maintaining the privacy of their individual data.
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.
Lecturers: Cas Cremers, David Basin
Abstract: The Tamarin prover is a state-of-the-art automated security protocol analysis tool that can be used to prove protocol properties and also automatically find attacks. Tamarin has been successfully used to analyze multiple versions of TLS 1.3, the mobile communication standard 5G, group key agreement protocols, the EMV chip-and-pin standard, as well as many other protocols, leading to the discovery of subtle attacks and/or automated proofs.
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.
Here are the currently confirmed lecturers!