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

in Bearbeitung

  • 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.
    Bearbeitung: Juni 2017 - SB

  • 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.
    Bearbeitung: Juni 2017 - SB
  • Local reasoning for authorisation in constraint environments
    Ziel der Arbeit ist die Untersuchung von Kommunikationsaufbau und das Herstellen von Vertrauen zwischen Geräten im Rahmen des Internet of Things (IoT).Es soll ein System untersucht werden, in welchem einzelne Geräte anhand vorher definierter Regeln (Policies) lokal Entscheidungen über die Berechtigungen anderer Geräte finden können. Grundstruktur ist ein Vertrauensmodell welches es ermöglichen soll, ohne Änderungen der Regeln neue Geräte hinzuzufügen (Plug and Play).Das System soll die Möglichkeit bieten über Policies Zugriff auf Ressourcen innerhalb des Netzes zu regeln. Dabei ist zu untersuchen wie diese Policies ohne zentrale Komponente verteilt und überprüft werden können.  Nach dem Festlegen einer Policy soll das Hinzufügen neuer Geräte per Plug and Play ohne weitere Konfiguration möglich sein.Um die Tauglichkeit für das IoT zu gewährleisten, soll das dabei entwickelte Protokoll möglichst wenig Ressourcen verbrauchen, um auf kleinen Geräten mit geringer Rechenleistung und Speicherausstattung zu funktionieren. Die genaue Abgrenzung soll zu Beginn festgestellt werden.
    Bearbeitung: April 2017
  • Klassifizierungssystems für 3D-Beschleunigungsdaten zur Aktivitäts-und Sturzerkennung bei neurologischen Bewegungsstörungen
    Eine Störung der Stand- und Gangregulation führt zu Beeinträchtigungen in der Alltagsmobilität von Patienten und erhöht das Risiko für Stürze. Die derzeit üblichen Messverfahren für die Stand- und Ganganalyse setzen aufwendige Messapparaturen voraus. Die Verfügbarkeit von kostengünstigen, kleinen und energiesparenden Beschleunigungssensoren ermöglicht die Aufnahme und Auswertung von Aktivitätsdaten „aus dem Alltag“. Die neue Technologie verspricht die Möglichkeit, tatsächliche Sturzvorkommnisse aufzuzeichnen, um ein besseres Verständnis des Sturzvorgangs und seiner Ursachen zu gewinnen und womöglich in Zukunft Algorithmen zur Sturzprävention zu entwickeln. Im Rahmen dieser Arbeit wird ein Klassifizierungssystem zur Detektion von Sturzereignissen in einem vorliegenden Datenbestand von 3D-Beschleunigungsdaten entwickelt. Die Daten wurden mit einem activePal Sensor am Knie der Patienten aufgezeichnet und umfassen insgesamt 20 Sturzereignisse.
    Bearbeitung: Mai 2017

  • Business Wargaming 2.0
    Ziel der Abschlussarbeit ist die theoretische, konzeptionelle und praktische Ausarbeitung einer softwarebasierten Lösung für ein Beratungsprodukt namens „Business Wargaming“.
    Business Wargaming ist ein Workshopmodell, das basierend auf einer Regression Szenarien modelliert, um daraus Handlungsempfehlungen, abhängig von dem Verhalten anderer Marktteilnehmer und unter Berücksichtigung spieltheoretischer Analysen, für den Kunden abzuleiten. Zurzeit werden die umfangreichen Vorbereitungen des Workshops und die notwendige Datenerhebung sowie deren statistische Analyse in gängigen Microsoft Office Anwendungen durchgeführt ohne auf eine standardisierte und digitalisierte Lösung zurückgreifen zu können. Zudem fehlt eine hinreichende Auseinandersetzung mit den zugrundeliegenden theoretischen Modellen, im Speziellen der spieltheoretischen Basis und der benötigten Regressionsanalyse.
    Bearbeitung: März 2017 - MH
  • Automatisierung von Systemtests am Beispiel von FTAPI Secutransfer
    Die Zielvereinbarung der Bachelorarbeit orientiert sich an dem zu Grunde liegenden Forschungsvorgehen, die Arbeit in mehrere, aufeinander aufbauende Arbeitsschritte aufzuteilen. Diese lassen sich als Ziele für die Bachelorarbeit ausgeben.
    Begonnen wird mit einer Einordnung des Themengebiets Testautomatisierung mit Literaturanalyse. Darauf folgt eine Evaluationsphase, in der drei Softwaresysteme für Testautomatisierung auf ihre Vor- und Nachteile untersucht und den Anforderungen von Secutransfer gegenübergestellt werden. Als Ergebnis der Evaluationsphase soll geklärt werden, welche Testautomatisierungssoftware am besten geeignet ist. Im nächsten Schritt wird Secutransfer auf seine Testbarkeit untersucht und gegebenenfalls angepasst. Im Anschluss wird die eigentliche Testreihe erstellt und in das für Continuous Integration zuständige Werkzeug Jenkins eingepflegt. Abschließend wird die Forschungsfrage durch Evaluation in realweltlichem Einsatz geklärt und das Ergebnisartefakt bewertet.
    Als optionales Ziel wird im Hinblick auf Continuous Delivery die Bereitstellung einer passenden Plattform für statische Code-Analyse mit anschließender Analyse und Bewertung des Codes von Secutransfer gesetzt
    Bearbeitung: Mai 2017 - MH

  • Leistung einer durch ein neuronales Netz unterstütze künstliche Intelligenz für Halm
    Aufgabe der Bachelorarbeit wird es sein, zuerst Halma (eng. Chinese Checkers) analog der Arbeit an der Stanford Universität zum Thema „Playing Chinese Checkers with Reinforce-ment Learning“ zu programmieren. In dieser Arbeit wurde ein Minimax Algorithmus kombiniert mit Alpha-Beta Pruning verwendet und mit heuristischen Features (z.B. durchschnittlicher vertikaler Abstand zur Zielbasis) eine Bewertungsfunktion erstellt, welche eine begrenzte Tiefensuche ermöglicht. Es wurde hier Reinforcement Learning verwendet, um die möglichst optimale Gewichtung der 3 gewählten Features zu finden. Hier soll angeknüpft und ein Monte Carlo Tree Search Algorithmus implementiert werden. Verwendet wird ein neuronales Netz anstatt der gewichteten Features, wobei das Spielfeld als Input der Neuronen dienen und das Netz damit für sämtliche Spielzustände eine möglichst sinnvolle Bewertung liefern soll. Das Netz wird durch Spiele gegen sich selbst (Reinforcement Learning) trainiert.
    Das Ziel wird es sein die Performance der lernenden künstlichen Intelligenz gegenüber dem Vorgänger zu analysieren, beziehungsweise den Einfluss des neuronalen Netzes zu messen. In der Arbeit an der Stanford Universität wurden zur Verkleinerung des Suchraumes die Größe des Spielfeldes verringert und außerdem die Anzahl der Spieler auf 2 begrenzt. Es soll getestet werden, ob die berechneten Spielzüge trotz des Aufhebens der Limitierungen im Spiel sinnvoll sind, beziehungsweise die KI im Durchschnitt besser spielt, als die Minimax-Version.
    Bearbeitung: März 2017 - MH

  • Decodierer für 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.
    Bearbeitung: Januar 2017
    - MH
  • 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.
    Bearbeitung: Mai 2017
    - MH
  • 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.
    Bearbeitung: Mai 2017 - MH
  • 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.
    Bearbeitung: 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.
    Bearbeitung: 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.
    Bearbeitung: 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.
    Bearbeitung: 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.
    Bearbeitung: Dezember 2016 - MH

