UnivIS
Informationssystem der Friedrich-Alexander-Universität Erlangen-Nürnberg © Config eG 
FAU Logo
  Sammlung/Stundenplan    Modulbelegung Home  |  Rechtliches  |  Kontakt  |  Hilfe    
Suche:      Semester:   
 Lehr-
veranstaltungen
   Personen/
Einrichtungen
   Räume   Forschungs-
bericht
   Publi-
kationen
   Internat.
Kontakte
   Examens-
arbeiten
   Telefon &
E-Mail
 
 
 Darstellung
 
Druckansicht

 
 
Einrichtungen >> Technische Fakultät (TF) >> Department Informatik (INF) >> Lehrstuhl für Informatik 11 (Software Engineering) >>
SMARTEST: Evaluierung von Verfahren zum Testen der Informationssicherheit in der nuklearen Leittechnik durch smarte Testfallgenerierung / Teilvorhaben: Modellbasierte Teststrategien

Ziel des SMARTEST-Verbundvorhabens ist, zukünftig möglichst viele Schwachstellen in nuklearen Leittechniksystemen mit Hilfe intelligenter Testverfahren aufzeigen zu können. Durch Behebung der erkannten Schwachstellen kann die Angriffsfläche für IT-basierte Angriffe entsprechend reduziert werden. Primär soll dadurch das Risiko kritischer Störfälle auch im Hinblick auf systematische IT-Angriffe gesenkt werden.

Anhand zu definierender Angriffsszenarien sind hierzu geeignete Modellnotationen auszuwählen, die diese Szenarien auf einer adäquaten Abstraktionsebene zu erfassen erlauben. Anschließend sind auf der Basis der erstellten Modelle pro Angriffsszenario Testziele zu ermitteln und zu formalisieren, deren Erfüllung die erfolgreiche Erkennung vorliegender IT-Schwachstellen zu belegen erlauben. Bei Nichterfüllung sind Metriken zur Quantifizierung des bereits erreichten Erfüllungsgrads zu identifizieren, die den bis dahin erzielten Testfortschritt signifikant zu erfassen erlauben. Mittels der dadurch messbaren Testendekriterien soll eine optimale Testdatengenerierung automatisch gesteuert erfolgen.

Die durchgeführten Arbeiten betrafen folgende Zielsetzungen:

Systematische Identifizierung von Angriffsszenarien und Klassifizierung von Angriffsstrategien.
Im Rahmen dieses Arbeitspakets wurden angriffsspezifische Wissensanforderungen in Bezug auf die zugrundeliegenden Wissensdomänen klassifiziert:
-Kommunikation: Netzwerktopologie und Netzwerkprotokoll;
-Technische Anwendung: Lage und Bedeutung von Sensoren und Aktoren;
-Digitale Steuerung: funktionale Anforderungen an die Steuerungslogik, Syntax und Semantik der ausgetauschten Signale;
-Software: Quell- und Maschinencode, einschließlich potentieller Schwachstellen derselben.
Angesichts der vor allem softwaretechnisch geprägten Kenntnisse und Erfahrungen des Verbundpartners FAU-SWE wurden hier vor allem die beiden zuletzt genannten Domänen in die weiteren Betrachtungen herangezogen. Dabei wurde von einem voll informierten und an Entwurfs- und Entwicklungsentscheidungen beteiligten Insider-Angreifer ausgegangen, der über Expertise und Wissen in allen erwähnten Bereichen verfügt.

Auf der Basis dieser Überlegungen wurden die folgenden, zueinander orthogonalen Angriffsmuster identifiziert:

Nachrichtenmanipulation: Gezielte Verfälschung der Information über den aktuellen Zustand der zu steuernden technischen Anlage anhand zu diesem Zweck manipulierter Sensorwerte; dadurch kann eine unter den gegebenen Bedingungen unangebrachte, unter Umständen unsichere leittechnische Reaktion hervorgerufen werden. Im Rahmen dieses Arbeitspakets wurde eine beispielhafte Automatisierungssoftware im Hinblick auf den von ihr zu bearbeitenden Nachrichtenstrom untersucht. Insbesondere wurden Klassen von Anforderungen an den legalen Nachrichtenstrom identifiziert und charakterisiert.

Versetzte Ausführung von Maschinenbefehlen: Gezielte Verfälschung der Interpretation der Maschinenbefehle anhand speicherzellenversetzter Ausführung des Maschinencodes; dadurch lässt sich eine vom ursprünglich geplanten Verhalten abweichende Reaktion hervorrufen. Voraussetzung hierbei ist die Verwendung einer CISC-Rechnerarchitektur, die den Einsatz von Befehlswörtern variabler Länge unterstützt. Dadurch lässt sich der Beginn eines jeden Befehlswortes nicht einfach durch Abstandsvergleich überprüfen; vielmehr kommt jede Zelle grundsätzlich als potentieller Anfang eines Maschinenbefehlswortes in Frage. Mit anderen Worten kann der gleiche Maschinencode verschiedene Interpretationen zulassen, je nachdem auf welche Speicherzelle der Befehlszähler zeigt. Dadurch wird die Ausführung illegaler, durch Sprünge verketteter Codestücke unterstützt. Hierzu erforderlich ist eine Umleitung des Befehlszählers auf die Anfangsadresse des ersten illegalen Fragments. Folgende existierende Umleitverfahren wurden identifiziert:
-Pufferüberlauf: Überschreiben der Rücksprungadresse mit der Anfangsadresse eines illegalen Codefragments mittels Pufferüberlauf;
-Format strings: Verwendung spezieller Formatfunktionen (z.B. printf) mit anschließender Angabe des Formatindikators %n zur Überschreibung der Rücksprungadresse mit der Anfangsadresse eines illegalen Codefragments;
-Nichtinitialisierte Variablen: Verwendung deklarierter Variablen bevor ihnen ein bestimmter Wert zugewiesen wurde. In einigen Programmiersprachen (darunter C) werden nichtinitialisierte Variablen zu den Werten ausgewertet, die in den von diesen Variablen referenzierten Zellen gerade gespeichert sind. Dadurch lassen sich etwa Rücksprungadressen betrachteter Funktionen überschreiben.

Anschließend wurde untersucht, inwieweit sich das Potential für das Vorliegen einer Schwachstelle dieses Typs im Vorfeld statisch einschätzen lässt. Hierzu wurde die Angriffsfläche eines potentiellen Angriffs dieses Typs anhand der formalen Unterteilung der gesamten Menge der den Programmcode enthaltenden Speicherzellen in folgende drei paarweise disjunkte Klassen modelliert:
-Menge regulärer Zellen, wo ein gutartiger (korrekt geplanter) Maschinenbefehl beginnt;
-Menge irregulärer Zellen, wo ein nicht gutartiger, evtl. ausführbarer Maschinenbefehl beginnt;
-Menge ungültiger Zellen, wo kein Maschinenbefehl beginnt.
Diese formale Klassifikation bietet eine Modellierungssprache an, die als Grundlage für eine kompakte und ausdrucksstarke Erfassung relevanter Aspekte des Angriffsverhaltens nutzbar ist. Zur Umsetzung dieser Klassifikation wurden die folgenden beiden statischen Ansätze an einem konkreten Beispiel erprobt und verglichen:
-manuelle syntaktische Analyse, welche jede Speicherzelle - im Zusammenhang mit einer gewissen Anzahl ihr unmittelbar nachfolgender Zellen - auf Einhaltung maschinensprachensyntaktischer Bedingungen überprüft; infolge des damit verbundenen Aufwandes ist dies u.U. nur ansatzweise realistisch;
-automatische Disassemblierung, welche analoge Überprüfungen vollautomatisch durchführt, indem für jede Speicherzelle der Programmcodeteil betrachtet wird, der dort beginnt, und durch den Versuch einer Rückübersetzung ermittelt wird, inwieweit sich (zumindest anfänglich) interpretierbare Befehle ergeben.
Angesichts seiner Automatisierbarkeit konnte sich letzterer Ansatz durchsetzen. Darüber hinaus lässt sich hiermit auch feststellen, inwieweit mehrere interpretierbare Codefragmente durch unbedingte, direkte Sprünge miteinander verkettet sind, was die Vermutung einer absichtlichen Konstruktion bösartigen Codes nahelegen könnte.

Provozieren eines Überlaufs: Gezieltes Überschreiben nicht zulässiger Speicherbereiche durch Überlaufeffekte; dadurch kann eine Verfälschung von Daten bis hin zu einer Ausführung von bösartigem Code hervorgerufen werden. In diesem Zusammenhang wurden existierende Integer Constraints Analysen im Hinblick auf ihre Signifikanz für eine anschließende dynamische Analyse näher untersucht mit dem Ziel, relevante Informationen daraus zu extrahieren, die das Erkennungspotential anschließender Testverfahren bestmöglich zu optimieren erlauben. Die vorausgehende statische Analyse unterstützt sowohl die Eingrenzung der anschließenden dynamischen Analyse auf schwachstellenrelevante Codeteile als auch die Ermittlung logischer Bedingungen (Constraints), deren Erfüllung für das Eintreten eines Überlaufs (bzw. eines Unterlaufs) notwendig bzw. hinreichend ist. Im besonderen Fall der Allgemeingültigkeit bzw. Nicht- Erfüllbarkeit solcher Prädikate lassen sich ohne weiteren Testbedarf grundsätzliche Aussagen hinsichtlich des Eintretens bzw. Nicht-Eintretens von Überläufen (bzw. Unterläufen) im Betrieb systematisch herleiten. Im Allgemeinen ist von einer statischen Herleitbarkeit definitiver Aussagen nicht auszugehen; in solchen Fällen ist es erforderlich, anhand anschließender intelligenter Tests die Erfüllbarkeit der statisch ermittelten Constraints dynamisch zu untersuchen. Hierzu können etwa heuristische (z.B. evolutionäre) Optimierungsverfahren Anwendung finden, die die Chancen von Über- (bzw. Unter-) Laufeffekten zu maximieren bezwecken.

Als Hauptergebnis der bisherigen Untersuchung ist ein neuartiger Verifikationsansatz zu verzeichnen, der durch Kombination von
-aus der Literatur bekannten statischen Ansätzen und
-aus eigenen Vorarbeiten bekannten und bewährten Heuristiken
entstanden ist. Dabei lässt sich die Erfüllung der statisch ermittelten Constraints als besonderes Testüberdeckungsproblem auffassen. Dieser Ansatz wurde bereits zu einem wesentlichen Teil umgesetzt und auf einige Beispiele angewendet. Die hierbei erzielten Ergebnisse sind vielversprechend und ermutigen zu einer Fortführung der Untersuchungen. Im Zusammenhang mit den betrachteten Anwendungsbeispielen konnten etwa anhand intelligenter Tests konkrete Überlaufeffekte zum Teil dynamisch antizipiert werden. In einem besonders komplexen Fall konnte allerdings die vorhandene Schwachstelle bisher noch nicht aktiviert werden. Dies legt nahe, den bisher implementierten Testansatz zu verfeinern. Da, wie bereits erwähnt, die Erfüllbarkeit der statisch ermittelbaren Constraints sich als Überdeckungsproblem interpretieren lässt, wird beabsichtigt, den soweit implementierten, auf globaler Optimierung basierenden Ansatz mittels lokal optimierender Heuristiken zu erweitern.

Projektleitung:
Prof. Dr. rer. nat. habil. Francesca Saglietti

Beteiligte:
Dipl.-Math. Lars von Wardenburg, Dr.-Ing. Matthias Meitner, Valentina Richthammer, B. Sc., Loui Al Sardy, M. Eng., Benedikt Sixt, M. Sc., Andreas Neubaum, M. Sc.

Laufzeit: 1.7.2015 - 31.12.2018

Förderer:
Bundesministerium für Wirtschaft und Energie (BMWi)

