Lectures

 

Lectures will be given in English, except "fault-based attacks". All course supports will be in English.

 

 

Lectures with an associated practical session (1h30 + 1h30)

 
The Frama-C Framework and some Applications to Code Security [slides]
Speaker: Julien Signoles
 
Abstract: Frama-C is a framework for analysis of code written in C. Its open-source distribution contains 28 code analyses that aim at enhancing code safety and security. Among them, Eva is an abstract-interpretation based value analysis that exhaustively detects at compile time several kinds of code vulnerabilities, while E-ACSL detects them at runtime through monitoring. Also, some Frama-C analyses (e.g. dependency analyses, slicing and impact analysis) may help security audits by exploiting Eva's results. Some others encode custom properties expressed in a dedicated formal specification language in order to verify them by other means. For instance, SecureFlow and MetACSL allow the user to
express confidentiality and integrity properties, as well as security policies, that may be verified by Eva and/or E-ACSL. This tutorial and its associated practical session will introduce Frama-C and these analyses by focusing on their different usages of Frama-C for code security.
 
 
Software vulnerabilities: principles, exploitability, detection and mitigation.  [slides]
Speaker: Laurent Mounier
 
Abstract: This course focuses on classical "software vulnerabilities" which can be found for instance in C/C++ programs, like buffer overflows, use-after-free, type confusions, etc. We explain their underlying mechanisms (at the binary code level), and how they can be effectively exploited by attackers. We also review the main protection mechanisms, offered at the programming level (how to write secure code), at the compilation level and at the execution platform level. Finally, we present the code analysis techniques and tools used in practice for vulnerability detection (fuzzing, dynamic-symbolic execution, and static analysis), and we terminate by discussing about physical fault injection attacks.
In addition, a lab session allows to experiment with concrete vulnerability exploitation examples (both at source and binary levels) and to practice with secure coding rules.
 
 
Symbolic verification of cryptographic protocols using Tamarin  [slides 1] [slides 2]
Speakers: Jannik Dreier and Lucca Hirschi
 
Abstract: In the era of the internet, cryptographic protocols such as SSL/TLS secure most of the applications we use day to day, e.g., online shops, online banking, electronic payments, mobile communications (4G, 5G, etc.). These protocols can be seen as distributed programs describing how to build and exchange secure messages. To achieve security, they use cryptographic primitives such as symmetric and asymmetric encryption, or digital signatures.  However, designing such protocols is notoriously difficult, and massive security failures continue to be revealed, even in mass media. One approach to improve the security of these protocols is the use of formal protocol verification. In formal protocol verification, one creates a precise model of the protocol and the attacker’s capabilities, and tries to prove that – within this model – the protocol ensures the desired properties. Tamarin is an automated verification tool that uses this approach, and which has been used to analyze group key protocols, public-key infrastructure proposals, and proposed standards, such as TLS 1.3 or 5G AKA. Tamarin works in the so-called symbolic model of cryptographic protocols, and enables automatic analysis as well as a powerful interactive mode. Tamarin supports both falsification and unbounded verification of cryptographic protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined convergent equational theory modeling the cryptographic primitives. Moreover, Tamarin also supports unbounded verification of equivalence properties.  During this introductory lecture, we will see how to model protocols in Tamarin, how to specify security properties, and how to interpret the results. In the hands-on session we will apply this to analyze some protocols ourselves. 
 
 
Formal security proofs of assembly cryptographic implementations  [slides]
Speaker: Benjamin Grégoire (and Pierre-Yves Strub for the practical session)
 
Abstract: Vulnerabilities in cryptographic libraries are challenging to detect and/or eliminate using approaches based on testing or fuzzing. This has motivated the use of formal verification for proving functional correctness and side-channel protection for modern cryptographic libraries. I will present an overview of EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt has been used to prove the security of complex cryptographic constructions. While EasyCrypt allows to reason on cryptographic constructions at the algorithmic level, it does not allows to develop directly real implementations. I will show that its link with the Jasmin language allows to obtain formal security garanties for highly optimised assembly implementations. The Jasmin language is designed to support “assembly in the head” programming, it smoothly combines high-level (structured control-flow, variables, etc.) and low-level (assembly instructions, flag manipulation, etc.) constructs. In the second part of the talk I will provide a short introduction to the Jasmin language and how it interact with EasyCrypt.

 
Other lectures 
  

