Dies ist das Thema des Projekts „Validation Using Modelling“, das von Airbus über Tutech finanziert wird. Das Projekt wurde vom Institut für sichere cyber-physische Systeme der Technischen Universität Hamburg unter der Leitung von Prof. Sibylle Fröschle durchgeführt. In drei Phasen, von Oktober 2022 bis Januar 2026, wurden eine Fallstudie und eine entsprechende Methodik für „TAGA: ein Touch-and-Go-Assistent im Luft- und Raumfahrtbereich“ entwickelt. Der Weg zur Zertifizierung ist nun vorgezeichnet.
Wenn ein Flugzeug gelandet ist und seinen Parkplatz am Zielflughafen erreicht hat, werden viele Bodenprozesse wie Betanken und Vorkonditionierung durchgeführt. Derzeit werden standardisierte Verfahren ausgeführt, die manchmal noch papierbasiert sind. Die Maschine-zu-Maschine-Kommunikation über drahtlose Netzwerke kann diese Prozesse in Bezug auf Energieeffizienz, Sicherheit und Zeitaufwand verbessern. Das Flugzeug sendet Sensordaten wie Kraftstoff- oder Temperaturmesswerte an die Bodeneinheit, die die Steuerung des Prozesses entsprechend anpasst. Um einen sicheren Datenaustausch zu gewährleisten, wird die Kommunikation kryptografisch authentifiziert und verschlüsselt. Es bleibt jedoch die Frage: Wie lassen sich die erforderlichen kryptografischen Schlüssel sicher erstellen?
Der Ansatz hinter TAGA besteht darin, dass ein menschlicher Bodenoperator die Bodeneinheit und das Flugzeug mithilfe eines Near Field Communication (NFC)-Systems koppeln kann. NFC ist eine drahtlose Kommunikationstechnologie mit kurzer Reichweite, die hinter vielen alltäglichen Anwendungen steht. Beispielsweise ermöglicht NFC bei kontaktlosen Zahlungen die Durchführung von Zahlungsvorgängen, indem eine Karte oder ein Smartphone an ein Zahlungsterminal gehalten wird. Bei TAGA ist jede Bodeneinheit und jedes Flugzeug mit einem NFC-Lesegerät ausgestattet, und der Bediener erhält eine NFC-Karte.
Während der physischen Einrichtung des Bodenprozesses geht der Bediener in der Regel von der Bodeneinheit zum Flugzeug und zurück, z. B. um einen Versorgungsschlauch anzuschließen. Auf diesem Weg tippt der Bediener
mit seiner Karte auf die NFC-Lesegeräte und ermöglicht so einen Austausch von kryptografischen Nachrichten zwischen den Maschinen zur Schlüsselerstellung.
Die entsprechende Verifizierungsmethodik folgt dem modernen Ansatz der nachweisbaren Sicherheit: Sie stützt sich nicht nur auf die Prüfung des Systems anhand einer Reihe von Bedrohungsszenarien, sondern legt Sicherheits- und Ausfallsicherheitseigenschaften für alle Kombinationen eines detaillierten Angreifer-Modells fest. Dazu werden die zugrunde liegenden kryptografischen Protokolle modelliert und
mit formalen Methoden und einem halbautomatischen Tool, dem Tamarin Prover, verifiziert. Darüber hinaus haben wir über die klassische Protokollverifizierung hinaus Anforderungen integriert, die speziell auf die cyber-physische Natur der Umgebung zugeschnitten sind, sowie Widerstandsfähigkeitseigenschaften, die den internationalen Kontext der Flughafenumgebung berücksichtigen. Diese bieten Sicherheitsgarantien, selbst wenn das System teilweise kompromittiert ist, und mindern durch ihre Konzeption das Risiko im Falle einer Sicherheitsverletzung.
Autor:
Prof. Sibylle Fröschle
Hamburg University of Technology
Institute for Secure Cyber-Physical Systems
Phone: 040 30601- 4681
sibylle.froeschle(at)tuhh(dot)de
https://www.tuhh.de/scps/startseite