Mitwirkende Institutionen:
Otto-von-Guericke Universität Magdeburg
Hochschule Magdeburg
Areva / Framatome GmbH

Publikationen
Al Sardy, Loui ; Saglietti, Francesca ; Tang, Tong ; Sonnenberg, Heiko: Constraint-based Testing for Buffer Overflows. In: Gallina, Barbara ; Skavhaug, Amund ; Schoitsch, Erwin ; Bitsch, Friedemann (Hrsg.) : Mälardalen University ; European Workshop on Industrial Computer Systems, Technical committee on Safety, Reliability and Security (EWICS TC7) (Veranst.) : Computer Safety, Reliability, and Security (SAFECOMP 2018 Workshops Västeras (S) 18.09). Cham (CH) : Springer, 2018, S. 99-111. (Lecture Notes in Computer Science Bd. 11094) - ISBN 978-3-319-99228-0
[doi>10.1007/978-3-319-99229-7_10]
Al Sardy, Loui ; Tang, Tong ; Spisländer, Marc ; Saglietti, Francesca: Analysis of Potential Code Vulnerabilities involving Overlapping Instructions. In: Tonetta, Stefano ; Schoitsch, Erwin ; Bitsch, Friedemann (Hrsg.) : European Workshop on Industrial Computer Systems, Technical Committee on Reliability, Safety and Security (EWICS TC7) ; Fondazione Bruno Kessler (FBK) (Veranst.) : Computer Safety, Reliability, and Security - SAFECOMP 2017 Workshops - ASSURE, DECSoS, SASSUR, and TIPS (ERCIM/EWICS/ARTEMIS Workshop on “Dependable Embedded and Cyber-physical Systems and Systems-of-Systems”, SAFECOMP Workshop DECSoS'17 Trento (I) 12 September 2017). Heidelberg : Springer, 2017, S. 103-113. (Lecture Notes in Computer Science (LNCS) Bd. 10489) - ISBN 978-3-319-66283-1
[doi>10.1007/978-3-319-66284-8]
Saglietti, Francesca: Evaluation of Testing Techniques for IT Security Checks in Automatic Control Software for Nuclear Power Plants / Sub-Project: Model-based Testing Strategies. ---- : ----. 2017 (GRS-F-2017 EN). - Interner Bericht (English Annual Report 2017, Technische Informationsbibliothek Hannover (TIB) // Forschungsstelle // GRS, Projektträger/ Behördenunterstützung, Köln)
Saglietti, Francesca ; Meitner, Matthias ; von Wardenburg, Lars ; Richthammer, Valentina: Analysis of Informed Attacks and Appropriate Countermeasures for Cyber-Physical Systems. In: Skavhaug, Amund ; Guiochet, Jérémie ; Schoitsch, Erwin ; Bitsch, Friedemann (Hrsg.) : European Workshop on Industrial Computer Systems, Technical Committee on Reliability, Safety and Security (EWICS TC7) ; Norwegian University of Science and Technology (NTNU) (Veranst.) : Computer Safety, Reliability, and Security - SAFECOMP 2016 Workshops - ASSURE, DECSoS, SASSUR, and TIPS (ERCIM/EWICS/ARTEMIS Workshop on “Dependable Embedded and Cyber-physical Systems and Systems-of-Systems”, SAFECOMP Workshop DECSoS'16 Trondheim (NO) 20 September 2016). Heidelberg : Springer, 2016, S. 222-233. (Lecture Notes in Computer Science (LNCS) Bd. 9923) - ISBN 978-3-319-45479-5
[doi>10.1007/978-3-319-45480-1]
Saglietti, Francesca: Evaluation of Testing Techniques for IT Security Checks in Automatic Control Software for Nuclear Power Plants / Sub-Project: Model-based Testing Strategies. ---- : ----. 2016 (GRS-F-2016 EN). - Forschungsbericht (English Annual Report 2016, Technische Informationsbibliothek Hannover (TIB) // Forschungsstelle // GRS, Projektträger/ Behördenunterstützung, Köln)
UnivIS ist ein Produkt der Config eG, Buckenhof