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

  • Master-Praktikum
    "Automatentheorie"

    siehe Vorlesungshomepage zur Automatentheorie, November 2016, MH
  • 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 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, Schriftliche Hausarbeit
    Referenzimplementierung von Turbocodes.

    Turbocodes bilden eine in den 90ern entwickelte und seit Anfang des Jahrhunderts auch in der Praxis, z.B. WiFi, LTE, verwendete neue Klasse fehlerkorrigierender Codes, die bisher unerreichte Korrekturqualitaet erreichen. Waehrend die Codierung relativ simpel ist, wird fuer die Decodierung ein recht komplexes iteratives Verfahren verwendet, welches zudem noch mit Wahrscheinlichkeiten, statt nur mit "harten" Bits rechnet. In der Arbeit sollen diese Verfahren implementiert und ausgiebig getestet werden, um einige Vermutungen und Hypothesen ueber das Verhalten von Turbocodes nachzupruefen und zu untersuchen. Z.B. soll durch (fuer die Praxis prohibitiv teure) exhaustive Suche die optimale Decodierung von zufaelligen Beispielen bestimmt werden und mit der durch dden iterativen Algorithmus gefundenen Naeherungsloesung verglichen werden.  Auch soll untersucht werden, inwieweit eine Decodierung ohne Wahrscheinlichkeiten moeglich ist und, wenn ja, wie sich das auf die Guete auswirkt.
    Ausschreibungsdatum: Januar 2017 - MH

  • Bachelor- oder Masterarbeit, Schriftliche Hausarbeit
    Suche von guten Faltungscodierern mit SAT Solvern.

    Ein Faltungscodierer codiert einen Bit-Datenstrom dadurch, dass aus den jeweils letzten L Bits mehrere (m) geeignet gewaehlte XOR Summen gebildet werden, so wird ein Datenstrom also auf das m-Fache aufgeblaeht, wodurch fehlerkorrierende Redundanz entsteht. Typisch sind Werte wie L3..10, m=2,3. Ein wichtiger Gueteparameter fuer einen Faltungskodierer ist die *freie Distanz*: die minimale Zahl von Einsen in der Ausgabe zu einem Eingabestrom, der nicht nur aus Nullen besteht. Geeignete Schaltplaene fuer solche Faltungscodierer wurden in den 80er Jahren durch exhaustive Suche vor allem von der NASA gefunden. Hier geht es darum, mithilfe eines SAT-Solvers moeglichst gute Faltungscodierer zu finden, also in erster Linie die Ergebnisse der NASA zu reproduzieren und vielleicht noch den ein oder anderen neuen Codierer aufzufinden.
    Ausschreibungsdatum: Januar 2017 - MH

  • Bachelor- oder Masterarbeit, Schriftliche Hausarbeit
    Decodierer fuer Reed-Solomon Codes.

    Beim Reed Solomon Code wird eine Nachricht als Koeffizientenliste eines Polynoms vom Grad k aufgefasst, welches dann an n festen Stuetzstellen ausgewertet wird, wobei n>k ist. Die Werte an den n Stuetzstellen werden dann als uebermittelt und koennen auf Empfaengerseite aufgrund der Redundanz n>k fehlerkorrigierend dekodiert werden. Reed Solomon Codes werden insbesondere bei der CD, aber auch bei verschiedenen Mobilfunk und WiFi Standards angewandt. Das klassische Decodierverfahren ist Berlekamps Algorithmus gefolgt von Chien-Suche. Es gibt aber noch ein anderes Verfahren, welches eigentlich einfacher ist und auf linearen Gleichungssystemen beruht. Hier sollen beide Verfahren implementiert und experimentell verglichen werden.
    Ausschreibungsdatum: Januar 2017 - MH

  • Bachelorarbeit
    Lernen eines Tokenizers durch Beispiele
    Automatenlernen ist eine der Möglichkeiten, aus Beispielen Regeln abzuleiten. Ziel dieser Arbeit ist es, mithilfe von Techniken zum Lernen endlicher Automaten einen Tokenzier, wie er beim Parsen von Daten verwendet wird, zu lernen.
    Ausschreibungsdatum: Januar 2017 - SB

  • Bachelorarbeit
    Approximationen von Binären Entscheidungsdiagrammen (BDD)
    BDDs sind eine Datenstruktur zur Repräsentation Boolescher Funktionen. Diese werden oft in der Synthese und Verifikation eingesetzt. Eines der Hauptprobleme bei der Verwendung von BDDs ist die mitunter stark anwachsende Größe von BDDs.
    Diese Arbeit behandelt Approximationen von BDDs: Ein BDD, welches sich in möglichst wenigen Eingaben von dem Original-BDD unterscheidet, aber weniger Zustände hat. Dabei sind hauptsächlich einseitige Approximationen von Interesse, also Approximationen, welche alle akzeptierten Eingaben des Original-BDDs akzeptiert, aber eben noch weitere Eingaben akzeptieren kann.
    Diese Arbeit umfasst Literaturrecherche, Entwicklung eigener Verfahren und eine Implementierung dieser Verfahren.
    Ausschreibungsdatum: Januar 2017 - SB

in Bearbeitung

  • Synthese von Belegungen zellulärer Automaten
    Zelluläre Automaten sind ein beliebtes Modellierungswerkzeug für dynamische Systeme. Bei der Analyse zellulärer Automaten finden sich oft interessante Konfigurationen, beispielsweise Glider in Game of Life oder ein nand-Gatter in Wireworld. Ziel dieser Arbeit ist es, mit Hilfe von SAT-Solvern gezielt nach Konfigurationen mit festgelegten Eigenschaften zu suchen.
    Bearbeitungsdatum: März 2017 - SB

  • 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.
    Bearbeitungsdatum: Januar 2017 - US

  • Implementierung von Shor's Algorithmus, Post-Quantum-Kryptographie.
    Shor's Algorithmus erlaubt die Faktorisierung von grossen Zahlen, sowie die Berechnung diskreter Logarithmen in polynomialer Zeit auf einem Quantencomputer. Fuer klassische Computer sind keine solchen Verfahren bekannt. Da alle derzeit gebraeuchlichen asymmetrischen Verschluesselungsverfahren ("public key") auf der Schwierigkeit dieser Aufgaben beruhen, wuerde ein funktionierender Quantencomputer diese Verfahren auf einen Schlag unsicher machen. Die NSA spricht daher seit kurzem vermehrt von "Post Quantum Cryptography" (PQC), die allerdings noch nicht wirklich existiert. In der Arbeit soll in erster Linie Shor's Algorithmus durch ein ("klassisches") Computerprogramm simuliert werden. Das erfordert natuerlich exponentielle Rechenzeit, aber kann verwendet werden um den Algorithmus zu testen, und insbesondere seine Abhaengigkeit von der Rechengenauigkeit zu untersuchen. Darueberhinaus koennte solch eine Implementierung fuer Lehrzwecke verwendet werden. Zusaetzlich koennten die bisher bekannten Ansaetze zu PQC recherchiert und dargelegt werden.
    Ausschreibungsdatum: Januar 2017 - MH
  • 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.
    Bearbeitungsdatum: Dezember  2016 - MH
  • 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
    Bearbeitungsdatum: Dezember  2016 - MH
  • 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: Dezember 2016 - MH

abgeschlossene Arbeiten

  • 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
  • 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

 

 

 

 

Artikelaktionen


Funktionsleiste