Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / Bachelor- und Masterarbeiten


Inhaltsbereich

Bachelor- und Masterarbeiten

Je nach den aktuellen Forschungsarbeiten gibt es kurzfristig weitere Themen; ausserdem können Sie gerne mit Ideen oder bestimmten Gebietswünschen zu einem Mitarbeiter unseres Lehrstuhls in die Sprechstunde kommen; falls möglich, kann dann ein speziell für Sie zugeschnittenes Thema entwickelt werden.

 

 


Zu vergebende Arbeiten

 

  • Untersuchung von Scrabble Strategien
    In dieser Bachelorarbeit soll zunächst ein Softwareagent entwickelt werden, welcher zu einer gegebenen Scrabblesituation alle möglichen Wörter, die gelegt werden können, findet. Hierzu muss ein geeignetes Lexikon eingebunden werden und die Möglichkeiten, Wörter zu platzieren, systematisch generiert werden. Darauf aufbauend, sollen dann verschiedene Strategien implementiert werden, wie zum Beispiel: jeweils den Zug mit der höchsten Punktzahl durchzuführen, daneben zu versuchen, den Gegnern Chancen zu "verbauen", das Buchstabenportfolio auf der Bank zu optimieren, etc. Durch Simulationen soll dann evaluiert werden, welchen Einfluss diese Strategien haben. Bei entsprechender Zeit und Interesse kann auch versucht werden, Methoden des maschinellen Lernens einzubauen.  Eine ähnliche Zielsetzung wurde bereits von einer Bachelorarbeit an der KTH Stockholm [1] verfolgt; dort wurde aber nicht der Zug mit dem höchsten Punktwert berechnet, sondern Wörter heuristisch gefunden. In der Arbeit [2] wird die Komplexität von Scrabble in einer verallgemeinerten Version untersucht.
    [1] F Connolly, Diana Gren. Smart Scrabble Playing - Strategies and their impact, KTH Stockholm
    http://www.csc.kth.se/utbildning/kandidatexjobb/datateknik/2012/rapport/connolly_frej_OCH_gren_diana_K12017.pdf

    [2] C Hube. Die Komplexitaet von Scrabble, THI
    http://www.thi.uni-hannover.de/fileadmin/forschung/arbeiten/hube-ba.pdf

    Ausschreibungsdatum: März 2016 - MH
  • Automatische Hardwaresynthese
    In dieser Arbeit soll eine Möglichkeit zur Übersetzung funktionaler Programme in FPGAs implementiert und bezüglich seiner Effizienz untersucht werden. Gegebene funktionale Programme werden von einem existierenden Compiler in eine einfache erststufige Zwischensprache übersetzt, die sich gut für Optimierung eignet. In diesem Projekt soll eine Übersetzung von dieser Zwischensprache nach Verilog/VHDL implementiert werden. Die Effizienz der Übersetzung soll experimentell untersucht und mit anderen Ansätzen verglichen werden. Neben den existierenden Optimierungen auf der Zwischensprache können eigene Optimierungen für die Zwischensprachen entworfen und evaluiert werden. Das Projekt knüpft an die Ergebisse einer früheren Bachelorarbeit an, in der eine direkte Übersetzung (ohne Zwischensprache und Optimierung) implementiert wurde.
    Ausschreibungsdatum: August 2014 - GC
  • Masterarbeit
    Amortisierte Analyse von integer-gesteuerten Schleifen

    Aufbauend auf existierenden Vorarbeiten (raml.tcs.ifi.lmu.de) soll eine am Lehrstuhl entwickelte automatische Laufzeit- und Speicherplatzanalyse für funktionale Programme auf integer-gesteuerte Schleifen erweitert werden. Kenntnisse in Haskell oder einer anderen funktionalen Programmiersprache sind erforderlich; ausserdem Grundkenntnisse über Programmanalyse und Typsysteme, wie sie z.B. in der Vorlesung "Formale Spezifikation und Verifikation" vermittelt werden.
    Ausschreibungsdatum: April 2014 -MH

  • Bachelor- oder Masterarbeit
    Regionenbasierte Analyse von Objekten
    Hier geht es darum ein von uns entwickeltes Typsystem für objektorientierte Programme (http://www2.tcs.ifi.lmu.de/~grabow/papers/beringeretal2013_regiontypesystems.pdf) zu implementieren. Sinn des Typsystems ist die genaue Analyse von Seiteneffekten und die Einhaltung vorgegebener Sicherheitspolitiken. Auf eine existierende OCAML-Implementierung eines Teilsystems, welches der Einhaltung einer bestimmten Richtlinie zur Vermeidung von cross-site-scripting dient, kann zurückgegriffen werden. Vorkenntnisse in Haskell oder einer anderen funktionalen Programmiersprache sind erforderlich; ausserdem Grundkenntnisse über Programmanalyse und Typsysteme, wie sie z.B. in der Vorlesung "Formale Spezifikation und Verifikation" vermittelt werden.
    Ausschreibungsdatum: April 2014 - MH

  • Bachelorarbeit
    Verifizierte Implementierung rein funktionaler Echtzeit-Deques
    In "Purely Functional, Real-Time Deques with Catenation" (Kaplan & Tarjan, 1999) wird eine rein funktionale Datenstruktur spezifiziert, die ansonsten die wesentlichen Eigenschaften doppelt verketteter  Listen hat: Das Hinzufügen und Entfernen von Elementen an beiden Enden, sowie das Aneinanderhängen zweier solcher Strukturen, geht in jeweils konstanter Laufzeit. Diese Datenstruktur ist allerdings vergleichsweise komplex, sodass eine verifizierte Implementierung in Coq wünschenswert ist. Spezifisch sollte verifiziert sein, dass die Struktur sich abgesehen von der Laufzeit bezüglich der genannten Operationen (Konkatenation, Hinzufügen/Entfernen vorne/hinten) wie Listen verhält. Ziel der Arbeit wird es sein, eine solche verifizierte Implementierung in Coq zu programmieren. Grundkenntnisse in Coq sind wünschenswert, können aber auch erlernt werden.
    Ausschreibungsdatum: April 2014 - CSS

  • Bachelor- oder Masterarbeit
    Specification of microkernels

    A microkernel [x] is a minimal operating system that merely manages processes,  memory, and other basic resources. Most services traditionally associated with an operating system kernel such as device drivers then run as user processes and do not necessarily need to be trusted because the microkernel ensures their separation from the other processes.
    A microkernel is then a rather simple piece of code (<10000LOC) which should be amenable to a very high standard of certification even including completely formal verification.
    While sequential microkernels have meanwhile been formally verified [x] there is still no consensus how exactly the specification of a microkernel to be subsequently verified should be formulated and, more importantly, whether the proposed specifications are indeed strong enough so as to imply desirable end-to-end properties.
    One desirable such end-to-end property could be the following non-interference property: Consider that a microkernel hosts two processes: one (the "user software") whose program code is known and which contains a secret variable to which it issues  no read or write access rights and another process (the "attacker") whose code is unknown and which runs for a while and then outputs a single bit. Can we deduce from the specification of the microkernel that the value of this bit is "independent" (and in what sense) of the value of the secret variable.
    The thesis should investigate this question for the case of the L4.verified microkernel specification [x] and possibly for simpler more high-level ones such as [boyton]. The thesis should clearly identify possible obstacles and caveats relating to the accuracy of the underlying model. For example, in reality, an attacker might have access to indirect channels such as measuring temperature or power consumptions which are not reflected in the underlying formal model of the microkernel.
    Ausschreibungsdatum: Juni 2015 - MH

  • Bachelor- oder Masterarbeit
    Specification of concurrent tree datatstructures in capability management
    An operating system kernel typically manages the access rights to resources ("capabilities") of all the processes it hosts. It may grant and also revoke such capabilities at various times. Since processes may themselves delegate such capabilities to other processes, e.g. to threads they create, the kernel must make sure that upon revokation all owners of the capability to be revoked are appropriately notified. To that end the kernel maintains a datastructure that records all the delegations of capabilities that are currently in force. Formal models of such capability management have been proposed and global properties about the maintenance of separation between disconnected components have been formally proved [boyton].
    These formal models assume that access to the data structure is atomic, i.e. capabilities to be revoked disappear simultaneously and at once. In practice, for efficiency reasons, the datastructures may, however,  allow concurrent access, i.e., capabilities may perhaps be exercised and even delegated while a revokation is currently in progress. This of course means that a very careful design of the traversal order of the data structure and of ancillary synchronisation mechanisms is necessary so as to avoid that capabilities to be revoked continue to persist somewhere.
    The thesis should describe existing solutions to that problem and then attempt to prove that with these solutions the consistency of the capabilities as asserted in the existing formal models continues to hold.
    Ausschreibungsdatum: Juni 2015 - MH

  • Bachelor- oder Masterarbeit
    Verification of a Secure Programming Guideline with Soot
    The aim of this project is to develop a Java application that checks if a source program (written in Java) follows a selected guideline for secure programming. Programming guidelines are best practices in software development to avoid common problems related to issues such as authorization, code injection, etc. One of the most extensive collections of secure programming guidelines are offered by OWASP, The Open Web Application Security Project. 
    Soot, on the other hand, a is program analysis framework for Java.  It provides support for code optimization and for analysis  of both Java source code and bytecode. For various levels of analysis (source code, bytecode etc.). A Soot application is implemented in Java; access to the Soot components is via packages and classes. There already exists a Soot implementation of a simple guideline related to code injection which can serve as a model.
    In this project, another guideline should be implemented in Soot and the results of the analysis should be reported back to the user through Eclipse. The model implementation cannot do that yet so this aspect would be completely new. The concrete guideline to be implemented is open to discussion; a sensible option is "Require authentication before allowing a file to be uploaded" (OWASP SCP Quick reference guide v2, page 12).
    This topic is part of a larger research project aimed at the development of a configurable analysis based on type systems and capable of checking arbitrary guidelines provided they are suitably formalised. Case studies like the one carried out in this topic will allow us to identify the right approach and granularity.
    In terms of training this project will help the students to understand and practice fundamentals of  program analysis, and become familiar with Soot, which has become popular in the field of practical  program analysis. 
    Ausschreibungsdatum: Juni 2015 - MH
     


in Bearbeitung

  • Bachelor- oder Masterarbeit
    Experimente mit HoTT

    In den letzten Jahren wurde eine neuartige Verwendung der Theorie der abhängigen Typen in der Mathematik vorgeschlagen ("homotopy type theory (HoTT)", homotopytypetheory.org). Grob gesprochen, geht es darum, Isomorphie auch formale durch echte Gleichheit zu ersetzen, wobei offensichtliche Widersprüche wie {0} =~= {1} => {0}={1} => 0=1 durch geeignete Abänderung der logischen Schlussregeln für die Gleichheit umgangen werden. In der Arbeit sollen zunächst einige der fortgeschrittenen Übungsaufgaben aus dem HoTT-Buch bearbeitet werden und dann ein bisher noch nicht betrachtetes Beispiel in HoTT formalisiert werden, z.B. monoidale Kategorien und Funktoren. Grundkenntnisse in Kategorien- oder Typentheorie wären hier wünschenswert, können aber auch im Rahmen der Betreuung erworben werden.
    Bearbeitungsdatum: August 2015

  • Bachelor- oder Masterarbeit
    Experimente mit Easycrypt

    Das Werkzeug EasyCrypt www.easycrypt.info dient der rechnergestützten Entwicklung formaler und geprüfter Beweise der Sicherheit kryptographischer Protokolle und Mechanismen. Nach Goldwasser und Micali definiert man ein solches System als "sicher", wenn es möglich ist, aus einer hypothetischen Attacke eine Attacke auf ein als sicher angenommenes krpytographisches Primitivum, wie Faktorisierung, Pseudozufallszahlen, etc abzuleiten. Solche Ableitungen können in Easycrypt formal entwickelt werden. In der Arbeit geht es darum, sich mit EasyCrypt vertraut zu machen, es mit eigenen Worten zu beschreiben und ein einfacheres Beispiel selbst darin zu entwickeln.
    Bearbeitungsdatum: Juni 2015

  


abgeschlossene Arbeiten

 


 

Artikelaktionen


Funktionsleiste