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 |