ProMiS

Scientific objectives

The Spectre vulnerability has recently been reported, which affects most modern processors. The idea is that attackers can extract information about the private data using a timing attack. It is an example of side channel attacks, where secure information flows through side channels unintentionally. How to systematically mitigate such attacks is an important and yet challenging research problem.

We propose to automatically synthesize mitigation of side channel attacks (e.g., timing or cache) using formal verification techniques. The idea is to reduce this problem to the parameter synthesis problem of a given formalism (for instance, variants of the well-known formalism of parametric timed automata). Given a program/system with design parameters which can be tuned to mitigate side channel attacks, our approach will automatically generate provably secure valuations of these parameters. We will use a 3-phase research plan:

1. define formally the problem of timing information leakage;
2. propose optimized parametric model checking algorithms for information leakage checking;
3. propose optimizations and methods translating real-worlds systems and programs into our formalisms to achieve practical scalability.

We plan to deliver a fully automated toolkit which can be automatically applied to real-world systems. This project will benefit from the synergy of 5 scientists in 4 partner labs, with a complementary expertise in security, formal methods and program analysis.

Meetings

Publications

2020

• Étienne André and Aleksander Kryukov. Parametric non-interference in timed automata. In Yi Li and Alan Liew (eds.), ICECCS’20, October 2020. To appear. (English)

2019

• Étienne André and Sun Jun. Parametric timed model checking for guaranteeing timed opacity. In Yu-Fang Chen, Chih-Hong Cheng and Javier Esparza (eds.), ATVA’19, Springer LNCS 11781, pages 115–130, October 2019. DOI: 10.1007/978-3-030-31784-3_7 (English) [PDF (author version) | BibTeX | data | Slides]