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

Scientific Staff |
---|

Johannes Bechberger |