Keynotes

Marco Patrignani (DISI, University of Trento, Italy)

Title: Secure Compilation: Formal Foundations and (Some) Applications

Abstract:

Secure compilation aims to devise compilation chains (compilers, linkers, loaders, runtime systems, hardware) that eliminate many of today’s security vulnerabilities and that allow sound reasoning about security properties upheld by said chains.

This talk defines what kind of vulnerabilities and of security properties are of interest in a secure compilation scenario.

Then, it presents the recently-devised formal foundations of secure compilation, which can be used to clearly specify the security of the aforementioned secure compilation chains.

Finally, the talk also discusses how these foundations can be applied to reason about realistic compilation chains in order to preserve crucial security properties such as memory safety, cryptographic constant time, and speculative non-interference.

Steve Kremer (Inria, Loria, Nancy)

Title: DY Fuzzing: Putting a Dolev-Yao attacker in the fuzzing loop

Abstract:
Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is today still out of reach. This leaves open whether such implementations are secure. Unfortunately, this blind spot hides numerous attacks, such as recent logical attacks on widely used TLS implementations introduced by implementation bugs.

We propose a novel and effective technique that we call DY model-guided fuzzing, which precludes logical attacks against protocol implementations. The main idea is to consider as possible test cases the set of abstract DY executions of the DY attacker, and use a novel mutation-based fuzzer to explore this set. The DY fuzzer concretizes each abstract execution to test it on the program under test. This approach enables reasoning at a more structural and security-related level of messages represented as formal terms (e.g. decrypt a message and re-encrypt it with a different key) as opposed to random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors. We implement a full-fledged and modular DY protocol fuzzer and demonstrate its effectiveness by fuzzing three popular TLS implementations, resulting in the discovery of several novel vulnerabilities.

Ioana Boureanu (University of Surrey, UK)

Title: Epistemic Verification of Information-Flow Properties in Programs

Abstract:
We will look at three approaches to make the verification of certain privacy-encoding properties in programs more expressive and more efficient.

Concretely, we target knowledge-intrinsic properties over the states of a program, such as “a program-thread knows that variable x is equal to y + 5”.

To formalise these at different levels, we introduce various “program-epistemic” logics, in which we can express statements like: if command/program C starts at a state satisfying φ, then in all states where the execution of C finishes, agent A is epistemically unaware of π. In the latter, π is a formula which can contain several knowledge/epistemic operators scoping quantifier-free first-order formulae. We show that, in some cases and for some programs, model checking different such logics can be reduced to SMT-solving. Lastly, we report our experimental results which show that this SMT-reducing technique outperforms classical, epistemic model checking.

(Based on joint work with several colleagues, published at IJCAI2017, AAAI 2023, and FM 2023)

Online user: 3

Privacy