Information flow analysis of discrete embedded control system models
| dc.contributor.advisor | Glesner, Sabine | |
| dc.contributor.author | Mikulcak, Marcus | |
| dc.contributor.grantor | Technische Universität Berlin | en |
| dc.contributor.referee | Glesner, Sabine | |
| dc.contributor.referee | Hammer, Christian | |
| dc.contributor.referee | Slomka, Frank | |
| dc.date.accepted | 2019-11-06 | |
| dc.date.accessioned | 2020-06-24T11:41:34Z | |
| dc.date.available | 2020-06-24T11:41:34Z | |
| dc.date.issued | 2020 | |
| dc.description.abstract | Embedded systems used in safety-critical domains have to uphold strict safety and security requirements. At the same time, their complexity has been strongly increasing across application domains. To manage this rise in complexity, manufacturers have shifted towards model-driven development methodologies. While successful in managing the complexity in the development of large, interconnected systems, analysis and verification techniques for model-driven development methods and languages still have to reach a similar level of maturity as those for text-based imperative programming languages traditionally used in the development of safety-critical em bedded systems. In this thesis, we present an information flow analysis method for discrete embedded control system models, which has the potential to identify possible violations of both safety requirements and security policies by analyzing where and under which conditions information travels through a model. The main challenges such an information flow analysis faces are to (1) consider the specific semantics of the modeling languages, which heavily rely on concurrency and a complex notion of timing, and (2) relate the strongly different semantics of signal-flow-oriented and state-machine-based components, which comprise embedded control system models. Our major contribution is twofold: First, we provide an information flow analysis for the signal-flow-oriented components of an embedded control system model. The main idea of this analysis is that we only extract that information from an existing model which is required to analyze information flow in respect to both its timing and functionality. To this end, our technique captures timed path conditions, i.e., the precise control, data and timing conditions under which information flow is enabled as well as when and how these conditions are triggered. Second, we relate the inherently different semantics of the signal-flow-oriented and the state-machine-based components. To this end, we first translate the state-machine-based controller into a formally verifiable representation and, second, combine this representation with condition observer automata which we generate from the timed path conditions extracted in the first step of our method. This enables us to use the well-established technique of model checking to identify precisely the behavior that leads to the execution of information flow paths under analysis. To show the practical applicability of our approach, we have implemented it as a fully automatic and modular framework for MATLAB Simulink/Stateflow and Modelica, two widely used languages from the domain of embedded control systems, and applied our information flow analysis to two industrial case studies. In these case studies, we are able to verify integrity by checking that no information flow is possible from a non-critical to a critical component. | en |
| dc.description.abstract | Im sicherheitskritischen Bereich unterliegen eingebettete Systeme strengen Anforderungen an Ausfall- sowie Datensicherheit. Zugleich ist die Systemkomplexität in den vergangenen Jahren in allen Anwendungsbereichen stark gestiegen. Um diesem Anstieg zu begegnen, nutzen Hersteller modellgetriebene Entwicklungsansätze. Während Ansätze dieser Art bereits erfolgreich dazu genutzt werden, komplexe, miteinander verbundene Systeme zu entwickeln, haben Ansätze zur Analyse und Verifikation dieser Systeme noch nicht den Stand erreicht, den ähnliche Methoden für imperative Programmiersprachen aufweisen. In dieser Arbeit stellen wir eine Informationsflussanalyse für diskrete eingebettete Kontrollsystemmodelle vor, die es ermöglicht, Verletzungen von Ausfall- sowie Datensicherheitsanforderungen zu erkennen. Unsere Analyse verfolgt, wie und unter welchen Bedingungen Informationen durch ein Modell fließen. Die Herausforderungen in der Entwicklung einer solchen Analyse liegen in (1) der Berücksichtigung der spezifischen Semantik der Modellierungssprachen, welche auf komplexen zeitlichen Abhängigkeiten und Parallelität basieren, und (2) der Verbindung der stark heterogenen Semantiken der signalflussorientierten und jener auf Zustandsautomaten basierenden Komponenten, aus denen Kontrollsystemmodelle aufgebaut sind. Die vorliegende Arbeit leistet in diesem Gebiet zwei Beiträge. Zum einen eine Informationsflussanalyse für die signalflussorientierten Komponenten eines Kontrollsystemmodells. Diese Analyse basiert auf der Idee, nur diejenigen Informationen eines Modells zu extrahieren, die für die Analyse des Informationsflusses hinsichtlich des Zeitverhaltens und der Funktionalität des Modells relevant sind. Um dies zu ermöglichen, erfasst unser Ansatz timed path conditions, das heißt, diejenigen Bedingungen, die präzise das Kontroll-, Zeit-, und Datenverhalten abbilden,unter denen Informationsfluss stattfindet. Zum anderen schafft unsere Arbeit eine Verbindung zwischen den stark heterogenen Semantiken der signalflussorientierten und den auf Zustandsautomaten basierenden Komponenten. Unser Ansatz ermöglicht dies durch eine Übersetzung der Automaten in eine formal verifizierbare Darstellung, und die Kombination dieser Darstellung mit condition observer automata, welche wir aus den im ersten Schritt extrahierten timed path conditions generieren. Diese Verbindung der Semantiken ermöglicht uns, eine wohlfundierte Technik wie model checking zu nutzen, um genau das Verhalten des Zustandsautomaten zu identifizieren, welches zur Ausführung eines Informationsflusspfades führt. Um die Anwendbarkeit unseres Ansatzes unter Beweis zu stellen, präsentieren wir außerdem eine vollautomatische und modular aufgebaute Implementierung für M ATLAB Simulink/Stateflow und Modelica, zwei im Bereich sicherheitskritischer eingebetteter Software weit verbreitete Sprachen. Mithilfe dieser Implementierung konnten wir unseren Ansatz zur Informationsflussanalyse auf zwei Fallstudien aus dem industriellen Bereich anwenden. In beiden Fallstudien waren wir in der Lage, die Integrität kritischer Berechnungen sicherzustellen, indem wir Informationsfluss zwischen nicht-kritischen und sicherheitskritischen Komponenten ausschließen konnten. | de |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/11094 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-9984 | |
| dc.language.iso | en | en |
| dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en |
| dc.subject.ddc | 006 Spezielle Computerverfahren | de |
| dc.subject.other | MATLAB | en |
| dc.subject.other | simulink | en |
| dc.subject.other | stateflow | en |
| dc.subject.other | timed path conditions | en |
| dc.subject.other | verification | en |
| dc.subject.other | information flow analysis | en |
| dc.subject.other | zeitbehaftete Kontrollflussbedingungen | de |
| dc.subject.other | Verifikation | de |
| dc.subject.other | Informationsflussanalyse | de |
| dc.title | Information flow analysis of discrete embedded control system models | en |
| dc.title.translated | Informationsflussanalysen diskreter eingebetteter Regelkreise | de |
| dc.type | Doctoral Thesis | en |
| dc.type.version | acceptedVersion | en |
| tub.accessrights.dnb | free | en |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik::FG Software and Embedded Systems Engineering | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.group | FG Software and Embedded Systems Engineering | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |