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.

## 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