Keynote: What is an attacker ?  [slides] [video (sorry, the few initial seconds are lost)]

Hubert Comon -- LMF (ENS Paris-Saclay)

The main difference between model checking and formal proofs of security is the interaction with an attacker. We wish to prove properties, for any (reasonable) attacker. This requires to formally define what is a reasonable attacker. This can be disputed and some programs that are formally proved secure could be attacked if we change the attacker model.

We advocate here the axiomatization method: design (first-order) axioms stating what an attacker cannot do. In other words, security proofs will rely on these axioms only, and the scope of the proof will be for any attacker that satisfies the axioms.

We will provide with examples and survey the project and results following this line of research since 2014. (This includes contributions by D. Baelde, G. Bana, R. Chadha, C. Jacomme, A. Koutsos, G. Scerri).

Secure Compilation for Software Fault Isolation and Information Flow Preservation [slides]

Frédéric Besson -- Irisa Celtique (Inria Rennes)

Compiler correctness ensures that a safe source code is compiled into a safe binary. What about security preservation? We present two approaches for preserving security through the compiler chain. In the first approach, we reduce security to safety and show how to enforce Software Fault Isolation (SFI), a sandboxing security property, by inserting a SFI transformation in the middle-end of CompCert. In the second approach, we study an information flow property modeling an attacker performing memory probing. Classic compiler optimisations such as dead code elimination and register allocation do not preserve this security property. We propose a framework to reason about security preservation and how optimisations can be secured.

Testing and Verifying Smart Contracts: From Theory to Practice [slides]

Josselin Feist -- Trail of Bits

Blockchain technology and its application in smart contracts are a recent and growing topic of research. Smart contracts enforce user trust by using a consensus-based protocol. Due to their reasonably small code size, contracts are a good target for the application of formal methods. Additionally, their business-oriented logic allows to leverage property-based techniques. However, several recent large incidents have demonstrated that smart contracts are not without vulnerabilities. In this presentation, we will discuss the state of smart contracts program analysis techniques and tools. We will demonstrate their usage through real-world bugs found by (semi)-automated tools. Finally, we will highlight the current challenges and research opportunities.

Decentralized Personal Data Management Systems: Challenges for Formal Methods [slides]

Guillaume Scerri -- DAVID (Univ. Versailles Saint-Quentin, Inria Saclay)

With the recent rise of secure hardware in consumer grade electronics (e.g. Intel's SGX) and advances in legislation regarding personal data, there has been a push towards secure decentralized personal data management systems. The main goal of this line of research is shifting personal data processing from centralized providers towards user controlled environments, giving back agency over their own data to users. We will give an overview of a number of recent advances tackling various aspects of this challenge, from safely storing and processing data on end user machines to secure collective data processing and sharing data or computation results with other users and service providers. We will also explore presents the unique challenges for formal methods presented by a full personal management system. In particular, such large new systems involve complex security definitions where user actions need to be carefully modeled, unclear code semantics for processing personal data (i.e. image processing and machine learning over personal data) and interaction between a lot of subsystems with of lot of security dependency (i.e. image processing over photos in your contacts could typically be linked to access control for sharing data with friends). Carefully modelling and verifying such systems could be critical for the adoption of secure decentralized personal data management and taking back control over personal data.

Efficient Relational Symbolic Execution for Speculative Constant-Time at Binary-Level [slides]

Lesly-Ann Daniel -- LIST (CEA Saclay)

The constant-time programming discipline is an efficient countermeasure against timing side-channel attacks, used in cryptographic libraries. However, since 2018, Spectre attacks undermine these guarantees and allow an attacker recover secrets, even in constant-time code, by exploiting speculation mechanisms in processors. Defenses at the software level have been proposed, yet assessing their correctness or detecting Spectre-vulnerabilities pose challenges due on one hand to the explosion of the exploration space induced by speculative paths, and on the other hand to the introduction of new Spectre vulnerabilities at different compilation stages. In this talk, we present new techniques to efficiently analyze binary-level code for constant-time in a speculative execution context. Our key technical insight is to adapt symbolic execution to execute the new behaviors introduced by speculation, at the same time as regular (in-order) executions. We implement these optimizations in a tool, Binsec/Haunted, and show that it is more efficient than other state-of-the-art tools. Finally, we analyzed real-world cryptographic libraries and found new Spectre-violations introduced during compilation, including one introduced by index-masking, a well known defense against Spectre.

Toward Complete Stack Safety for Capability Machines [slides]

Alix Trieu -- Logic and Semantics group (Aarhus Univ., Danemark)

Capability machines are computers that provide support for fine grained control over memory accesses. Pointers are replaced by capabilities, unforgeable tokens of authority that represent the ability to access a memory location. As such, capability machines are an attractive target for secure compilation, and this interest is further compounded by the recent commitment from Arm to develop an industrial prototype of CHERI-based capability machines. It is thus no surprise that numerous recent works have proposed techniques for enforcing well-bracketed control-flow (WBCF) and local state encapsulation (LSE), temporal stack safety, or temporal heap safety. However, these solutions still fall short of ensuring complete stack safety. In this presentation, I will review recent propositions from the literature for protecting the call stack and identify limitations. I will further propose an extension to capability machines and a potential solution for achieving complete stack safety.

Secure Optimization Through Opaque Observations [slides]

Son Tuan Vu -- LIP6 (Sorbonne Université)

Secure applications implement software protections against side-channel and physical attacks. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. To prevent optimizing compilers from altering the protection, security engineers embed input/output side-effects into the protection. These side-effects are error-prone and compiler-dependent, and the current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. Instead, we introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the traditional input/output-preservation contract of compilers. We show how to guarantee their preservation without modifying compilation passes and with as little performance impact as possible.