QUAIL is a tool to evaluate the security of systems through a quantitative analysis of information leakage. It takes as an input a program written in a simple imperative language with randomized primitives. It builds a Markovian model of the program and analyzes the information leakage in the model.
The tool consists in a preprocessor, an analyzer and a simulator. The preprocessor compiles a program written in the QUAIL imperative language into a lower level language.
The analyzer performs an exhaustive depth-first search of all program traces, and for each one computes the probability of the trace and the posterior entropy of the secret induced
by the trace. This values are used to compute the expected value of the posterior entropy of the secret over all traces, and consequently the information leakage as the difference of the prior and posterior entropy of the secret.
To give a meaningful result, the analyzer must explore all execution traces of the system.
The simulator performs a similar analysis but chooses the traces to analyze randomly. While this means that many traces will be analyzed more than once, it also allows to draw conclusions on the expected posterior entropy of the secret in case not all traces are explored, allowing QUAIL to approximate the information leakage of programs whose trace space is too large to be completely explored.
People
QUAIL is the result of a collaboration between INRIA Rennes and IT University in Copenhagen. The people currently working on the tool are:
- Fabrizio Biondi is a postdoc researcher at INRIA Rennes, lead developer of the project.
- Axel Legay is a researcher at INRIA Rennes and supervisor of the project.
- Louis-Marie Traonouez is a postdoc researcher at INRIA Rennes and developer on the project.
- Andrzej Wąsowski is a professor at IT University and supervisor of the project.
