Abschlussarbeiten

Bachelor- und Master-Arbeiten ergeben sich bei uns meist aus aktuellen Forschungsinhalten. Wenn sie Interresse an einer Arbeit bei uns haben, konsultieren sie bitte die unten stehende Liste oder wenden sie sich direkt an uns. Um eine Vorstellung von weiteren möglichen Themen zu bekommen, können sie sich unsere Liste abgeschlossener Arbeiten ansehen.

Offene Themen

Bachelorarbeiten
ThemaBetreuerKurzbeschreibung

Evaluation eines Programs-from-Proofs Ansatzes für Informationsflusskontrolle

Marie-Christine Jakobs

Programs-from-Proofs ist ein Verfahren zur einfachen Sicherstellung von der Korrektheit von Software, die bei einem Nutzer ausgeführt wird. In dem Verfahren prüft der Hersteller einer Software aufwändig die Korrektheit bezüglich der gegebenen Anforderungen und nutzt anschließend den Beweis, um die Software in eine schneller prüfbare und dennoch verhaltensäquivalente Version zu transformieren. Bisher haben wir dieses Verfahren für Sicherheitseigenschaften wie Protokolle und Invarianten benutzt. In dieser Abschlussarbeit soll ein bereits theoretisch beschriebenes Verfahren [1] evaluiert werden, welches Security Eigenschaften mittels Typsystemen prüft. Konkret prüft das Verfahren, dass keine unerlaubten Informationsflüsse auftreten, z.B. eine Variable am Programmende keine Informationen über Anfangswerte von Variablen mit höherem Sicherheitslevel enthält. In der Abschlussarbeit sollen die Typprüfungsverfahren auf Seiten des Herstellers und Nutzers sowie die Programmtransformation implementiert werden. Anschließend soll praktisch evaluiert werden, wie viel besser (z.B. bzgl. Zeit und Speicherbedarf) die Prüfung des transformierten Programms gegenüber der Prüfung des originalen Programms beim Hersteller ist. Dafür müssen auch geeignete Programme(Benchmark) gefunden werden.

Literatur:
[1]
Sebastian Hunt and David Sands. 2006. On flow-sensitive security types. In Symposium on Principles of Programming languages (POPL '06). ACM, 79-90. http://doi.acm.org/10.1145/1111037.1111045
[2] Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. J. Comput. Secur.
4, 2-3 (January 1996), 167-187.

Strategy Design for Graph-Based Models using
Evolutionary Algorithms

Julia Krämer

Lorijn van Rooijen

Specification and verification of systems have become a crucial element of design processes in industry and research, especially in the development of security- and safety-critical systems. Whereas the development of security-critical systems focuses on the robustness against malicious intruders, safety-critical systems need to adhere to their specification in any environment. In both domains, the overall
system structure is antagonistic, for instance, a possibly hostile environment tries to force a system error to occur in safety-critical system. In security-critical systems, the system's defender tries to prevent the system's attacker, for example, from retrieving any sensible data.
During the design process, several alternatives might exist to accomplish the same task. Thus, developers are interested in choosing the best alternative
with respect to objectives such as costs or success probability. Strategies are functions, which resolve such alternatives given a specific status of the system. Therefore, developers are interested in optimal strategies, which resolve
decisions in such a way that the system not only meets its requirements but also objectives like costs and success probabilities are optimized.
In [2], a formal game-theoretic framework to model attacks on security-critical systems was proposed, but the question how to compute good strategies for the defender remains as an open problem. The synthesis of strategies in general is computationally difficult or even undecidable (as in the context of [2]) based on the system model chosen.
Therefore, it is worthwhile to look into heuristic approaches to approximate optimal strategies. Evolutionary algorithms are so-called black-box optimizers that are applicable to a wide range of problems. Such an algorithm evolves a population of possible solutions (individuals).  This is done by measuring the quality (fitness) of the solutions, selecting solutions of higher quality, mutating these and letting these reproduce new solutions.
Applying this approach to the problem discussed above amounts to encoding strategies as individuals, defining a quality measure, and constructing an appropriate mutation operator and reproduction mechanism. In this case, the quality of solutions depends on both cost and success probability, making the problem a multi-objective optimization problem [1].

Literatur:
[1] K. Deb, S. Agrawal, A. Pratap, and T. Meyarivan. A fast and elitist multiobjective genetic algorithm: NSGA-II. IEEE Trans. Evolutionary Computation, 6(2):182–197, 2002.
[2] Holger Hermanns, Julia Krämer, Jan Krčál, and Mariëlle Stoelinga. The value of attack-defence diagrams. In Frank Piessens and Luca Viganò, editors, POST 2016, pages 163–185, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.

Masterarbeiten
ThemaBetreuerKurzbeschreibung

Aktuell Laufende Arbeiten

Bachelorarbeiten
ThemaBetreuerKurzbeschreibung
Evaluation von Graph-partitionierungsalgorithmen im Kontext von Konfigurierbarer SoftwarezertifizierungMarie-Christine JakobsIn der heutigen Zeit installieren wir immer häufiger Anwendungen, z.B. Programme, Apps, die aus unbekannten, nicht verlässlichen Quellen stammen. Um solche Anwendungen ohne Risiko anzuwenden, muss geprüft werden, dass sie gewisse Eigenschaften, z.B. Sicherheitseigenschaften, einhalten. Ein Nachweis der Eigenschaften mittels Verifikation ist aufwändig und verhindert eine typischerweise gewünschte zeitnahe Ausführung der Anwendung. Um trotzdem eine zeitnahe Ausführung zu garantieren, wurde das PCC Prinzip entworfen. In PCC führt der Hersteller der Anwendung die teure Verifikation durch und liefert die Anwendung zusammen mit einem Beweis für die Verifikation aus. Der Nutzer der Anwendung überprüft vor erstmaliger Anwendung lediglich den Beweis. Der Vorteil für den Nutzer ist, dass die Überprüfung wesentlich schneller und einfacher ist. Konfigurierbare Software Zertifizierung ist ein generisches, auf PCC basierendes Zertifizierungsframework, welches Eigenschaften mittels diverser Analysen absichern kann. Um die Zertifikatsprüfung weiter zu beschleunigen, wird in dem Zertifizierungsframework der Beweis (in Form eines Abstract Reachability Graphs) in mehrere Teile aufgeteilt. Die Aufteilung geschieht mittels Graphpartitionierung. Der Nutzer kann somit die einzelnen Teile parallel prüfen. Bis jetzt geschieht die Graphpartitionierung zufällig. In der Bachelorarbeit sollen verschiedene Partitionierungsalgorithmen angeschaut, implementiert und evaluiert werden. Fragen für die Evaluation sind z.B. wie groß wird der aufgeteilte Beweis, welcher Partitionierungsalgorithmus liefert das beste Ergebnis für die Beweisprüfung?
A Prolog Approach to Service Composition VerificationJulia KrämerA Prolog Approach to Service Composition Verification

Services are self-contained and platform independent pieces of software, which are usually described by an interface. An interface of a service usually contains the service name and the pre- and postcondition it complies to, where precondition are formulated using first order logic. Services can be combined to service compositions using branches, loops and assignment.

A simple service composition is, for example, given by

1 Set<Book> result := emptyset;
2 foreach b in B do
3   Price y := hasBookPrice(b,S);
4   if isMinRating(y) then
5     result := result union {b}
6   fi;
7 od

where B is a set of books and S is a given book store. The given service composition computes a subset of books contained in the set B, which is available in the book store S at a minimal price. This service compositon is functional correct if the set result only contains books, which are available in S at a minimal price.

In [1], the functional correctness of services is verified using an SMT approach. i.e. the problem is reduced to checking the satisfiability of a propositional logic formula with background knowledge [3].

This thesis aims at an alternative verification tool for service composition based on declarative programming language Prolog [2]. In Prolog, logic is expressed in terms of relations, represented by so-called facts and rules and computations are invoked by a query over these relations. For example,

student_advisor(you,julia).
advisor_supervisor(julia,professor).
student_supervisor(X,Y):- student_advisor(X,Z), advisor_supervisor(Z,Y).

describes the logic relations between students, advisors and supervisors. A possible query, is, for instance,

student_supervisor(X,Y).

which checks whether there exists a student with a supervisor.

This bachelor thesis can also be extended to a master thesis.

[1] S. Walther, H. Wehrheim: Knowledge-Based Verification of Service Compositions - An SMT approach. In Engineering of Complex Computer Systems (ICECCS), 2013 18th International Conference. , pp. 24-32 (2013)
[2] https://en.wikipedia.org/wiki/Prolog
[3] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
Error Localization for Service CompositionsJulia Krämer

Services are self-contained and platform independent pieces of software, which are usually described by an interface. An interface of a service usually contains the service name and the pre- and postcondition it complies to, where precondition are formulated using first order logic. Services can be combined to service compositions using branches, loops and assignment, which facilitates the construction of large software systems.

In contrast, most error localization approaches for software are tailored towards imperative programs and existions thereof and not to service compositions.

The goal of this bachelor thesis is to adapt existing approaches to error localization to the setting of service compositions and to evaluate their effectiveness.

Verifikation von Service Kompositionen mit Interface AutomatenJulia KrämerZiel des komponenten-basierten Software Engineering ist es die Konstruktion von Software durch ein Einsatz von bestehender, eindeutig spezifizierter Sofware-Komponenten zu vereinfachen. Gegebenenfalls können komplexe Aufgaben dabei von bereits exitierenden Komponenten gelöst werden und müssen so nicht neu implementiert werden. Die zentralen Fragen, die man sich als Entwickler stellen muss, um schließlich qualititativ hochwerte Produkte auszuliefern, sind die gleichen geblieben: Welche Eingaben führen zu korrekten Ausgaben? Erfüllen die Ausgaben immer die Anforderungen? Wo liegen möglicherweise Fehler? Die Analyse dieser Fragen ist mit komponenten-basierter Software mitunter schwerer, da man zum Beispiel bestehene Komponenten nicht oder nur kaum modifizieren kann und sich auf die Korrektheit der Spezifikation verlassen muss.
Ein bestehender Ansatz, die Korrektheit dieser Software zu prüfen, arbeitet mit der Erfüllbarkeit logischer Formeln. Jedes Program und die verwenden Komponenten werden dabei in der Formel kodiert, so dass das Programm genau dann die korrekt ist, wenn die Formel nicht erfüllbar ist. Ziel dieser Bachelor-Arbeit ist es, einen alternativen Ansatz zu implementieren und mit dem bestehenden Ansatz zu vergleichen.
Komponenten-basierte Software soll dabei als sogenannter Interface Automat kodiert werden. Mithilfe existierender Algorithmen zur Überprüfung von Sicherheitseigenschaften auf Interface Automaten soll dann bewiesen werden, dass das Program die Eigenschaft erfüllt bzw. ein Gegenbeispiel ausgegeben werden, wenn dies nicht Fall nicht. Der neu implementierte Ansatz soll dann mit der bestehenden Überprüfung hinsichtlich Laufzeit und Skalierbarkeit verglichen werden.

Literatur
* Luca de Alfaro & Thomas A. Henzinger, Interface Automata In Proc. of ESEC/FSE 2001, ACM Press, 2001
* Luca de Alfaro & Thomas A. Henzinger, Interface Theories for Component-Based Design Embedded Software, Springer Berlin Heidelberg, 2001, 2211, 148-165
* Michael Emmi, Dimitra Giannakopoulou, and Corina S. Păsăreanu. 2008. Assume-Guarantee Verification for Interface Automata. In Proceedings of the 15th international symposium on Formal Methods (FM '08), Jorge Cuellar, Tom Maibaum, and Kaisa Sere (Eds.). Springer-Verlag, Berlin, Heidelberg, 116-131



Masterarbeiten
Thema Betreuer Kurzbeschreibung

Abgeschlossene Arbeiten

Auswahl:

 

Predicting Rankings of Software Verfication Tools Using Kernels for Structured Data
Mike Czech (Masterarbeit)

Program slicing: A Way of Separating C Program into Approximate and Precise Portions
Guangli Zhang (Masterarbeit)

Evaluierung von Przessmanagementlösungen im Hinblick auf agile Prozesse
Jan Bödefeld (Bachelorarbeit)

Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs"
Philipp Korth (Bachelorarbeit)

Ein hierarschischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit
Johannes Heil (Bachelorarbeit)

Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren
Felix Pauck (Bachelorarbeit)

Entwicklung eines Konzeptes zur Kodierung eines objekt-orientierten Typsystems in SMT
Andreas Krakau (Bachelorarbeit)

Visualisierung von SMT-Solver Ausgaben
Sebastian Osterbrink (Bachelorarbeit)

Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB
Manuel Töws (Masterarbeit)

Linearisierbarkeitsbeweis der Work-Stealing Deque
Monika Wedel (Bachelorarbeit)

Integration von History-basierten Korrektheits-Checks im Model Checker SPIN
Katharina Dridger (Bachelorarbeit)

Formal Semantics of Probalistic SMT Solving in Verification of Service Compositions
Maryam Sanati (Masterarbeit)

Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen
Christoph Klauke (Bachelorarbeit)

Vergleichsstudie zur Ausdrucksstärke von SMT-Solvern
Marco Engelbrecht (Bachelorarbeit)

Analyse von Benutzeranforderungen an Service-Kompositionen mittels Modelchecking
Tobias Nickel (Bachelorarbeit)

Berechnung von Memory Model-spezifischen Kontrollflussgraphen
Michael Feldmann (Bachelorarbeit)

Combining Three-Valued Logic and Quantified Boolean Formulae in Bounded Model Checking Encodings
Nikolaos Ikonomakis (Masterarbeit)

Dreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von Gegenbeispielen
Mike Czech (Bachelorarbeit)

Suchraumeinschränkung für Graphgrammatiken durch tempoallogische Formeln
Marcel Friedrich (Bachelorarbeit)

Multiagenten-Koordination in temporaler Planung
Thomas Hauck (Masterarbeit)

Exploiting Planning Graphs and Landmarks for Efficient GTS Planning
Shayan Ahmadian (Masterarbeit)

Bounded Model Checking für Graphtransformationssysteme als SAT-Problem
Tobias Isenberg (Masterarbeit)

Change and Validity Analysis in Deductive Program Verification
Marie-Christine Jakobs (Masterarbeit)

Konzeption und Anwendung von Verhaltensmodellen in georeferenzierten Monitoringszenarien
Patrick Backhaus (Bachelorarbeit)

Function Specification Inference Using Craig Interpolation
Schremmer, Alexander (Masterarbeit)

Heuristic Search-Based Planning for Graph Transformations Systems
Estler, Hans-Christian (Diplomarbeit)

Reputation-based reliability prediction of service compositions
Galina Besova (Masterarbeit)

Generierung von Shape-Analysen aus Graph-Spezifikationen
Buckler, Christoph (Masterarbeit)

Increasing the preciseness of shape analysis for graph transformations systems
Daniel Wonisch (Masterarbeit)

Modellierung und Analyse eines Bluetooth Protokolls mit Graphtransformationssystemen
Marco Rizzi (Bachelorarbeit)

Effiziente Validierung und Bewertung von Modellzerlegungen
Meik Piepmeyer (Diplomarbeit)

Rückführung und Visualisierung von Gegenbeispielen aus einem Model Checker
Sebastian Micus (Bachelorarbeit)

Sichere Konfigurationsplanung adaptiver Systeme durch Model Checking
Malte Röhs (Diplomarbeit)

Bounded Model Checking für partielle Systeme
Nils Timm (Masterarbeit)

Spezifikation des partiell replizierten, verteilten Systems DORS mit CSP-OZ in einem iterativen Entwicklungsprozess
Braun, Rudolf (Diplomarbeit)

Konzeption und Implementierung der Diagnose-Therapie-Komponente eines Softwarequalitätszykluses
Beister, Frederic (Bachelorarbeit)

Konzeption & Implementierung eines Dekompositions-Werkzeugs für kompositionelle Verifikation
Herbold, Klaus (Diplomarbeit)

Konzeption und Implementierung eines Testframeworks für parametrisierte Tests und Isolation des Testgegenstandes
Schröder, Marina (Diplomarbeit)

Optimierung und Erweiterung einer Testsuite für eine Beschaffungslösung im öffentlichen Sektor
Dertmann, Nadine (Studienarbeit (DPO4))

Automatisiertes kompositionelles Model Checking von CSP Spezifikationen
Wonisch, Daniel (Bachelorarbeit)

Variablenordnungsstrategien für den symbolischen Modelchecker TINY
Steenken, Dominik (Studienarbeit (DPO4))

Semantikerhaltende Transformation objekt-orientierter in zustandsbasierte Spezifikationen / Übersetzung von CSP-OZ nach ProZ
Müller, Steven (Studienarbeit (DPO4))

Entwurfsmuster in integrierten Methoden am Beispiel Object-Z
Xianghua, Zheng (Studienarbeit (DPO4))

Evaluating a model checker for the analysis of refactorings
Estler, Hans-Christian (Bachelorarbeit)

Erstellung einer CSP-OZ Spezikation der Flugkontrolle eines Flughafens mittels Syspect
Jakoblew, Marcel (Studienarbeit (DPO4))

Grundlagen für Bounded Model Checking mit 3-wertiger Logik
Liao, Hai (Studienarbeit (DPO4))

Modellierung und Verifikation verteilter Systeme mit TINY
Walther, Sven (Diplomarbeit)

Verifikation von CSP-OZ mit SPIN
Zorlu, Fatih (Studienarbeit (DPO4))

Design Pattern for Object-Z specifications
Yang, Le (Studienarbeit (DPO4))

Entwicklung eines Übersetzers einer Teilsprache von CSP-OZ in die Eingabesprache CSPM von FDR2
Wagner, Elena (Studienarbeit (DPO4))

Qualitätssicherung durch Optimierung des Testprozesses
Michalek, Dominika (Studienarbeit (DPO4))

Generierung von Refaktoringwerkzeugen
Ziegert, Steffen (Masterarbeit)

Impressum | Webmaster | Letzte Änderungen am : 03.08.2016