TU Darmstadt / ULB / TUbiblio

Generierung von effizienten Security-/Safety-Monitoren aus modellbasierten Beschreibungen

Patzina, Lars (2014)
Generierung von effizienten Security-/Safety-Monitoren aus modellbasierten Beschreibungen.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Computer werden heute zunehmend durch kleine Recheneinheiten mit Sensoren zur Erfassung der Außenwelt ergänzt. Diese Recheneinheiten kommunizieren untereinander und mit externen Einheiten, um Informationen weiterzugeben und sich untereinander abzustimmen. Hierdurch findet auch eine Öffnung von sicherheitskritischen eingebetteten Systemen nach außen statt. Die Systeme können nun entweder direkt oder indirekt über zusätzliche Einheiten angegriffen werden.

Des Weiteren ist die auf eingebetteten Systemen eingesetzte Software durch beschränkte Ressourcen auf das Nötigste reduziert und bietet keine komplexen Sicherheitsmechanismen. Maßnahmen wie Testen von Software kann deren Fehlerfreiheit nicht sicherstellen. In realen Systemen ist zudem davon auszugehen, dass nicht bekannte Fehler existieren, die u.a. auch von Angreifern ausgenutzt werden können.

Die Laufzeitüberwachung solcher Systeme hat sich als geeignet erwiesen, um auch unbekannte Angriffe und Fehler zu erkennen. Zur Spezifikation solcher Laufzeitmonitore über Beschreibungen (Signaturen) von erlaubtem und verbotenem Verhalten haben sich viele verschiedene Spezifikationssprachen herausgebildet. Diese basieren auf verschiedensten Modellierungskonzepten. Zur Generierung von Monitoren aus diesen Spezifikationen in Software und Hardware müssen für die unterschiedlichen Sprachen verschiedenste Codegeneratoren erstellt werden. Des Weiteren besitzen einige der gewöhnlich verwendeten einfach zu verstehenden Spezifikationssprachen keine formalisierte Syntax und Semantik.

In dieser Arbeit wird zusammen mit [Pat14] der Model-based Security/Safety Monitor (MBSecMon)-Entwicklungsprozess vorgestellt. Dieser umfasst parallel zu dem eigentlichen Softwareentwicklungsprozess des zu überwachenden Systems die Spezifikation, die Generierung und die Einbindung von Laufzeitmonitoren.

Ziel dieser Arbeit ist die Definition einer formal definierten Zwischensprache zur Repräsentation stark verschränkter nebenläufiger Kommunikationen. Zu ihrer Entwicklung werden Anforderungen basierend auf existierenden Arbeiten aufgestellt. Auf Grundlage dieser Anforderungen wird die Zwischensprache Monitor-Petrinetze (MPN) entworfen und formal definiert. Diese Zwischensprache unterstützt die Repräsentation von Signaturen, die in verschiedensten Spezifikationssprachen modelliert sind, und die Generierung von effizienten Laufzeitmonitoren für unterschiedliche Zielplattformen. Die MPNs sind ein auf Petrinetzen basierender Formalismus, der um Konzepte der Laufzeitüberwachung erweitert wurde. Es wird gezeigt, dass die MPN-Sprache alle ermittelten Anforderungen an eine solche Zwischensprache, bis auf ein Hierarchisierungskonzept für Ereignisse, das in dieser Arbeit nicht behandelt wird, erfüllt.

Die MPN-Sprache wird in einem prototypischen Werkzeug zur Monitorgenerierung eingesetzt. Dieses unterstützt die MBSecMon-Spezifikationssprache [Pat14] als Eingabesprache und verwendet die MPN-Sprache als Zwischenrepräsentation zur Monitorgenerierung für verschiedenste Plattformen und Zielsprachen. Die generierten Monitore werden auf ihr Laufzeitverhalten und ihren Speicherverbrauch evaluiert. Es hat sich gezeigt, dass sich die MPN-Sprache trotz ihrer hohen Ausdrucksstärke zur einfachen Generierung effizienter Laufzeitmonitore für verschiedenste Plattformen und Zielsprachen eignet.

