Tutorials - Crypto Summer School 2024

Summer School Tutorials

Tutorial Talks

Here are the currently confirmed tutorial talks!

Hands-on introductory tutorial on hardware accelerated machine learning for network intrusion detection
Lecturers: Nele Mentens, Wouter Hellemans, Jelle Biesmans
Abstract: In today’s interconnected world, network security remains vital. One essential component therein is network intrusion detection, where some intrusion detection system (IDS) inspects network traffic to detect anomalies. In this session, we investigate how convolutional neural networks (CNN) can be used to construct IDSs that can be accelerated on Field-Programmable Gate Arrays (FPGA) for high- throughput applications. For this purpose we use Brevitas and FINN, two free and open source frameworks developed by AMD Xilinx to quantize neural networks and then translate them to High-Level Synthesis (HLS), which in turn can be used to generate specialized hardware.

After introducing the problem setting and corresponding network traffic dataset, we guide the participants through all the steps required to generate high-performance hardware. At each step, we stop to investigate how design choices might impact security and performance, and discuss how to reach the optimal solution.

Reverse Engineer ECC implementations Using Side-Channel Analysis
Lecturers: Ján Jančár, Łukasz Chmielewski
Abstract: SCA is a relatively new research area in applied cryptography that has continuously gained prominence since the late nineties. In SCA, attackers closely monitor 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.

In particular, side-channel attacks on Elliptic Curve Cryptography 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 multipliers, 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 a real-world attacker that usually only has black-box access to the target - i.e., has 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, as evidenced by [1] and [2].

This tutorial covers the topic of reverse-engineering, using the side-channel analysis (SCA), implementations of ECC, 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, the participants will perform exercises, including reverse-engineering well-known implementations running on a simple embedded target. 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. The demo, examples, and exercises utilize two open-source libraries micro-ecc and sca25519. We will also discuss other most commonly used open- source ECC libraries, which show a surprisingly wide variety of implementation details.

The main goal of the tutorial is to introduce to the audience the most common ECC implementation approaches and side-channel techniques to learn 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 functionality of the device. For majority of the practical exercises we will be using Python Elliptic Curve cryptography Side-Channel Analysis toolkit (pyecsca).

References

[1] J. Jancar, V. Sedlacek, P. Svenda a M. Sys, „Minerva: the curse of ECDSA nonces,“ IACR TCHES, p. 281–308, 2020. URL: https://tches.iacr.org/index.php/TCHES/article/view/8684
[2] T. Roche, V. Lomné, C. Mutschler a L. Imbert, „A side journey to Titan.,“ USENIX Security, p. 231–248, 2021. URL: https://www.usenix.org/conference/usenixsecurity21/presentation/roche

Cryptographic Hardware Optimization for ASIC
Lecturer: Patrick Schaumont
Abstract: Cryptographic hardware are specialized computation structures dedicated to the execution of a single or a few cryptographic algorithms. Through specialization, hardware achieves higher performance, lower power consumption, and lower silicon cost compared to equivalent cryptographic software implementations. The difference in efficiency can be orders of magnitude. Yet, while the performance benefits of hardware are well understood, the cryptographic engineering community is generally unfamiliar with the process of mapping algorithms to hardware structures. For example, reference implementations of new cryptographic standards are more commonly found in software than in hardware. With the advent of open source hardware design tools, and especially open-source ASIC design tools, a great opportunity exists for a culture of hardware engineering in the cryptographic community. The potential gains of cryptographic implementations in efficiency, in scope, and in innovation are simply too big to ignore the hardware design domain.
The objective of this tutorial is to introduce a standard open-source ASIC design flow using cryptographic hardware design examples. Tutorial attendees will learn specifically about techniques for high performance, and techniques for low area. In each case, attendees will target the OpenROAD ASIC design flow for Google Skywater 130nm standard cells.

In this design process, the attendees will learn how to analyze the tool output, and how to make meaningful design decisions towards high performance or low area in hardware.
- 1/ Transform a C reference implementation to RTL hardware, without the magic of a compiler or a high-level synthesis tool.
- 2/ Understand common RTL design transformations for high performance in hardware: pipelining, unfolding, and retiming
- 3/ Understand common RTL design transformations for low area in hardware: multiplexing and bitserial design.

