Hide menu

Extending Parameterized Verification to Side-channel Leakage Analysis

Supervisor: Associate professor Ahmed Rezine, ESLAB, Department of Computer and Information Science

Context and Research Area:

Computer programs run on machines with specific micro-architectural components such as caches, pipelines and out-of-order or branch-prediction units. These microarchitectural components impact the relation between program inputs and their behaviors. The gaussian-like figure below was obtained by analysing 256000 randomly chosen keys for an AES-128 implmentation. It shows the number of secret input keys corresponding to each number of cache misses. Capturing this relation is
important both for analysing efficiency and vulnerability to side-channel timing attacks. For instance, the cache misses with the least number of keys leak most information as an attacker would have less keys to guess among.

The configuration details of these micro-architectural components, such as sizes and numbers of cache levels, depths of out-of-order and branch-prediction units, or sizes
of GPU-shared memories do impact this relation between program inputs and behaviors. For instance, the size and associativity of caches defines, together with
the program input, do impact the memory access patterns and the resulting timing behavior of the program. This is cpatured in the figure below where information
leakage for an AES implementation differs from one configuration to the other. Consequently, these specific configurations need to be accounted for when analyzing efficiency or information leakage of mainstream and cryptography
programs.

Simply testing is not enough. Most existing verification techniques are based on static-analysis. Apart from ignoring fundamental micro-architectural details (e.g.,
speculation or cache sizes), they fail to precisely reason about the dynamic relationship between inputs and micro-architectural states observed by attackers.
This lack of precision manifests itself when merging and widening the behaviors of all input values or when estimating the number of possible observations as opposed
to estimating the weight of the observations. In several works, only small classes of computer programs are considered, e.g., constant-time cryptographic programs, or
microarchitectural states are ignored. More recent works only look for certain patterns or disregard the weights of the observations. None considers the
parameterized verification problem.


We aim to generically and symbolically account for several micro-architectural details, including cache sizes and speculative and out-of-order executions.
Parameterized verification aims to verify families of systems, one for each instance of the considered parameter. It can be used to check whether there is some relevant
instance of the parameter that violates the property at hand (e.g., allows for an attacker observation). Existing works on parameterized systems typically use the
number of concurrent components in the system as a parameter. Existing techniques have mainly considered the verification of safety and liveness properties:
from establishing correctness of cache coherence protocols to showing a coherence protocol results in a given consistency memory model.


This work proposes to parameterize verification with respect to input sizes (e.g. array sizes in GPU programs), underlying micro-architecture (e.g., cache
configurations and prediction depths) and classes of attacks and observations

Required Qualifications:

The ideal candidate should have a master’s degree, or equivalent, in computer science with a solid theoretical background in logic and algorithms and excellent software skills. The candidate should have a strong commitment to achieve assigned goals and to reaching research excellence.