Typ des Eintrags: Dissertation
Erschienen: 2014
Autor(en): Patzina, Lars
Art des Eintrags: Erstveröffentlichung
Titel: Generierung von effizienten Security-/Safety-Monitoren aus modellbasierten Beschreibungen
Sprache: Deutsch
Referenten: Schürr, Prof. Dr. Andy ; Jürjens, Prof. Dr. Jan
Publikationsjahr: 2014
Ort: Darmstadt
Datum der mündlichen Prüfung: 10 Juli 2014
URL / URN: http://tuprints.ulb.tu-darmstadt.de/4133
Kurzbeschreibung (Abstract):

Computer werden heute zunehmend durch kleine Recheneinheiten mit Sensoren zur Erfassung der Außenwelt ergänzt. Diese Recheneinheiten kommunizieren untereinander und mit externen Einheiten, um Informationen weiterzugeben und sich untereinander abzustimmen. Hierdurch findet auch eine Öffnung von sicherheitskritischen eingebetteten Systemen nach außen statt. Die Systeme können nun entweder direkt oder indirekt über zusätzliche Einheiten angegriffen werden.

Des Weiteren ist die auf eingebetteten Systemen eingesetzte Software durch beschränkte Ressourcen auf das Nötigste reduziert und bietet keine komplexen Sicherheitsmechanismen. Maßnahmen wie Testen von Software kann deren Fehlerfreiheit nicht sicherstellen. In realen Systemen ist zudem davon auszugehen, dass nicht bekannte Fehler existieren, die u.a. auch von Angreifern ausgenutzt werden können.

Die Laufzeitüberwachung solcher Systeme hat sich als geeignet erwiesen, um auch unbekannte Angriffe und Fehler zu erkennen. Zur Spezifikation solcher Laufzeitmonitore über Beschreibungen (Signaturen) von erlaubtem und verbotenem Verhalten haben sich viele verschiedene Spezifikationssprachen herausgebildet. Diese basieren auf verschiedensten Modellierungskonzepten. Zur Generierung von Monitoren aus diesen Spezifikationen in Software und Hardware müssen für die unterschiedlichen Sprachen verschiedenste Codegeneratoren erstellt werden. Des Weiteren besitzen einige der gewöhnlich verwendeten einfach zu verstehenden Spezifikationssprachen keine formalisierte Syntax und Semantik.

In dieser Arbeit wird zusammen mit [Pat14] der Model-based Security/Safety Monitor (MBSecMon)-Entwicklungsprozess vorgestellt. Dieser umfasst parallel zu dem eigentlichen Softwareentwicklungsprozess des zu überwachenden Systems die Spezifikation, die Generierung und die Einbindung von Laufzeitmonitoren.

Ziel dieser Arbeit ist die Definition einer formal definierten Zwischensprache zur Repräsentation stark verschränkter nebenläufiger Kommunikationen. Zu ihrer Entwicklung werden Anforderungen basierend auf existierenden Arbeiten aufgestellt. Auf Grundlage dieser Anforderungen wird die Zwischensprache Monitor-Petrinetze (MPN) entworfen und formal definiert. Diese Zwischensprache unterstützt die Repräsentation von Signaturen, die in verschiedensten Spezifikationssprachen modelliert sind, und die Generierung von effizienten Laufzeitmonitoren für unterschiedliche Zielplattformen. Die MPNs sind ein auf Petrinetzen basierender Formalismus, der um Konzepte der Laufzeitüberwachung erweitert wurde. Es wird gezeigt, dass die MPN-Sprache alle ermittelten Anforderungen an eine solche Zwischensprache, bis auf ein Hierarchisierungskonzept für Ereignisse, das in dieser Arbeit nicht behandelt wird, erfüllt.

