Summer School Tutorials

• Firmware development on an IBEX (RISC-V) open-source processor and functional verification using cycle-accurate simulation.
• Design, functional verification, and performance evaluation of memory-mapped accelerators for cryptography.
• Design, functional verification, and performance evaluation of instruction-set extensions for cryptography.
• Evaluation of the hardware design cost and performance of accelerators based on the OpenROAD ASIC design flow and open-source PDK.

Attendees should have a working knowledge of hardware design including register-transfer level hardware description and synchronous logic design. The ideal candidate would have taken an undergraduate-level course in logic design as well as in embedded software (firmware and bare-metal) programming.

Attendees do not need to have previous experience with ASIC design. Most of the design code will be provided, and the assignments will be of the form ’Analyze what happens if you change X to Y and run the tools again’.

Despite its advantages, SL introduces challenges for security. One of them is poisoning attack, where malicious clients manipulate the training process to compromise the model. Poisoning attacks, also called backdoor attacks, embeds hidden triggers that activate malicious behavior while keeping the model's performance on regular inputs intact. Unlike Federated Learning, where model updates from each client can be analyzed, in SL the server can only partially observe the model, limiting its ability to detect poisoned training contributions.

This tutorial provides an introduction to the privacy and security challenges of SL, with a focus on security threats. In multiple hands-on exercises, participants will first set up an SL scenario before iteratively implementing attacks and corresponding defense mechanisms. This practical tutorial will offer insights into the unique challenges of mitigating poisoning attacks in SL. Participants will learn to execute backdoor attacks and develop defense strategies that enhance the robustness and resilience of SL models against security threats.

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 nonspecic 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. A rst version of this tutorial was given at Summer School on real-world in 2023, and the material is available here: https://ileanabuhan.github.io/leakage/assessment/2023/06/14/Hypothesis_testing_SCA.html. In this second version of the tutorial, we have more diverse trace sets and we clarify additional fundamental concepts such as: effect size and power of a test.

The participants of the tutorial will get an initiation into this broad area of research, by looking into both the modeling and solving phase and focusing on systems of equations over finite fields (as is almost always the case in cryptography). We first give a survey of the state-of-the-art algorithms for tackling this problem. We start with algorithms that rely heavily on enumeration and are thus suitable for small finite fields. Then, we continue with Gr¨obner-based algorithms that can also tackle big fields. We connect these two ends by looking at hybrid systems and ending with the current record-setter for small fields – the Crossbred algorithm. We also mention examples of cryptographic systems when the best known attacks are indeed algebraic attacks.

Our main goal is that all participants of the tutorial leave with a global view of the different algorithms and the core ideas behind them, but also with scripts developed in SageMath that allow us to:

• 1. Ask the machine to output a system of equations that corresponds to a description of the problem using symbolic variables. This can be seen as implementing the modeling phase in a semi-automated way;
• 2. Execute one of the state-of-the-art algebraic solvers with our input system and obtain a solution (and running times);
• 3. Derive the complexity of the solving algorithm in the case of random (unstructured) systems.

These three programs form a practical toolbox for anyone whose primary research is not in the field of algebraic cryptanalysis, but is often confronted with the problem of solving such systems and deriving the resulting complexity. This includes designers of cryptographic schemes that need to make an initial assessment of the resistance of their scheme against direct algebraic attacks, or cryptanalysts that focus on different approaches but need to compare their algorithms against existing algebraic attacks as well. In addition to developing this handy toolbox, the participants will be offered a choice of four modeling exercises. Finding an efficient modeling for a problem is a skill that is developed through experience, and the participants of the tutorial will gain an initial intuition by solving one of the exercises during the tutorial session. After the tutorial, they can continue to develop this skill and strengthen their intuition by solving the other exercises.

While circuit-level HRE starts with extracting the gate-level netlist from a target device, this hands-on tutorial will mainly cover the subsequent “sense-making” steps operating on the netlist itself. The tutorial demonstrates a typical gate-level netlist analysis workflow using our open-source framework HAL [1]. Together, we explore how to identify functional modules such as registers in order to analyze the hardware implementation of a modern block cipher. To this end, we will identify a malicious sub-circuit leaking the secret key of the cipher using both static and dynamic reverse engineering techniques developed in the context of our IACR CHES 2020 [2] and ACM CCS 2024 [3] publications. If time permits, we will demo additional features and plugins of HAL such as HAWKEYE [4], a tool to automatically locate symmetric ciphers in gate-level netlists.

Participants are required to bring their own laptop running Ubuntu 22.04 or newer (natively or within a VM). Installation instruction for HAL will be provided. Basic skills in Python programming are required and some understanding of (symmetric) cryptography and digital circuits would be nice to have.

• [1] https://github.com/emsec/hal
• [2] N. Albartus et al., “DANA - Universal Dataflow Analysis for Gate-Level Netlist Reverse Engineering”, IACR CHES 2020, URL: https://eprint.iacr.org/2020/751.pdf
• [3] S. Klix et al., “Stealing Maggie's Secrets - On the Challenges of IP Theft Through FPGA Reverse Engineering”, ACM CCS 2024, URL: https://dl.acm.org/doi/pdf/10.1145/3658644.3690235
• [4] G. Leander et al., “HAWKEYE – Recovering Symmetric Cryptography From Hardware Circuits”, IACR Crypto 2024, URL: https://eprint.iacr.org/2024/860.pdf

ProVerif is one of these state-of-the-art tools for verifying cryptographic protocols within symbolic models. It takes as input a protocol described in a small specialised language (a variant of the applied pi-calculus), the specification of cryptographic primitives written as rewrite rules or equations, and the properties to prove. For each property, ProVerif either proves the property, finds an attack, or returns an “I don’t know” result. This outcome is inevitable in some cases because ProVerif handles an unbounded number of protocol executions (even in parallel) and an unbounded message space, making protocol verification an undecidable problem. Despite this limitation, ProVerif can efficiently verify many practical cases and supports a wide range of cryptographic primitives, including encryption, digital signatures, hash functions, and Diffie-Hellman key agreements.

This tutorial provides participants with a comprehensive introduction to using ProVerif for the verification of cryptographic protocols. Designed for researchers, students, and practitioners in the fields of cybersecurity and formal methods, the tutorial balances theoretical foundations with practical, hands-on exercises to facilitate a deep understanding of the tool and its capabilities. Key topics covered include:

• (Basic) Modelling: Participants will learn how to formally represent cryptographic primitives, protocols and both correspondence and equivalence properties in ProVerif.
• (Basic) Understanding ProVerif’s Output.
• (Intermediate) Introduction to More Complex Features of ProVerif: The tutorial will cover some advanced features to handle sophisticated verification scenarios.
• (Advanced) Tricks to Handle the "I Don’t Know" Case: Strategies for mitigating and working around indeterminate results will be discussed.