Program

Keynotes

Electronic Voting: Properties, Design, and Attacks — Véronique Cortier

Electronic voting aims to achieve the same properties as traditional paper based voting. Even when voters vote from their home, they should be given the same guarantees, without having to trust the election authorities, the voting infrastructure, and/or the Internet network. The two main security goals are vote privacy: no one should know how I voted; and verifiability: a voter should be able to check that the votes have been properly counted.
In this talk, we will explore how these properties can be realized but also attacked. We will in particular illustrate our presentation with the Belenios protocol.

Building Great Fuzzers in Five Minutes — Andreas Zeller

Generating software tests automatically is one of the great promises of Software Analyses and Testing. Traditionally, building a test generator (or “fuzzer”) has been work that would take months, if not years of work; extending fuzzers for particular purposes wasn’t an easy thing to do either. In this lecture, I introduce students and researchers into “The Fuzzing Book” (fuzzingbook.org), which is both a textbook and executable software collection for a large number of test generation techniques. Starting from simple fuzzers, I show how to develop and build a number of test generation approaches, from simple random and feedback-driven fuzzing to advanced techniques such as grammar-based testing or automated GUI testing – using super-compact Python code that can be extended and adapted within minutes. The session will be mainly live coding and experimenting, with plenty of opportunities for interaction and further suggestions. All examples can be run live in your browser at fuzzingbook.org.

A Quest for Provable Security against Side-Channel Attacks — Matthieu Rivain

We live in a world in which cryptography has become ubiquitous. Devices around us are constantly processing cryptographic computations to ensure the confidentiality and the authenticity of our communications. Over the last forty years, the scientific community and the industry have converged towards the paradigm of provable security for cryptographic algorithms and protocols: they should come with a security proof formally stating their security under well-studied computational hardness assumptions.

In the late 90’s, it was shown that the implementations of (provably secure) cryptosystems could be practically broken by side-channel attacks which exploit their physical leakage, such as their execution time, power consumption, or electromagnetic emanation. While a lot of progress was made over the last decades to design practical countermeasures against side-channel attacks, achieving provable security for cryptographic implementations under this threat is still a work in progress.

In this talk, I will present on-going research efforts to achieve this goal. We will see how to formally model the side channel leakage under the assumption that it is somehow noisy. We will further study the masking technique whose principle is to apply secret sharing at the computation level. We will see how to reason about the security of masking in different formal models and will discuss the remaining gaps to be closed in the quest for provable security against side-channel attacks.

Lectures

Formal Proofs of Cryptographic Protocols with Squirrel — David Baelde and Adrien Koutsos

Cryptographic protocols organize many of our electronic activities: chatting, shopping, voting, etc. Technically speaking, they are small concurrent programs making use of cryptographic primitives: encryption, signature, hashes, etc. Analyzing cryptographic protocols is difficult because they execute in unknown, adverse environments, and because the expected properties are complex, involving notions like knowledge and indistinguishability.

Formal methods have been used for decades to analyze security protocols, with many success stories. A widespread approach, pioneered by Dolev and Yao, abstracts messages as formal terms. Other techniques stick to the cryptographer’s model where messages are arbitrary bitstrings and adversaries perform arbitrary probabilistic computations.

We will present a specific approach to protocol verification, pioneered by Bana and Comon, which leverages the symbolic toolkit of logic but provides guarantees in the cryptographer’s model for provable security.
This approach is embodied in the Squirrel proof assistant, which we will use to discover the logic by experimenting on small examples. The course will not require any priori knowledge of formal logic.

Cryptanalysis in Practice — Gaëtan Leurent

The security of cryptographic primitives can not be proven formally and must be evaluated through cryptanalysis. Well-designed primitives like the AES have been analysed for years and we have a strong confidence that they offer a good security margin. Typical attacks only reach reduced versions of primitives, and are not practical due to a high complexity or a strong adversarial model.

However, some primitives are weaker than expected, and cryptanalysis can sometimes lead to practical breaks. In this talk, we will focus on two examples: SHA-1 and GEA. They illustrate the importance of public specification, constant analysis, and quick deprecation when a primitive is found to be broken.

On Malware Detection, Why is it Difficult — Guillaume Bonfante