Die MPN-Sprache wird in einem prototypischen Werkzeug zur Monitorgenerierung eingesetzt. Dieses unterstützt die MBSecMon-Spezifikationssprache [Pat14] als Eingabesprache und verwendet die MPN-Sprache als Zwischenrepräsentation zur Monitorgenerierung für verschiedenste Plattformen und Zielsprachen. Die generierten Monitore werden auf ihr Laufzeitverhalten und ihren Speicherverbrauch evaluiert. Es hat sich gezeigt, dass sich die MPN-Sprache trotz ihrer hohen Ausdrucksstärke zur einfachen Generierung effizienter Laufzeitmonitore für verschiedenste Plattformen und Zielsprachen eignet.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Small processing units with sensors for the collection of environmental data increasingly complement classical computers. These units communicate with each other and with external units to propagate information and coordinate with other units. As a result, even safety-critical embedded systems open up to the outside world. These systems are now vulnerable to direct attacks and indirect attacks that are performed involving additional non-safety-critical units.

Software that is used on resource constrained embedded systems is typically reduced to the most necessary and does not include complex security mechanisms. Measures such as testing of software cannot ensure the absence of errors. In real systems, it can be assumed that errors exist that can be exploited by attackers.

Runtime monitoring of such systems has been proven to be effective to detect previously unknown attacks and failures. Many different languages have emerged that support the description of such specifications (signatures) of allowed and prohibited behavior. These languages support diverse modelling concepts. For the generation of monitors from these specifications in software and hardware, various code generators have to be developed. Additionally, some of the commonly used specification languages have no formal definition of their syntax and semantics.

This PhD thesis presents in conjunction with [Pat14], the \emph{Model-based Security/Safety Monitor (MBSecMon)} development process. The process is parallel to the actual software-development process of the system that should be monitored and includes the specification, the generation and the integration of runtime monitors.

The goal of this thesis is the design of a formally defined intermediate language for the representation of highly interleaved concurrent communications. Based on existing approaches the requirements for such an intermediate language are determined. On this basis, the intermediate language Monitor Petri nets (MPN) is designed and formally defined. This intermediate language supports the representation of signatures that are modeled in various specification languages and the generation of efficient runtime monitors for different target platforms. The MPNs are a formalism that is based on Petri nets and is extended with concepts for the domain of runtime monitoring. The MPN language completely fulfils the determined requirements except of a hierarchical concept for events, which is out-of-scope of this thesis.

A prototypical tool has been developed that supports the generation of runtime monitors. It supports the MBSecMon specification language [Pat14] as complex input language and uses the MPN language as intermediate representation for the generation of monitors for various target platforms and languages. The generated monitors are evaluated for their runtime behavior and their memory consumption. It becomes apparent that the MPN language despite its expressiveness is suited for the straightforward generation of efficient runtime monitors for various platforms and target languages.

Englisch
Freie Schlagworte: Monitor-Petrinetze, eingebettete Systeme, Petrinetze, MBSecMon, Safety, Security, Sicherheit, Laufzeitmonitor, modellbasiert, Modelltransformation, Codegenerierung
Schlagworte:
Einzelne SchlagworteSprache
Monitor Petri nets, embedded systems, Petri nets, MBSecMon, safety, security, run-time monitor, model-based, model transformation, code generationEnglisch
URN: urn:nbn:de:tuda-tuprints-41334
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften und Maschinenbau
Fachbereich(e)/-gebiet(e): 18 Fachbereich Elektrotechnik und Informationstechnik
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik > Echtzeitsysteme
LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
Zentrale Einrichtungen
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik
LOEWE
LOEWE > LOEWE-Zentren
Hinterlegungsdatum: 23 Nov 2014 20:55
Letzte Änderung: 23 Nov 2014 20:55
PPN:
Referenten: Schürr, Prof. Dr. Andy ; Jürjens, Prof. Dr. Jan
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 10 Juli 2014
Schlagworte:
Einzelne SchlagworteSprache
Monitor Petri nets, embedded systems, Petri nets, MBSecMon, safety, security, run-time monitor, model-based, model transformation, code generationEnglisch
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen