Nachweis umfassender Systemsicherheit

Sytemsicherheit

Neben der systematischen, Modell-basierten Erfassung von Sicherheitseigenschaften muss auch die Einhaltung dieser Sicherheitseigenschaften in der Implementierung sichergestellt ist. In KASTEL wurde deshalb ein Konzept für den Nachweis der modellbasierten Spezifikationen in der Implementierung erarbeitet. Des Weiteren werden Werkzeuge für den Nachweis der Sicherheitseigenschaften in den Implementierungen entwickelt.

Nachweis von Sicherheitseigenschaften in Java-Programmen

KASTEL entwickelt Methoden für die Übersetzung von Sicherheitsanforderungen im Modell in Spezifikationen für Java Programme. Diese Spezifikationen sind mit den Werkzeugen KeY und JOANA in den Implementierungen nachweisbar.

KeY ist ein deduktives Verifikationswerkzeug, das teilautomatisierte Sicherheitsbeweise für Java Quellcode ermöglicht. JOANA untersucht Java Bytecode mittels Programmabhängigkeitsgraphen auf Informationsflüsse.

Um zu verhindern, dass im Laufe der Systementwicklung die Spezifikation eines Systems und deren Implementierung auseinander entwickeln, forscht KASTEL an Möglichkeiten zur automatischen Konsistenzhaltung einer modellbasierten Spezifikation und der Implementierung die es erlauben, im Falle von architekturrelevanten Änderungen im Code das Modell mitevolvieren zu lassen.

Beteiligte Forschergruppen waren das Institut für Theoretische Informatik (ITI), sowie das Institut für Programmstrukturen und Datenorganisationen (IPD).

Ansprechpartner: Simon Greiner (ITI)Martin Hecker (IPD)Max Kramer (IPD)

Referenzen

  1. Max Kramer, Erik Burger, Michael Langhammer View-centric engineering with synchronized heterogeneous models Proceedings of the 1st Workshop on View-Based, Aspect-Oriented and Orthographic Software Modelling

Weiterführende Links

KeY

JOANA

Spezifikation und Nachweis komplexer Vertraulichkeitsanforderungen

Oftmals sind komplexe Informationsflußspezifikationen für Systeme notwendig um deren Sicherheit nachweisen zu können. KASTEL entwickelt daher das bestehende Werkzeug KeY weiter, so dass auch diese komplexen Anforderungen Werkzeuggestützt nachgewiesen werden können.

So ist es möglich für den Datenspeicher eines intelligenten Kameraüberwachungssystems den sicheren Informationsfluss zu formulieren und nachzuweisen. Hierbei tritt das sogenannte Tracking Paradox auf, das besagt, dass personenbezogene Daten erfasst werden müssen um diese schützen zu können. Gleichzeitig verändern sich über die Laufzeit die Anforderungen an den Schutz der Daten im System.

Des Weiteren wird an Methoden geforscht, die quantitative Aussagen über Informationsflüsse zulassen. So können Aussagen darüber getroffen werden, zu welchem Anteil Informationen über ein Eingabedatum erlangt werden können, wenn bestimmte Daten ausgelesen werden.

Beteiligte Forschergruppen waren das Institut für theoretische Informatik (ITI) sowie das Fraunhofer IOSB.

Ansprechpartner: Simon Greiner (ITI)Vladimir Klebanov (ITI)Pascal Birnstill (IOSB)Erik Krempel (IOSB)

Referenzen

  1. Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter Schmitt, Matthias Ulbrich Information Flow in Object-Oriented Software LOPSTR 2013: 23rd International Symposium on Logic-Based Program Synthesis and Transformation
  2. Simon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert, Jürgen Beyerer Privacy Preserving Surveillance and the Tracking-Paradox Future Security -- Security Research Conference 2013 (Future Security 2013)
  3. Vladimir Klebanov Precise Quantitative Information Flow Analysis -- A Symbolic Approach Theoretical Computer Science, Volume 538 (2014)

Sicherheitsnachweis für die Implementierung kryptografischer Protokolle

Real eingesetzte Systeme nutzen oft Verschlüsselungsmechanismen um die Geheimhaltung von Informationen zu gewährleisten. Implementierungen, die Verschlüsselung nutzen können nicht direkt von den oben beschriebenen Werkzeugen behandelt werden, da geheime Informationen in Chiffren zwar nicht mit vertretbarem Aufwand ausgelesen werden kann, aber trotzdem vorhanden ist.

Unter Verwendung passender kryptografische Annahmen ist der Nachweis von Sicherheitseigenschaften dennoch mit KeY und JOANA möglich. In KASTEL konnte dies für die Implementierung eines eVoting Systems gezeigt werden, sowie für eine sichere Mehrparteienberechnung, bei der die involvierten Parteien zwar den Wert einer Berechnung kennen dürfen, nicht jedoch die Eingaben der anderen Parteien.

Beteiligte Forschergruppen waren das Institut für Theoretische Informatik (ITI), sowie das Institut für Programmstrukturen und Datenorganisationen (IPD).

Ansprechpartner: Jürgen Graf (IPD)Simon Greiner (ITI)Martin Hecker (IPD)

Referenzen

  1. Ralf Küsters, Tomasz Truderung, Jürgen Graf A Framework for the Cryptographic Verification of Java-like Programs Computer Security Foundations Symposium (CSF), 2012 IEEE 25th
  2. Florian Böhl, Simon Greiner, Patrick Scheidecker Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-Honest Sender 13th International Conference on Cryptology and Network Security (CANS)