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.