Markovian Processes for Quantitative Information Leakage

Quantification of information leakage is a successful approach for evaluating the
security of a system. It models the system to be analyzed as a channel with
the secret as the input and an output as observable by the attacker as the output, and applies information theory to quantify the amount of information transmitted through such channel, thus effectively quantifying how many bits of the secret can be inferred by the attacker by analyzing the system’s output.

Channels are usually encoded as matrices of conditional probabilities, known as
channel matrices. Such matrices grow exponentially in the size of the secret and
observables, are cumbersome to compute and store, encode both the behavior
of the system and assumptions about the attacker, and assume an input-output
behavior of the system. For these reasons we propose to model the systemattacker scenario with Markovian models.

We show that such models are more compact and treatable than channel matrices. Also, they clearly separate the behavior of the system from the assumptions about the attacker, and can represent even non-terminating behavior in a finite model.

We provide techniques and algorithms to model and analyze both deterministic
and randomized processes with Markovian models and to compute their information leakage for a very general model of attacker. We present the QUAIL tool that automates such analysis and is able to compute the information leakage of an imperative WHILE language. Finally, we show how to use QUAIL to analyze some interesting cases of secret-dependent protocols.