ProMiS

Provable Mitigation of Side Channel through Parametric Verification
An ANR-NRF French-Singaporean project (2020-2023)

Scientific objectives

security (Credit: Philipp Katzenberger)

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.

Permanent members

Étienne André

Étienne André

Université de Lorraine, France

French PI

Jun Sun

Jun Sun

Singapore Management University (SMU), Singapore

Singaporean PI

Sudipta Chattopadhyay

Sudipta Chattopadhyay

Singapore University of Technology and Design (SUTD), Singapore

Didier Lime

Didier Lime

École Centrale Nantes, France

Olivier H. Roux

Olivier H. Roux

École Centrale Nantes, France

Temporary members

Aleksander Kryukov

Intern (2020)
Université de Lorraine, France

Lorem ipsum amet

PhD student
Université de Lorraine, France

Aliquam sed nullam

Post-doc
Université de Lorraine, France

Meetings

Date Meeting Place
29th May 2020 Kick-off meeting Virtual

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