Provable Mitigation of Side Channel through Parametric Verification – ProMiS

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 including, those in the DARPA challenge.
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.