{"id":4,"date":"2011-12-08T11:55:34","date_gmt":"2011-12-08T11:55:34","guid":{"rendered":"http:\/\/project.inria.fr\/template1\/?page_id=4"},"modified":"2014-09-17T17:45:27","modified_gmt":"2014-09-17T15:45:27","slug":"home","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/quail\/","title":{"rendered":"About"},"content":{"rendered":"

QUAIL is a tool to evaluate the security of systems through\u00a0a quantitative analysis of information leakage. It takes as\u00a0an input a program written in a simple imperative language with randomized primitives. It builds a Markovian model of\u00a0the program and analyzes the information leakage in the model.<\/p>\n

The tool consists in a preprocessor, an analyzer and a simulator.\u00a0The preprocessor compiles a program written in the QUAIL imperative\u00a0language into a lower level language.<\/p>\n

The analyzer performs an exhaustive depth-first search of all\u00a0program traces, and for each one computes the probability of\u00a0the trace and the posterior entropy of the secret induced
\nby 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.
\nTo give a meaningful result, the analyzer must explore all\u00a0execution traces of the system.<\/p>\n

The simulator performs a similar analysis but chooses the traces\u00a0to analyze randomly. While this means that many traces will be analyzed\u00a0more than once, it also allows to draw conclusions on the expected posterior entropy of the secret in case not all traces are explored,\u00a0allowing QUAIL to approximate the information leakage of programs\u00a0whose trace space is too large to be completely explored.<\/p>\n

<\/a><\/p>\n

People<\/span><\/h1>\n

QUAIL is the result of a collaboration between INRIA<\/a> Rennes and IT University<\/a> in Copenhagen. The people currently working on the tool are:<\/p>\n