Informationsflusskontrolle (IFC) untersucht, ob ein Angreifer aus öffentlichen Ausgaben eines Programms Rückschlüsse auf geheime Eingaben ziehen kann. Manchmal müssen Programme zur Erfüllung ihrer Aufgaben aber geringe Mengen an Information herausgeben, beispielsweise in einer Passwortüberprüfung. In der quantitativen IFC wird daher untersucht, wie viel Information über die geheimen Eingaben ein Angreifer aus den öffentlichen Ausgaben gewinnen kann. Üblicherweise wird dafür ein Entropie-Maß zugrunde gelegt und der Informationsfluss in Bit angegeben.
Für C existieren bereits mehrere Analysen (z.B. ApproxFlow, Scalable Approximation of Quantitative Information Flow in Programs) die auf Approximate Model Counting basieren. Dabei wird typischerweise mit Hilfe von einem Tool wie CBMC eine SAT-Formel für ein gegebenes Programm erzeugt und dann evaluiert, wie oft diese erfüllbar ist. Damit kann in gewissen Grenzen eine gute Approximation für den Informationsfluss gefunden werden.
Mit JBMC existiert ein relativ neues Werkzeug, dass es ermöglicht auch für Java SAT-Formeln zugenerieren. Mit kleinen Adaptionen kann ApproxFlow hierauf adaptiert werden. Diese Adaption ist zur Zeit noch einfach und kann nur mit einfachen Programmen, die am Ende eine öffentliche Ausgabe haben, umgehen.

Aufgabe:

Ziel dieser Arbeit ist eine auf Approximate Model Counting (konkret dem Paper zu ApproxFlow) basierte Analyse für Java zu entwickeln, welche zusätzlich

• öffentliche und private Ausgaben via System.out.println(),
• öffentliche Eingaben
• kontextabhängige Ausrolltiefen für Schleifen

unterstützt.

Voraussetzungen

Grundlagen Formaler Logik (z.B. durch die Vorlesung Formale Systeme) sind hilfreich

Schlüsselworte

Statische Analyse, Informationsflusskontrolle 

Veröffentlichungen

Veröffentlichung

Model Counting Based Quantitative Information Flow for Unbounded Loops and Recursions

Betreuer

Ehemalige Mitarbeiter
M.Sc. Johannes Bechberger