Abstrakte und konsistente Vertraulichkeitsspezifikation von der Architektur bis zum Code

Vortragende(r)	Nils Wilka
Vortragstyp	Bachelorarbeit
Betreuer(in)	Kateryna Yurchenko
Termin	Fr 24. November 2017
Vortragsmodus
Kurzfassung	Bei der Software-Entwicklung kann ein Architekturmodell verwendet werden, um ein Software-System auf einer abstrakten Ebene zu beschreiben. Innerhalb des Systems findet ein Informationsaustausch zwischen den Komponenten statt. Dabei kann es vorkommen, dass sensible Informationen verarbeitet werden. Um zu garantieren, dass sie vertraulich bleiben und nicht an unberechtigte Nutzer weitergeleitet werden, kann man eine Analyse während der Entwicklung durchführen. Dazu definiert man Vertraulichkeitsanforderungen in der Software-Architektur, die anschließend überprüft werden. Für den Einsatz des Systems, muss es zusätzlich implementiert und hinsichtlich des Informationsfiusses untersucht werden. Die Vertraulichkeitsspezifikation muss daher auf die Quellcodeebene übertragen werden. Wird das System weiterentwickelt, kann sich ihre Repräsentation für die Architektur und die der Implementierung jeweils verändern und dementsprechend widersprüchliche Aussagen enthalten. Die Untersuchung durch ein Werkzeug zur formalen Verifikation gibt zusätzlich eine spezielle Spezifikationssprache vor. Möchte man die Vertraulichkeit der Informationen verifizieren, müssen die Spezifikationselemente im Quellcode folglich in einem zusätzlichen Schritt in die richtige Sprache übersetzt werden. Die vorliegende Arbeit beschäftigt sich mit der Transformation der unterschiedlichen Repräsentationen der Vertraulichkeitsspezifikation eines Software-Systems. Es wird ein Konzept vorgestellt, dass die Konsistenz zwischen dem Vertraulichkeitsmodell auf der Architekturebene und seiner Repräsentation auf der Quellcodeebene gewährleistet. Anhand von Abbildungsvorschriften zeigen wir, wie Spezifikationselemente von der Architektur auf die Implementierung übertragen werden. Des Weiteren wird ein System vorgestellt, das die Vertraulichkeitsspezifikation des Quellcodes übersetzt, sodass sie in einer Sprache vorliegt, die zur Verifikation benutzt werden kann. Wir haben unseren Ansatz anhand zweier Fallbeispiele aus der Literatur untersucht. Dabei kommen wir zu dem Ergebnis, dass unser Verfahren erfolgreich für die Übersetzung der Spezifikationssprache in beiden Systemen eingesetzt werden kann.

Vortrag bearbeiten