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:
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.
Post-doc (2020-…)
Université de Lorraine, France
Master student (2020)
Université de Lorraine, France
PhD student (2020-…)
Université de Lorraine, France
PhD student
SUTD, Singapore
Research Scientist
SMU, Singapore
Date | Meeting | Place |
---|---|---|
29th May 2020 | Kick-off meeting | Virtual |
5th January 2021 | Quick meeting #1 | Virtual |