Information Flow Control (IFC) examines whether an attacker can gain knowledge on the secret inputs of a program by just examining the public output. Sometimes leaking a small amount of information to the attacker in inevitable, e.g. a password checker will leak whether the password is equal to a given input or not. The amount of leakage is evaluated in quantitative IFC using a measure of entropy.
There are existing tools for analysing C and C++ Code based on Approximate Model Counting, e.g. ApproxFlow, Scalable Approximation of Quantitative Information Flow in Programs. These tools typically generate a SMT formula for a given program, using e.g. CBMC, and then evaluate the number of times that the model is satisfiable. This gives a good approximation on the amount of leakage.
JBMC is a rather new tool that allows to generate SMT formulas for Java too. For more in depth information see the german description.

Task:

The aim of this thesis is to develop an Approximate Model Counting based analysis for Java, using JBMC and adapting an existing analysis (e.g. ApproxFlow) for Java.

Prerequisits

Basic knowdledge on formal logic

Keywords

Static Analysis, Information Flow Control 

Publications

Publication

Model Counting Based Quantitative Information Flow for Unbounded Loops and Recursions

Advisors

Former Staff Member
M.Sc. Johannes Bechberger