We discuss the question of malware detection. Taking this point of view, we present the underlying problems that deserve a scientific approach. Standard methods in code analysis quite often fail when applied to malware. This is due to the fact that malware are protected against reverse-engineering. We will illustrate that with some traps we could observe in some malware.

Micro-Architectural Attacks: from CPU to Browser — Clémentine Maurice

Hardware is often considered as an abstract layer that behaves correctly, just executing instructions and outputting a result. However, the internal state of the hardware leaks information about the programs that are executing, paving the way for covert or side-channel attacks. Many micro-architectural components can be used for such attacks; in particular, the CPU cache has been a target highly studied in the last years.
In this lecture, we will first cover the basics of micro-architectural attacks: what type of attacks can be performed, how, and in which conditions. We will then focus on how to mount these attacks from web browsers. Indeed, micro-architectural attacks require precisely monitoring low-level hardware features. In contrast, browsers only provide high-level sandboxed languages with a limited set of functions. Porting these attacks to the web thus exposes a series of challenges.

High-Assurance High-Speed Cryptography Implementations in Jasmin — Vincent Laporte and Benjamin Grégoire

Cryptography implementors face multiple challenges: efficiency (every CPU cycle is precious), correctness (lest usefulness and security guaranties vanish), security in spite of side-channels (sensitive data should not leak). The Jasmin language has been designed to address these conflicting goals: Jasmin programs are amenable to formal verification; yet, programmers can control many low-level details of the assembly code produced by the Jasmin compiler and achieve very high performance.

In this lecture, participants will learn how to get started with the Jasmin ecosystem to write programs and verify, using automated tools, that they enjoy desirable safety and security properties.

Practical sessions

Please complete all instructions to install the required software and working environment before the summer school starts.

Formal Proofs of Cryptographic Protocols with Squirrel — David Baelde and Adrien Koutsos

Instructions:

There are two ways to install the Squirrel Prover

  • with Docker: the simplest solution, but only supports CLI or web browser interface. Advised for less technical savy users. Please favor the standard installation below since, on some systems, the web interface has problems such as poor rendering or clumsy keyboard shortcuts.
  • standard installation, with Proof General: more complicated, but allows to use Squirrel with a real graphical interface (Emacs + Proof General).
With Docker

Squirrel can be installed using a Docker image. This is the simplest solution, but it only allows to use Squirrel in the terminal, or in a web browser. Installation instructions can be found here
https://github.com/squirrel-prover/squirrel-prover/blob/master/docker/README.md

Standard installation from source (preferred)

Installing Squirrel from sources allow to use Squirrel with a complete graphical interface (Emacs + Proof General). Installation instructions can be found here
https://github.com/squirrel-prover/squirrel-prover/#readme
Be sure to also install and configure the Proof General mode for Emacs.

Useful links

High-Assurance High-Speed Cryptography Implementations in Jasmin — Vincent Laporte and Benjamin Grégoire

Instructions:
Install the Jasmin Compiler at version 2022.04.0, either

For troubleshooting, contact us on Zulip (https://github.com/jasmin-lang/jasmin/wiki/Get-support#zulip-chat)

On Malware Detection, Why it is Difficult — Guillaume Bonfante

Instructions:

Please download and load (for example with VMWare, VirtualBox, or Fusion on MacOS) the following virtual machine image:

https://filesender.renater.fr/?s=download&token=541f5f03-f95d-4ca7-a88f-8de7a69aff71

CTF CrytpoLocker: challenge launch — Fabrice Sabatier and Guillaume Bonfante

(same instructions as above)

Social Event

We will meet at 17:30 on Tuesday July 5th at Place Stanislas, next to “l’office du tourime” (here on the map) for a 1 hour and a half guided tour of Nancy. There will be two guides: one speaking in french and one speaking in English.

Right after the guided tour, we will meet for the banquet at 19:00 the same day at Grand Café Foy, which is also at Place Stanislas (here on the map).

Feel free to organize meetups in the city center the other days. There is a channel dedicated to this on the Discord server.

Rump and Poster session

If you wish to participate to the rump or/and the poster session, please go to the link we sent you on the June 29th to register. During the rump session, anyone can give a short talk (maximum 5 minutes) about his/her work; it can be about ongoing, unpublished work. You can also bring a poster about your work and we will provide poster support so that you can display your poster throughout the summer school and present your work this way.

Comments are closed.