USDL ist eine Sprache zur Beschreibung von Online-Dienstleistungen und zur Verknüpfung mit Prozessen in der physikalischen Welt, die von der SAP AG Ende 2009 als neuer Standard geplant worden ist und sich seitdem in der Entwicklung befindet. Die Kernidee ist, über gängige "Webservices" hinaus betriebswirtschaftliche und operationale Aspekte wie Urheberrechte, Verfügbarkeit und Preismodelle zu thematisieren.In diesem Vortrag soll eine Einführung in USDL gegeben werden. Darüber hinaus wäre es überlegenswert, ob es bereits Bestrebungen gibt, Sicherheitsanforderungen in USDL zu beschreiben, und falls ja wie diese aussehen?
Im Security-Bereich müssen immer wieder Aussagen bewiesen werden. Für die Anwendung is Laufenden System bieten sich Theoremprover an, diese Arbeit halbautomatisch zu übernehmen. In diesen Vortrag soll das System KIV als Beispiel vorgestellt werden.
Literatur:
Seitenkanalangriffe greifen nicht das kryptographische Verfahren selbst an, sondern seine Implementieren. Dabei werden durch Beobachtungen des Geräts Informationen gewonnen. Im Vortrag sollen die grundlegenden Verfahren von Paul Kocher vorgestellt werden.
Literatur:
Zusatzliteratur:
Stört man die Berechnung kryptographischer Verfahren lassen sich aus den verfälschten Ergebnissen unter Umständen Erkenntnise über die verwendeten Schlüssel gewinnen. Ziel des Vortrags ist das Prinzip dieses Angriffs zu erläutern und einen konkreten Angriff (theoretisch) vorzustellen.
Literatur:
Zusatzliteratur:
Wie kann man an entfernten Orten fair Poker spielen oder beispielsweise eine Münze werfen? Ziel des Vortrags ist die Vorstellung kryptographischer Protokolle, die es ermöglichen die angesprochenen und verwandte Problem zu lösen.
Literatur:
Mittels Programm Obfuscation lässt sich die Funktion eines Programms beibehalten, wobei aber beispielsweise der Quelltext geändert werden kann, z.B. um Reverse-Engineering zu erschweren. Ziel des Vortrags ist neben der formalen Erklärung des Begriffs zwei unterschiedliche Einschränkungen der Programm Obfuscation aufzuzeigen.
Literatur:
In Cloud Computing Umgebungen können Berechnung auf nicht vertrauenswürdige Server ausgelagert werden. Mit homomorpher Verschlüsselung und sicheren Multiparty Computation stehen entsprechende kryptographische Primitive zur Verfügung, die eine vertrauenswürdige Berechnung leisten können. Entsprechende Software muss allerdings sorgfäaltig aufgebaut sein, um Vertrauenswürdigekeit zu garantieren. Alex Bain et al. schlagen eine auf Haskell basierende domain-specific language (DSL) für Cloud Computing vor. Ziel des Vortrags ist eine kurze Einführung in (e)DSLs und die Vorstellung der DSL für die Berechnung auf verschlüsselten Daten.
Literatur:
Modell-basiertes Testen hilft bei der Bewältigung der Aufgabe, komplexe Systeme automatisiert auf ihre Funktionsfähigkeit zu testen. Die Arbeit soll einen Überblick über das Feld des Modell-basierten Testens geben und ein paar aktuelle Beispiele aussuchen und beschreiben.
Literatur:
Im Refinement-basierten Ansatz des Software-Designs existiert eine Reihe von verbundenen Modellen. Um diese Modelle während der Evolution konsistent zu halten, werden in diesem Paper Ko-Evolutionen mit Hilfe der formalen Methode Object-Z entwickelt, die die Modelle konsistent halten.
Literatur:
Die Verarbeitung vertraulicher Daten stellt Sicherheits- und Complianceanforderungen an die Cloud. Diese Anforderungen ans Cloud Computing sollen erläutert und bestehende Ontologien und Referenzmodelle diskutiert werden.
Literatur:
Refinement Checking erlaubt den Vergleich verschiedener Spezifikationen in Bezug auf funktionale Äquivalenz. Der Vortrag stellt die Grundlagen des Verfahrens vor, sowie ggf. deren praktische Umsetzung, z.B. anhand des Refinement Checkers FDR2.
Literatur:
In der Softwareentwicklung werden Graphen für unterschiedliche Aspekte verwendet: Zur Beschreibung statischer
Strukturen in UML-Modellen, als Quellcode-Graphen, aber auch zur Beschreibung von Ausführungssemantiken. GROOVE ist ein
Werkzeug, das die Verarbeitung von Graphgrammatiken erlaubt, sowie als "Graph Model Checker" in der Lage ist, Aussagen
über Eigenschaften solcher Grammatiken zu treffen.
In diesem Vortrag sollen zunächst die Grundlagen der verwendeten Graphgrammatiken vorgestellt werden, sowie deren
Anwendung auf dem Gebiet der modellbasierten Softwareentwicklung.
Literatur:
Core Gnosis basiert auf Demos2k und ist eine ausführbare Modellierungssprache. Mit Hilfe dessen komplexe Systeme mit stochastischen Eingängen und ortsbezogene Ressourcen modelliert und simuliert werden können. Basierend auf SCCS und (L)SCRP existiert ein sematischer Calculus zur mathematischen Darstellung der Sprache.
Literatur:
UML Sequenzdiagramme zur Spezifikation von Nachrichtenflüssen sind Ihnen bereits aus den Grundvorlesungen bekannt. Die Grundlage hierfür bilden Message Sequence Charts, die sich nicht wesentlich unterscheiden. Darüber hinaus gehen Life Sequence Charts, LSCs, die z.B. auch ermöglichen bestimmte Situationen zu verbieten. Im Rahmen dieses Seminarthemas soll die Modellierung mit LSCs eingehend untersucht und vorgestellt werden. Hierbei soll insbesondere darauf eingegangen werden, wie konkrete (Sicherheits-)Anforderungen mit LSCs spezifiziert werden können.
Literatur:
Zur Definition von Anforderungen existieren diverse Sprachen, sogenannte Requirements Specification Languages (RSLs). Sie eignen sich dazu die Anforderungen in einheitlicher und semantisch eindeutigen Form zu spezifizieren. In der Komponentenbasierten Softwareentwicklung, können diese Sprachen z.B. genutzt werden, um die Anforderungen an einzelne Komponenten zu definieren und andererseits, um zu prüfen, ob eine Komponente diese Anforderungen auch tatsächlich erfüllt. Im Rahmen dieses Seminarthemas, soll vorgestellt werden, wie RSLs zur eindeutigen Spezifikation von Sicherheitsanforderungen genutzt werden können und wie eine Prüfung der Erfüllung dieser Anforderungen umgesetzt werden kann.
Literatur:
Spieltheorie ist ein bedeutendes Feld in zur Entscheidungsbewertung. ARA ist eine Methode, die diese Spieltheorie auf feindliche Umgebungen anpasst, in denen die Annahmen der Gegner unsicher sind. Dabei wird versucht Entscheidungen in Konfliktsituationen abzuleiten. An Hand eines Szenarios "Die Somalia Piraten" wird die Anwendbarkeit von ARA gezeigt.
Literatur:
Für große Unternehmen ist die Bereitstellung von Patches eine kostspielige Aufgabe, mit erhebliche Folgen für die Verfügbarkeit des Systems. Sollte ein Patch nicht oder zuspät bereitstellen werden, riskiert die Organisation eine Ausnutzung der Schwachstellen. In dem Paper wird eine Berechnung der optimalen Patchpolitik vorgestellt.
Literatur: