Beweisbare Sicherheit für komplexe IT-Systeme

Server

Modell-basierte Plausibilitätsprüfung 

Die klassische Fehler- und Angriffserkennung in Energienetzen analysiert das informationstechnische System auf nicht plausible Kommunikationsflüsse. Dabei werden jedoch nur lokale Manipulationen des Energienetzes erkannt. Dies führt dazu, dass in dezentral verwalteten Energienetzen sowohl die Gefahr von inselnetzübergreifenden Angriffen als auch die Abhängigkeit zwischen den Inselnetzen steigt.

 

 

Die Modellierung der Inselnetze enthält nicht nur das informationstechnische System, sondern auch die Energie-, Stoff- und Wärmeströme (Gesamtnetz). Die auf den Modellen basierende Plausibilitätsprüfung kann nun Unstimmigkeiten zwischen den ausgetauschten Daten und den daraus resultierenden Veränderungen im Verhalten des Energienetzes aufdecken und je nach Gefährundungsbeurteilung Meldung geben oder Alarm schlagen. 

 

Beweisbare Sicherheit für komplexe IT-Systeme

Absolute Sicherheit kann für ein System nur dann erreicht werden, wenn die domänenspezifischen Sicherheitseigenschaften auf einer Ebene entwickelt werden, in der sichergestellt werden kann, dass die spezifizierten und die überprüften Sicherheitseigenschaften miteinander kompatibel sind.

Die Systeme werden dabei nicht komplett neu entwickelt sondern bauen auf bereits existierende Systemen und Funktionalitäten auf. Daher stellt die Integration unterschiedlicher Entwicklungsphasen eine besondere Herausforderung dar. Des Weiteren ist es notwendig, dass die Sicherheit eines Systems über den gesamten Lebenszyklus hinweg betrachtet wird. Hierfür ist ein fundiertes Risiko- und Sicherheitsmanagement notwendig, das auf einer grundlegenden Systemtheorie aufbaut, bestehend aus Analysen von Gefährdungen von Schutzgütern, Angreifermodellen und geeigneten Schutzprozessen, -konzepten und -mechanismen.

Beteiligte Forschungsgruppen sind das Institut für theoretische Informatik (ITI) und das Institut für Programmstrukturen und Datenorganisation (IPD).

 

Komponierbare Sicherheit

 

Absolute Sicherheit ist schwer zu beweisen, da nur Fälle abgedeckt werden können, die man sich auch vorstellen kann. Um den Begriff der Sicherheit fassbar zu machen, werden Sicherheitsmodelle entwickelt, welche die Möglichkeiten von Angreifenden formal beschreiben. Des Weiteren wird genau definiert, was es bedeutet, ein gegebenes Verfahren zu brechen. Ein gegebenes kryptographisches Verfahren ist für ein Sicherheitsmodell ausreichend sicher, wenn AngreiferInnen es nur mit vernachlässigbar kleiner Wahrscheinlichkeit brechen können.

 

Bei KASTEL wird nach den Aspekten der komponierbaren Sicherheit geforscht. Dabei wird untersucht, inwiefern das Zusammenfügen einzelner in sich bewiesener Komponenten zu einem sicheren Gesamtsystem führt. Des Weiteren wird an aggregierbaren Signaturverfahren gearbeitet. Dabei handelt es sich um Verfahren, um die Signaturen und mehreren Nachrichten in eine einzelne Signatur umzuwandeln und damit Bandbreite beim Transport zu sparen. 

Beteiligte Forschungsgruppe ist das Institut für theoretische Informatik (ITI).

 

Systemtheorie

Bei KASTEL wird an einer grundlegenden Systemtheorie geforscht, die eine durchgängige und gesamtheitliche Sicherheitsbetrachtung von der Gefährdungsanalyse, über die Anforderungserstellung bis hin zur Verifikation der integrierten Mechanismen auf Implementierungsebene ermöglicht. Ein besonderer Fokus der rechtlichen Perspektive wird auf die Integration von gesetzlichen Vorabwägungen bei Wertkollisionen, beispielsweise zur Bewertung von Schutzgütern, gelegt. Dies trägt zur Sicherung von Rechtskonformität in Abwägungsprozessen bei, die bisher größtenteils eine alleinige Domäne der Informatik war. Hierfür arbeiten unterschiedlichste Forschungsdisziplinen zusammen an disziplinübergreifenden Lösungen. 

Beteiligte Forschungsgruppen sind das Zentrum für angewandte Rechtswissenschaften (ZAR) sowie das Fraunhofer IOSB.

 

Tool-Unterstützung im Entwicklungsprozess

Im Rahmen von KASTEL wird ein modellgetriebenes Spezifikationsverfahren zur Erhebung und Dokumentation von Sicherheitsanforderungen für Systeme entwickelt.

 

Es wird untersucht, wie diese Sicherheitsanforderungen aus der Modellebene semantisch korrekt auf Teilsysteme verteilt und so auf konkrete Implementierungen abgebildet werden können. So kann deren Sicherheit direkt in der Implementierung nachgewiesen werden. Darauf aufbauend entwickelt KASTEL Werkzeuge und Methoden zur Analyse, Verifikation und Integration von Source- und Bytecode, um die Stärken unterschiedlicher Ansätze möglichst gewinnbringend zu vereinen. Drei Werkzeuge werden hierbei kombiniert: Palladio ist ein Architekturwerkzeug, das es erlaubt, Software mit bestimmten Qualitätseigenschaften zu erzeugen. JOANA untersucht Java-Programme auf sequentielle und probabilistische Lecks in Informationsflüssen. KeY ermöglicht es, formal zu verifizieren, dass ein Java-Programm bestimmte Eigenschaften erfüllt. 

Beteiligte Forschungsgruppen sind der Lehrstuhl für Programmierparadigmen (IPD) sowie das Institut für theoretische Informatik (ITI)