SATiSFy

Frühzeitige Validierung von Safety- und Security-Anforderungen in autonomen Fahrzeugen

01.05.2018 bis 31.07.2021

Mit dem Einzug des autonomen Fahrens in zukünftigen Automobilgenerationen wird eine Vielzahl von komplexen Systemkomponenten in eine Wirkungskette gebracht – ein jegliches Fehlverhalten des Systems kann dabei lebensbedrohlich sein. Potentielle Angriffe von außen stellen daher eine besondere Bedrohung für diese Systeme dar, so dass jegliche Safety- und Security-Anforderungen unbedingt in Kombination betrachtet werden müssen. Da klassische Entwicklungsprozesse hierfür unzureichend sind, müssen mittels formaler Methoden frühzeitig im Entwicklungsprozess Sicherheitsgarantien integriert werden, mit denen Komponenten einzeln und in ihrer Komposition validiert werden können. Ziel des Vorhabens SATisFy ist es, Techniken zur formalen Erfassung und frühzeitigen Verifikation für Systeme zum autonomen Fahren zu entwickeln, um die notwendigen Security- und Safety-Anforderungen im Ansatz sowohl auf Hardware- als auch auf Softwareebene gesamtheitlich zu spezifizieren, zu visualisieren und sie insbesondere vor einem abschließenden Integrationstest bereits formal validieren zu können.

Die Universität Tübingen wird primär Methoden zur frühzeitigen Verifikation von Hardware-basierten Safety- und Security-Maßnahmen erforschen, die im Betrieb im Entwurf festgelegte Constraint-Korridore auswerten. Nach einer Analyse möglicher Bedrohungsszenarien und der Bestandsaufnahme existierender Designmechanismen für Security-Architekturen erfolgt eine Formalisierung von Sicherheitsanforderungen, um zur Entwurfszeit geeignete Constraint-Korridore zu bestimmen. UT befasst sich des Weiteren mit einer Methodik zur Anomalieanalyse sowie zur systematischen Bestimmung applikationsspezifischer Sicherheitskorridore im Entwurf. Ferner werden geeignete Online-Monitore sowie ein Security-Controller entwickelt, um Anomalien im Betrieb zu detektieren und geeignete Gegenmaßnahmen automatisiert einleiten zu können. Die Evaluierung der Projektergebnisse erfolgt anhand eines realen Demonstrators.