Programme

09h30	—	Accueil autour d'un café
10h00	Cristian Cadar	Keynote. Finding Bugs and Security Vulnerabilities with Dynamic Symbolic Execution. [abstract] [slides]
11h00	—	Pause
11h20	Barbara Fila	Attack trees: meaning, analysis, and correctness. [abstract] [slides]
12h05	Itsaka Rakotonirina	Efficient verification of observational equivalences in finite-process calculi. [abstract] [slides]
12h35	—	Déjeuner
14H00	Cătălin Hrițcu	When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. [abstract] [slides]
14h45	Thomas Letan	Specifying and Verifying Hardware-based Security Enforcement mechanisms. [abstract] [slides]
15h15	—	Pause
15h35	Patricia Mouy	Use of formal methods in the Common Criteria Context. [abstract]
16h20	Johan Laurent	A Cross-Layer Security Approach: Combining Accurate Modelling of Hardware Faults with Static Software Analysis. [abstract] [slides]
16h50	les organisateurs	Mot sur le GT. [slides]
17h00	—	Fin de la journée

Résumés des présentations

Keynote — Finding Bugs and Security Vulnerabilities with Dynamic Symbolic Execution

Cristian Cadar – Imperial College London

Abstract. Software systems are affected on a regular basis by bugs and security vulnerabilities. In this talk, I will present dynamic symbolic execution, a technique that can help detect many of these problems before they make it into production. Dynamic symbolic execution has already started to make a positive impact on the reliability and security of software, with several high-profile companies using it on a regular basis to analyse their software.

The talk will focus on recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different scenarios, such as high-coverage test input generation, bug detection, patch testing and bounded verification, among many others.

Cristian Cadar is Professor of Software Reliability in the Department of Computing at Imperial College London, where he leads the Software Reliability Group (http://srg.doc.ic.ac.uk), working on automatic techniques for increasing the reliability and security of software systems. Cristian's research has been recognised by several prestigious awards, including the EuroSys Jochen Liedtke Award, the HVC Award, the BCS Roger Needham Award, the ACM SIGOPS Hall of Fame Award, and the ACM CCS Test of Time Award. He also received an ERC Consolidator Grant and an EPSRC Early-Career Fellowship. Many of the research techniques he co-authored have been open-sourced and used by several groups in both academia and industry. In particular, he is co-author and the principal maintainer of the KLEE symbolic execution system, a popular system with a large user base. Cristian has a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.

Attack trees: meaning, analysis, and correctness

Barbara Fila – IRISA, INSA Rennes

Abstract. Since their introduction in 1999, attack trees have become one of the most popular models for representation of security issues. They have been successfully adopted by industry where they are employed to evaluate the security of systems and organizations. More recently, attack trees attracted the attention of formal methods scientists interested in their meaning, their automated creation, and their potential for quantitative analysis of security.

This talk will focus on three practical aspects related to attack tree modeling and analysis. We will be first interested in attack trees with repeated nodes representing attacker's actions that may contribute to several distinct attack vectors. Next, we will investigate the problem of multi-parameter security analysis with attack trees. Finally, we will develop a semantics allowing us to verify the quality of an attack tree with respect to the system to be analyzed.

This presentation will be based on my joint research work with Wojciech Widel, Sophie Pinchinat, and Maxime Audinot.

Efficient verification of observational equivalences in finite-process calculi

Itsaka Rakotonirina – INRIA - LORIA

Abstract. Security protocols are distributed programs used for circulating information remotely, especially for sensitive applications such as online banking, electronic voting–or any internet connection to any website. These protocols are notoriously hard to design and have a long history of flawed structures, making it possible for external parties controlling the communication network to bypass their security. In this work we are interested in automated proofs that a given protocol is privacy preserving for a chosen notion of privacy, and number of users. Such properties are usually modelled as behavioural equivalences in concurrent process calculi (e.g. variants of the pi-calculus). We implement the DeepSec prover, an automated tool deciding such equivalences, as well as powerful optimisations that reduced its verification time by several orders of magnitude by exploiting the process symmetries that naturally arise during practical verification.

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

Cătălin Hrițcu – INRIA

Abstract. We propose a new formal criterion for evaluating secure compartmentalization schemes for unsafe languages like C and C++, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior—for example, by accessing an array out of bounds. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others—in particular, from components that have encountered undefined behavior and become compromised. To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We propose a novel proof technique and give a machine-checked proof in Coq that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor.

Catalin Hritcu is a researcher at Inria Paris where he works on security foundations. He is particularly interested in formal methods for security (secure compilation, compartmentalization, memory safety, security protocols, integrity, information flow), programming languages (program verification, proof assistants, type systems, semantics, formal metatheory, certified tools, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, secure hardware). He was awarded an ERC Starting Grant on formally secure compilation (https://secure-compilation.github.io), and is also actively involved in the design of the F* verification system (https://www.fstar-lang.org/), which is used for building a formally verified HTTPS stack (https://project-everest.github.io). Catalin received a PhD from Saarland University in Saarbrücken, a Habilitation from ENS Paris, and was previously also a Research Associate at University of Pennsylvania and a Visiting Researcher at Microsoft Research Redmond.

Specifying and Verifying Hardware-based Security Enforcement mechanisms

Thomas Letan – ANSSI

Abstract. In this talk, we focus on Hardware-based Security Enforcement (HSE) mechanisms, when trusted software components configure hardware mechanisms to constrain the execution of untrusted —and arbitrary– software components. Over the past decade, several critical vulnerabilities have been disclosed which specifically target HSE mechanisms and which leveraged errors in the specifications of the underlying hardware mechanisms rather than inconsistencies in the implementation.

We discuss our motivations to apply formal methods to this particular use case, and our related contributions. Initiated in late 2014, our work is in line with ongoing efforts to increase the robustness of commodity hardware architectures (e.g., ARM formal specification by Reid et al.).

Use of formal methods in the Common Criteria Context

Patricia Mouy, Thomas Letan – ANSSI

Abstract. The Common Criteria (CC) is a international standard for IT security certification. Seven evaluation assurance levels (EAL 7) are defined and reflect assurance requirements that must be met to achieve Common Criteria certification. Formals methods are required for the highest levels of assurance of common criteria i.e. the most stringent and expensive ones. This talk will begin with a general overview of the common criteria context. Then, in the particular context of CC and the French scheme, the definition of a formal method will be presented with the associated expectations and precautions about its use for an evaluation. Finally, the process and conditions of accepting a new formal method in the CC context will be explained.

A Cross-Layer Security Approach: Combining Accurate Modelling of Hardware Faults with Static Software Analysis

Johan Laurent – LCIS

Abstract. As technology evolves, digital systems with increasing complexity are becoming more vulnerable to hardware fault attacks. Analyzing the vulnerabilities of a program against these fault attacks hence requires powerful techniques such as static code analysis. The methods developed so far usually apply these techniques with typical software fault models. However, the effects of fault attacks on a program are very diverse, and are not entirely captured by these typical software fault models. In this presentation, we will present a method to accurately model at the software level what happens when a modern processor is attacked with hardware faults; and show what kind of analyses can be conducted to prove the validity of various security properties against these accurate software fault models.