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

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.

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.