abgeschlossene Arbeiten

  • Interprozedurale Analyse mit Heros
    In der Arbeit sollen verschiedene Algorithmen für die interprozedurale Analyse miteinander verglichen und teilweise implementiert werden. Zunächst soll dargelegt werden, wie die interprozedurale Analyse als Fixpunkt-Gleichungs-system verstanden werden kann und der Zusammenhang mit kontextfreien Grammatiken erläutert werden. Sodann sollen sowohl der naive Worklist-Algorithmus, als auch dessen von Seidl und Fecht [1] vorgeschlagene Verbesserung implementiert werden. Dies soll im Rahmen des Soot- Frameworks [2] erfolgen, welches ein Java Frontend und Datanstrukturen für Kontrollflussgraphen und intraprozedurale Analyse bereits bereitstellt.
    Schliesslich soll die in Soot in Form des Plugins Heros bereits vorhandene Implementierung des IFDS Algorithmus [3] hinzugezogen und mit diesen beiden Implementierungen sowohl qualitativ (Funktionsweise) und quantitativ (Laufzeit) verglichen werden. Dazu sollen eine Reihe von Benchmarks verwendet werden, die sowohl tatsächlich verwendete Programme, als auch synthetische zu Testzwecken entwickelte umfassen. Konkretes Analyseziel soll die Lebendigkeitsanalyse von Programmvariablen [4] sein. Die Richtlinienanalyse aus dem Projekt GuideForce am Lehrstuhl TCS [5] wird als fakultatives Analyseziel festgehalten.
    Optional sollen in Absprache mit dem Betreuer, einfache Heuristik zur Verbesserung des naiven Worklist-Algorithmus untersucht werden, mit dem Ziel eine möglichst einfache und dennoch konkurrenzfähige Implementierung zu bekommen.
    Abgabe: Mai 2017 - 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
    Abgabe: Mai 2017 - MH
  • 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. 
    Abgabe: Mai 2016 - MH

 

 

 

 

Artikelaktionen


Funktionsleiste