QILURA

Quantifying Information Leaks using Reliability Analysis

Description

A tool for qualitative and quantitative information flow analysis using Symbolic PathFinder.

Install

QILURA requires the following tools to be installed: Symbolic PathFinder, z3 for Java, Omega and Latte.

In the root folder of the JPF toolsets, edit the site.properties file as follows:

    jpf-home = /homes/qsp30/Programs/jpf # change this with your directory
    jpf-core = ${jpf-home}/jpf-core 
    jpf-symbc = ${jpf-home}/jpf-symbc
    jpf-qilura = ${jpf-home}/jpf-qilura
    extensions+=,${jpf-core} 
    extensions+=,${jpf-symbc}
    extensions+=,${jpf-qilura} 
    

Download jpf-qilura from the github repository, then run:

    ant build

And that's it. There are a set of small case studies under jpf-qilura/src/examples. The python script configEx.py automatically fixes the configurations for the examples corresponding to your installation of Omega and Latte.

All the examples are set for quantitative information flow analysis. Except for SanityCheck1, which sets symbolic.sif.analysis=qualitative for qualitative analysis.