TU Darmstadt / ULB / TUprints

Entwicklung einer Spezifikationssprache zur modellbasierten Generierung von Security-/Safety-Monitoren zur Absicherung von (Eingebetteten) Systemen

Patzina, Sven (2014)
Entwicklung einer Spezifikationssprache zur modellbasierten Generierung von Security-/Safety-Monitoren zur Absicherung von (Eingebetteten) Systemen.
Technische Universität
Ph.D. Thesis, Primary publication

[img]
Preview
Text
20141119_Thesis_SvenPatzina_Final.pdf
Copyright Information: CC BY-NC-ND 2.5 Generic - Creative Commons, Attribution, NonCommercial, NoDerivs .

Download (5MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Entwicklung einer Spezifikationssprache zur modellbasierten Generierung von Security-/Safety-Monitoren zur Absicherung von (Eingebetteten) Systemen
Language: German
Referees: Schürr, Prof. Dr. Andy ; Jürjens, Prof. Dr. Jan
Date: 31 January 2014
Place of Publication: Darmstadt
Date of oral examination: 10 July 2014
Abstract:

Getrieben durch technische Innovationen gewinnt die Kommunikation zwischen eingebetteten Systemen immer mehr an Bedeutung. So kommunizieren heutzutage nicht nur PCs über lokale Netzwerke oder das Internet, sondern auch mobile Geräte wie Smartphones und Tablets erobern den Markt. Diese bieten aufgrund ihrer geringeren Rechenleistung neue Angriffsflächen, da Sicherungsmaßnahmen der PC-Domäne nicht ohne Anpassung anwendbar sind. Durch die Vernetzung dieser mobilen Geräte mit Fahrzeugen und die Anbindung der Fahrzeuge an externe Dienstleistungen sind selbst eingebettete Systeme im Fahrzeug, die sicherheitskritische Aufgaben erfüllen, nicht mehr vollständig von der Außenwelt abgeschirmt. Bei ihrer Entwicklung wurde jedoch wenig Aufmerksamkeit auf Sicherheitsmechanismen, wie Verschlüsselung und sicheres Komponentendesign, zur Abwehr von Angriffen aus der Außenwelt gelegt. Solche Fahrzeuge sind hierdurch von außen für aktive und passive Angriffe anfällig. Selbst wenn bei einer Neuentwicklung eines eingebetteten Systems großer Wert auf die Absicherung gelegt wird, ist es meist nicht möglich, alle Sicherheitslücken zu eliminieren und jeden möglichen Angriff vorherzusehen. Betrachtet man komplexe heterogene Systeme oder Komponenten und will diese nachträglich absichern, ist dies meistens ökonomisch oder technisch nicht zu realisieren. Resultierend daraus kann bei keinem System davon ausgegangen werden, dass es sicher ist -- sei es durch unbekannte Schwachstellen oder der Verwendung von Legacy-Komponenten. Um Systeme dennoch gegen Angriffe, die vorher unbekannte Fehler und Sicherheitslücken ausnutzen, absichern zu können, hat sich die Überwachung eines Systems während der Laufzeit als geeignet herausgestellt.

Eine solche Absicherung wird durch den in dieser Dissertationsschrift und in [Pat14] vorgestellten verständlichen Model Based Security/Safety Monitor-Entwicklungsprozess (MBSecMon-Entwicklungsprozess) erreicht, der sich in bestehende modellbasierte Systementwicklungsprozesse nahtlos eingliedert. Dieser MBSecMon-Entwicklungsprozess generiert aus einer in der Anforderungsphase entstandenen Spezifikation automatisch effiziente Sicherheitsmonitore für hoch nebenläufige Kommunikationen.

Diese Arbeit betrachtet zwei Schritte dieses Entwicklungsprozesses. Der erste Teil der Arbeit stellt eine neue auf dem szenariobasierten Design aufbauende graphische, modellbasierte Signaturbeschreibungssprache vor - die MBSecMon-Spezifikationssprache. Diese Sprache vereinigt die Vorteile bestehender Formalismen, indem sie (1) alle wichtigen Konzepte zur Modellierung von verhaltensbeschreibenden Signaturen für hoch nebenläufige Kommunikationsabläufe unterstützt und diese kompakt repräsentieren kann. Sie bezieht (2) bestehende Entwicklungsartefakte des Systementwicklungsprozesses in die Modellierung ein, (3) befindet sich auf einer höheren Abstraktionsebene als üblicherweise zur Spezifikation eingesetzte Sprachen und unterscheidet explizit zwischen Normalverhalten und bekannten Angriffsmustern und -klassen. Durch diese Unterscheidung und durch Nähe der Sprache zur UML wird (4) eine hohe Verständlichkeit der Spezifikation sowohl für den Softwaretechniker als auch für Nicht-Experten erreicht.

Den zweiten Teil dieser Arbeit bildet die Abbildung der sehr kompakten in der MBSecMon-Spezifikationssprache verfassten Spezifikationen in die formale Zwischensprache Monitor-Petrinetze [Pat14]. Hierdurch wird zum einen die Semantik der MBSecMon-Spezifikationssprache formalisiert und zum anderen der im MBSecMon-Entwicklungsprozess eingesetzte automatische Übergang in eine für die Generierung effizienter Monitore besser geeignete Repräsentation realisiert.

Alternative Abstract:
Alternative AbstractLanguage

Driven by technical innovation, embedded systems are becoming increasingly interconnected. Nowadays, not only PCs communicate by local networks or the Internet, but also mobile devices, such as smart phones and tablets, capture the market. These mobile devices offer a new target for attacks because their limited processing power prevents the direct adaptation of protection mechanisms used within the PC domain. By linking these mobile devices with vehicles and by introducing new connectivity between vehicles and external services, even embedded in-vehicular systems that perform safety-critical tasks are no longer completely isolated from the outside world. Often, little attention has been paid to security mechanisms of these embedded systems, such as encryption and safe component design for protection against attacks. Caused by this development, the embedded systems in vehicles become vulnerable for active and passive attacks from the outside world. Even if safety and security issues are considered during the development of an embedded system, in the majority of cases it is impossible to eliminate all security vulnerabilities and to foresee all possible attacks. Considering complex heterogeneous systems or components, it is often economically or technically infeasible to secure them against external adversaries retroactively. Therefore, systems cannot be considered as safe, either due to unknown vulnerabilities, or due to the required integration of legacy components. To secure such systems, monitoring the system at runtime is proven able to detect attacks that exploit previously unknown errors and security vulnerabilities.

Such a protection is reached by the Model Based Security and Safety Monitor (MBSecMon) development process presented in this PhD thesis and in [Pat14]. The MBSecMon-Process integrates seamlessly into existing system development processes and generates automatically efficient safety and security monitors for highly concurrent communication processes based on specifications from the requirement phase.

This PhD thesis focuses on two steps of this development process. The first part of this thesis presents a new graphical, model-based signature description language that is based on the scenario driven approach - the MBSecMon Specification Language. This language combines the advantages of existing formalisms by (1) providing all essential concepts for modeling behavioral signatures for highly concurrent communication processes and enables their compact representation. It (2) takes advantage of existing development artifacts in the modeling of the signatures, (3) is located on a higher abstraction level as commonly used languages and distinguishes explicitly between standard behavior and attack patterns and classes. By this explicit distinction and its resemblance to the UML, the language achieves (4) a high comprehensibility for software engineers as well as for non-experts.

The second part of this thesis presents the transformation of the compact specification, which is modeled in the MBSecMon specification language, into the formal intermediate language Monitor Petri nets. This transformation formalizes, on the one hand, the semantics of the MBSecMon specification language and provides, on the other hand, the automatic transformation in the MBSecMon development process to a more suitable representation for the generation of efficient monitors.

English
Uncontrolled Keywords: MBSecMon, Signaturbeschreibungssprache, Sequenzdiagramme, Use-Case, Misuse-Case, Safety, Security, Sicherheit, Laufzeitmonitor, Modellbasiert, Generierung, Live Sequence Charts, LSC, Modelltransformation
Alternative keywords:
Alternative keywordsLanguage
MBSecMon, signature description language, sequence diagrams, use case, misuse case, safety, security, run-time monitor, model-based, generation, Live Sequence Charts, LSC, model transformationEnglish
URN: urn:nbn:de:tuda-tuprints-41327
Classification DDC: 000 Generalities, computers, information > 004 Computer science
600 Technology, medicine, applied sciences > 620 Engineering and machine engineering
Divisions: 18 Department of Electrical Engineering and Information Technology
18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems
LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
Date Deposited: 21 Nov 2014 08:38
Last Modified: 21 Nov 2014 08:38
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/4132
PPN: 386759758
Export:
Actions (login required)
View Item View Item