Cryptographic Vulnerabilities and How To Find Them
Lecturers: Kien Tuong Truong, Mia Filić
Abstract: Cryptography is notoriously hard to get right in practice. Creating a secure cryptographic protocol is a non-trivial task that, as in the case of TLS 1.3, can take many years of design iteration on the part of a large group of experts to get right. In an ideal world, formal analysis techniques would be used to analyze protocol specifications before developers start work on implementing them. Meanwhile, in the real world, complex systems using cryptography frequently get developed and rolled out without even having a specification, never mind any kind of formal verification having been done on them. This leads to many such systems containing severe cryptographic flaws, as recent analyses of systems like MEGA, Matrix, Bridgefy and Threema have demonstrated. How can such flaws be identified and exploited?

In this tutorial, we offer a hands-on experience in analyzing cryptographic code from an adversarial perspective. Participants will be given code inspired by our experience in finding vulnerabilities in cryptography deployed “in the wild”, and they will try to first find the vulnerabilities and then figure out how to exploit them. The difficulty will steadily increase to ensure that both beginners and more experienced people will enjoy the tutorial. Excited about trying to spot a Bleichenbacher oracle in the wild? Want to understand how the CRIME attack really works? Then, this is the tutorial for you!

The tutorial will be structured similarly to a Capture the Flag (CTF) competition but with a lighter focus on the competition side and some additional twists. Each vulnerable service will contain a secret string called a “flag”, which the participants can submit to our website in exchange for points. For the more competitive players, a leaderboard will be available so they can try to achieve the maximum amount of points in the shortest amount of time.

We do not require experience with any particular programming language, though previous exposure to Python would be beneficial. We will be using various tools, frameworks and programming languages, so the only thing required is being flexible and willing to learn something new.

The Hitchhiker’s Guide to the Security and Privacy of Federated Learning
Lecturer: Ahmad-Reza Sadeghi, Alessandro Pegoraro, Phillip Rieger
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. Instead of sharing their individual data, each participant trains its own neural network locally and shares only the parameter of the trained model, allowing the participants to maintain the privacy of their private datasets.

The tutorial is centered around the privacy and security threats in federated learning systems, with more focus on security attacks. These security attacks fall into two main categories, targeted and untargeted attacks. Targeted (backdoor) poisoning attacks involve the insertion of a backdoor trigger into the global model that prompts a hidden malicious behavior that would otherwise be concealed when normal inputs are used. On the other hand, untargeted attacks aim to impede the convergence of the aggregated model and reduce its utility (i.e., accuracy). The primary objective of this tutorial is to investigate various types of poisoning attacks and defense solutions that can be employed to mitigate their impact.

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

Tamarin Prover Tutorial
Lecturers: Aurora Naska, Sofia Giampietro
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 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 https://tamarin-prover.com/ . For some examples of its real-world use, see this article: https://hal.archives-ouvertes.fr/hal-03586826/document.

Implementing cutting-edge isogeny-based cryptography for beginners
Lecturers: Lorenz Panny, Krijn Reijnders
Abstract: In this tutorial, we will teach you everything you need to know about elliptic curves and isogenies. You will go from ignoramus to isogenist in three easy steps!
- 1. Curves: The first step are elliptic curves: We explain the basics of elliptic-curve arithmetic for Montgomery curves, which you will then implement by yourself.
- 2. Isogenies: The second step are isogenies: “nice” maps between elliptic curves. We explain how such maps are used and computed, so that you can implement isogeny arithmetic using your own elliptic-curve implementation.
- 3. SQIsign: We are then ready for the final step: SQIsign verification. This uses the tools built in the two steps above in a specific way. We will detail this verification minutely, so that you’ll be able to implement it without spending years on reading papers first.
An optional side quest is a competition: Who can build the fastest SQIsign verification using their own curve and isogeny implementation? Students are encouraged to look at the existing literature to improve their implementations of curves, isogenies, and SQIsign verification beyond the bare minimum as taught in the tutorial.

The default choice of programming language will be Python, but you are free to use whatever you want — just be aware that we won’t be able to help with all languages. We provide materials for Python and Rust, so you might have to work more independently if you use another language.

Design and Verification of Side-Channel Resistant Implementations
Lecturers: 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 both masking and 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 second 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 a small S-box (e.g., the Ascon S-box) and subsequently verifying it with Coco. Here, we show off all the steps of the design and verification process. Afterwards, the attendees should be comfortable with the practical aspects of masking, as well as its verification through Coco.