Advanced symbolic verification of cryptographic protocols using Tamarin [slides]
Speaker: Lucca Hirschi (1h30)
 
Abstract:  In this second lecture, we will touch upon advanced protocol verification using Tamarin and recent research results. We will discuss advanced modeling and proof techniques, equivalence properties which can be used to verify privacy properties, refined symbolic modeling of cryptographic primitives, and extensive case studies such as 5G AKA, TLS, and Noise.  
 
 
Synthetic computer malware analysis [slides]
Speaker: Jean-Yves Marion (1h30)
 
Abstract: This lecture is a general introduction to computer malware analysis. It should be of interest to beginning security researchers who are interested in programming language theory, with a few theoretical aspects, or vice versa. Malware analysis is closely related to low-level program analysis and constitutes a great challenge. The goal is to reconstruct an higher-level semantics of a given low-level program and then to understand its behavior from different components and their interactions. The difficulty is that quasi-all information is given by a sequence of bytes coming from an obfuscated source program. The lecture will contend that fields of programming languages, formal methods and Machine Learning have much to offer to malware analysis.
 
 
Differential analysis of a cipher using Constraint Programming [slides]
Speaker: Marine Minier (1h30)
 
Abstract:  The aim of this presentation is to show the problems raised by modeling a differential attack on a given cipher. The main obstacle lies on the difficulty of correctly modeling the XOR operator that increases the size of the search tree. For this, we will first use high-level the language Minizinc and a SAT solver then the constraint programming language written in Java, Choco.
 
 
 
Cryptographic Constant-Time Verification of C programs by Abstract Interpretation [slides]
Speaker: David Pichardie (3h)

Abstract : Constant-time programming is an established discipline to secure programs against timing attacks. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We present an advanced static analysis, based on state-of-the-art techniques from abstract interpretation, to report time leakage during programming. To that purpose, we analyze source C programs and use full context-sensitive and arithmetic-aware alias analyses to track the tainted flows. We first present the basics of Abstract Interpretation for and then present and prove correct the security analysis design on a core language. We also present a prototype implementation for C programs that is based on the CompCert compiler toolchain and its companion Verasco static analyzer. The prototype has been successfully applied on several cryptographic implementations.
 
 
 
Attaques en faute: modélisation, sécurisation et analyse de robustesse de code [slides]
Speaker: Karine Heydemann (1h30) [in French]
 
Abstract: Les attaques dites physiques sont puissantes car elles permettent de compromettre la sécurité d'algorithmes cryptographiques prouvé sûrs, de retrouver des informations sensibles, de contourner des protections, d’escalader des privilèges, etc.  Ce type d’attaques concerne majoritairement les systèmes embarqués. En effet, leur accès physique permet aux attaques dites "par observation" de mesurer des grandeurs physiques (consommation de courant, émanations électromagnétiques, ...). Par ailleurs, les attaques dites "par perturbation" ou "en faute" permettent d'altérer l'environnement d’exécution et en conséquence le comportement de l’application.
 
L’objectif de ce cours est de présenter ces attaques avant de se concentrer sur les problématiques en lien avec les attaques en faute. Plus précisément, se prémunir contre ces attaques en faute nécessite de comprendre les effets induits par les moyens d’injection de fautes, de concevoir des protections et de valider la robustesse de ces protections. La première partie de la présentation se concentrera sur les moyens d’injection de faute et l'exploitation de fautes avant d’aborder la modélisation des effets des injections de faute au niveau logiciel. La deuxième partie concernera les protections logicielles contre ces attaques et la problématique de leur déploiement. Enfin, les techniques d’analyse de la robustesse de code seront abordées.  La conclusion présentera des questions ouvertes autour de ces sujets.

 
Online user: 3 Privacy
Loading...