Implementierung und Evaluation von Vorbedingungskommunikation für unsafe Code in Rust

09 Aug 2023 - 17:03 | Version 3 | UnknownUser

worked on by: Niclas Schwarzlose

Outline

Korrektheit ist in der Regel eines der Hauptziele bei der Softwareentwicklung. Es gibt viele Werkzeuge, die Entwickler beim Erreichen dieses Ziels unterstützen sollen. Die Programmiersprache Rust hat viele solcher Werkzeuge als Sprachfeatures fest eingebaut. So ist es beispielsweise normalerweise nicht möglich, in Rust einen Speicherzugriffsfehler zu erzeugen. Da es für manche Operationen jedoch notwendig ist, diese Sicherheitsfeatures zu umgehen, gibt es in Rust `unsafe` Code. Dieser erlaubt es bestimmte Operationen durchzuführen und damit auf einem ähnlichen Abstraktionslevel wie in C zu programmieren. `unsafe` Code kann jedoch bei falscher Verwendung zu undefiniertem Verhalten und damit auch zu Sicherheitslücken führen. Deswegen wird die korrekte Verwendung in der Regel in Form von Vorbedingungen dokumentiert.

`unsafe` Code tritt in zwei Formen auf: Bei der Definition von `unsafe` Funktionen, für deren korrekten Aufruf Vorbedingungen erfüllt sein müssen, und beim Aufruf dieser Funktionen. In dieser Bachelorarbeit soll ein Werkzeug entwickelt werden, dass überprüft, ob an der Funktionsdefinition angegebene Vorbedingungen auch an den Aufrufstellen dieser Funktion angegeben werden. Eine solche Überprüfung würde Nutzer von `unsafe` Funktionen dazu zwingen, sich mit allen Vorbedingungen auseinanderzusetzen und zu dokumentieren, warum sie eingehalten werden. Außerdem würde eine Veränderung der Vorbedingungen dazu führen, dass Code, der sich noch auf die alten Vorbedingungen bezieht, nicht mehr kompilieren würde, bis er entsprechend aktualisiert wäre. Dadurch wird verhindert, dass eine solche Veränderung untergeht oder nur teilweise beachtet wird. Es wäre insgesamt schwerer `unsafe` Funktionen falsch zu verwenden und würde damit die Fehlerwahrscheinlichkeit in der Software reduzieren.

Im zweiten Teil dieser Bachelorarbeit soll überprüft werden, wie hilfreich dieses Werkzeug in der Praxis ist. Eine Möglichkeit, dies zu überprüfen, wäre es zu versuchen, die Verwendung des Werkzeugs in bestehende Open Source Projekte zu integrieren. Eine weitere Option wäre es zu überprüfen, inwieweit das Werkzeug sich für Codeprüfungen eignet. Dabei kann beispielsweise bei einem bekannten und schon behobenen Fehler das Werkzeug angewendet werden und dann überprüft werden, ob dieser Fehler mithilfe des Werkzeugs entdeckt worden wäre. Ziel der Evaluation des Werkzeugs ist es, entscheiden zu können, in welchen Situationen seine Verwendung angemessen ist und in welchen Situationen der Mehraufwand die Verwendung nicht rechtfertigt.

Thesis Requirements

formulate requirements here (together with your adviser)

Milestones and Planning

A milestone is a scheduled event signifying the completion of a major deliverable or a set of related deliverables. A milestone has zero duration and no effort -- there is no work associated with a milestone. It is a flag in the workplan to signify some other work has completed. Usually a milestone is used as a project checkpoint to validate how the project is progressing and revalidate work. (Source: http://www.mariosalexandrou.com/definition/milestone.asp)