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

TBA

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 it is 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

CTF CrytpoLocker: challenge launch — Fabrice Sabatier and Guillaume Bonfante

TBA.

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

See above.

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

See above.

On Malware Detection, Why it is Difficult — Guillaume Bonfante

See above.

Comments are closed.