Summer School
June 13–17, 2022

Šibenik, Croatia
   Summer School
   on real-world crypto and privacy
Tutorial speakers

List of (currently) confirmed tutorial speakers

Abstracts

  • Manuel Barbosa, University of Porto (DCC-FCUP) and HASLab/INESC TEC, Portugal
    Title: An introduction to machine-checked cryptography in EasyCrypt and Jasmin
    Duration: 1/2 day
    Abstract: EasyCrypt is a toolset for construction and verification of game-based cryptographic proofs. It has been used to develop proofs of the proofs of a number of cryptographic primitives and protocols, as well as a verification backend for verified assembly implementations of cryptographic primitives written in the Jasmin language. This tutorial will explain how to use EasyCrypt and Jasmin in combination to obtain high-assurance assembly implementations of cryptography, with formal cryptographic security guarantees. We will do so by looking at a simple symmetric encryption example, with exercises building up to a full symmetric encryption scheme.

  • Steffen Becker , MPI-SP, Germany (joint work with Nils Albartus, Thorben Moos, Julian Speith)
    Title: A Brief Introduction to Hardware Reverse Engineering
    Duration: 1/2 day
    Abstract: Hardware Reverse Engineering (HRE) is the basis for a wide range of applications: For example, it helps detect malicious circuit manipulations or enables competitor analysis - but it can also provide important information to an adversary who may want to plagiarize designs or insert hardware trojans into a circuit.
    In this tutorial, we explore and comprehend the inner workings of integrated circuits through the example of a modern block cipher. To this end, you will break the cryptographic implementation of the block cipher using the state-of-the-art netlist reverse engineering framework HAL (github.com/emsec/hal). Together we will take the first steps of netlist sensemaking and gain hands-on experience with some fundamental methods of reverse engineering hardware circuits based on current scientific knowledge.
    As a prerequisite, you only need to bring your own laptop. A basic understanding of digital hardware circuits and elementary knowledge of Python are recommended, but not required.

  • Chitchanok Chuengsatiansup and Yuval Yarom, University of Adelaide, Australia
    Title: A Primer on Cache Attacks
    Duration: 1/2 day
    Abstract: To improve performance, modern processor include a wide array of caches that store data and results of internal computation. In 2002, Tsunoo and others first demonstrated that these caches can leak sensitive information. Since then, dozens of attacks affecting various caches have been published, demonstrating that caching can pose a significant threat to computer security. In this tutorial explores the various caches that modern computers employ. We discuss some of the attack techniques that have been published, and supplement the discussion with live demonstration. We further explore some of the technique used for reverse engineering the implementation details of caches, approachs for improving attacks, and proposed defenses.

  • Cas Cremers, CISPA, Germany
    Title: Tamarin Prover Tutorial
    Duration: 1 day
    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.

  • Nele Mentens, Jo Vliegen, Laurens Le Jeune and Arish Sateesan, KU Leuven, Belgium and Leiden University, Netherlands
    Title: Hands-on Introductory Tutorial on Network Intrustion Detection
    Duration: 1/2 day
    Abstract: This tutorial gives an introduction to Network Intrusion Detection Systems (NIDS). It starts with explaining three popular approaches, namely pattern matching, flow measurement and machine learning. In the hands-on part of the tutorial, the participants will experiment with the three approaches in a Python simulation framework.

  • Stjepan Picek, Radboud University, Netherlands
    Title: Deep Learning-based Side-channel Analysis
    Duration: 1/2 day
    Abstract: In the last few years, profiling side-channel analysis (SCA) based on deep learning proved to be very successful in breaking cryptographic implementations. Still, despite successful attacks, even in the presence of various countermeasures, there are many open questions. This tutorial provides a quick introduction to deep learning-based SCA. We start with basic multilayer perceptron and convolutional neural network architectures to attack simpler datasets. Afterward, we will visit more advanced topics like denoising autoencoders to remove countermeasures and generative adversarial networks for data augmentation. We finish with the state-of-the-art results that allow us to break publicly available datasets with only a few attack traces. For the tutorial, we will use the recently developed AISY framework (GitHub - AISyLab/AISY_Framework: Deep Learning-based Framework for Side-Channel Analysis).

  • Ahmad-Reza Sadeghi, TU Darmstadt, Germany (joint work with Hossein Fereidooni and Phillip Rieger)
    Title: The hitchhiker's guide to the Security and Privacy of Federated Learning
    Duration: 1/2 day
    Abstract: With the increasing digital transformation and emerging applications, Big data and Artificial intelligence (AI) have been developing rapidly. The widespread and rapid deployment of AI enlarges the attack surface and requires new security and privacy- enhancing methodologies and technologies to tackle the intrinsic AI security and privacy shortcomings.
      Federated Learning (FL) is a Machine Learning approach in which multiple clients collaboratively train a Neural Network (NN) model on their private data without the need to share the data.  With the increasing application of FL systems, a number of security, privacy, and functional challenges are posed on the design and implementation of the underlying algorithms and systems.  Attacks on FL stem from either the privacy perspective when a malicious user or the central server attempts to infer the private data of a victim user, or the security perspective when a malicious user aims to compromise the global model.
      In this tutorial, we mainly focus on security threats in FL systems such as model/data poisoning that are categorized into targeted and untargeted attacks. In targeted (backdoor) poisoning attacks, an adversary aims to hide a backdoor trigger into the global model by adding malicious data to the local datasets, or, if the adversary fully controls the malicious clients, also by changing the hyperparameters of the training process. Untargeted attacks aim to thwart the learning of the global model (i.e., convergence failure).  The primary objective of this tutorial is to investigate different kinds of backdoor attacks and defense solutions that help to mitigate the effect of these attacks. The tutorial is accompanied with hands on exercise where the participants learn how to launch backdoor attacks and implement a defense mechanism that is sufficiently robust and resilient to security attacks that compromise the integrity of the FL model and the training dataset.