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

2021

• Étienne André, Didier Lime and Mathias Ramparison. Parametric updates in parametric timed automata. Logical Methods in Computer Science, February 2021. To appear. (English) [PDF]
• Étienne André, Didier Lime, Mathias Ramparison and Mariëlle Stoelinga. Parametric analyses of attack-fault trees. Fundamenta Informaticæ, January 2021. To appear. (English) [data]
• Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS’21, March 2021. To appear. (English) [data]
• Masaki Waga (和賀 正樹), Étienne André and Ichiro Hasuo (蓮尾 一郎). Model-bounded monitoring of hybrid systems. In Mohammad Al Farque and Meeko Oishi (eds.), ICCPS’21, May 2021. To appear. (English)

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]

Talks

2020

• Étienne André. Retour d’expérience sur le plan de gestion de données du projet ProMiS. In 3^e journée annuelle de séminaire autour de la science ouverte : les données de la recherche, October 2020. (French 🇫🇷) [Slides]