Wintersemester 2014/15
Projektgruppe Event-Basierter Informationsfluss
Prof. Dr. Bernhard BeckertSimon Greiner
Ziel dieser Projektgruppe ist es, eine geeignete Definition von event-basiertem Informationsfluss für java Programme zu finden, sowie ein Werkzeug zu entwickeln das den Nachweis dieser Informationsflusseigenschaften ermöglicht.
Sicherheit ist ein aktuelles Thema, das insbesondere für Systeme relevant ist, die sensible Nutzerdaten verarbeiten. Während übliche Methoden sich hauptsächlich auf die Qualitätskontrolle von Designartefakten, sowie das Testen der fertigen Systeme konzentrieren, wäre ein Formaler Nachweis der Sicherheit einer Implementierung wünschenswert.
Eine solche Sicherheitseigenschaft ist der Informationsfluss in Systemen. In verteilten Systemen müssen Nachrichten zwischen den Teilsystemen kommuniziert werden um Informationen auszutauschen. Diese Nachrichten, oder Events, können von unterschiedlichen Personengruppen beobachtet oder auch versendet werden. In einem sicheren System lassen diese Beobachtungen jedoch keinen Rückschluß auf geheime Informationen zu.
Die Projektteilnehmer müssen sich in event-basierte Non-Interference Begriffe, sowie deren Unterschiede einarbeiten, eine geeignete Formalisierung in Dynamischer Logik entwickeln, sowie das Verifikationswerkzeug KeY so erweitern, dass ein Nachweis der entwickelten Sicherheitseigenschaft ermöglicht wird.
Voraussetzungen
- Interesse an Theoretischer Informatik, Programmverifikation und Security
- Interesse an Formalen Systemen und Logik
- Vorlesung Formale Systeme
- Grundlagen Java
Bei Interesse bitte per E-Mail bei Simon.GreinerFbp1∂kit edu melden.