Theoretical Computer Science

News

2. Feb

Die technischen Informationen (zu Kitty und CAT) sind noch vorläufig.

20. Apr

Das Kickoff-Meeting findet am Donnerstag, den 23. April, um 13:00Uhr statt.

21. Apr

Die SEP eigene Projektseite ist hier online. Die technischen Details wurden finalisiert.

22. Apr

Die fehlenden Abschnitte in Teil 2 wurden ergänzt.

Überblick

Das diesjährige Softwareentwicklungsprojekt des Instituts für Theoretische Informatik (TCS) beschäftigt sich mit der hardwarenahen Verifikation. Genauer soll ein Tool entwickelt werden, welches Assembler-Programme für eine gegebene Prozessorarchitektur analysiert. Dabei sind sowohl das zu verifizierende Assembler-Programm als auch eine formale Beschreibung der Prozessorarchitektur Eingaben des zu entwickelnden Tools.

Motivation

Bei der Entwicklung sicherheitskritischer Software und Software für den Finanzsektor wird besonderes Augenmerk auf die Qualitätssicherung gelegt, da Fehler (Bugs) hier zu schweren Personen- und Sachschäden führen können. Ein großes Problem bei der Qualitätssicherung stellt allerdings die Komplexität heutiger Computersysteme dar. Zum einen werden Programme in Hochsprachen geschrieben, danach automatisch kompiliert und der resultierende Assembler-Code ausgeführt. Zum anderen integrieren Prozessoren beim Ausführen von Assembler-Code viele Optimierungen. Zusammen führt dies dazu, dass Programmierende zumeist nicht wissen (können) was genau im Prozessor passiert, wenn sie ihren Code ausführen.

Im diesjährigen SEP wollen wir die durch Hardwareoptimierungen entstehenden Probleme aufdecken und Programmierenden eine Möglichkeit geben diese zu erkennen bzw. zu verstehen. Dazu soll ein CPU-Simulator entwickelt werden, welcher alle durch eine gewisse Prozessorarchitektur erlaubten Ausführungen berechnet. In der Tat, selbst wenn das auszuführende Assembler-Programm deterministisch ist, weisen moderne Prozessoren durch oben genannte Optimierungen nicht-deterministisches Verhalten auf. Dies führt in der Praxis oft zu Fehlern, insbesondere wenn sich Programmierende der Problematik nicht bewusst sind.

Die oben beschriebene Problematik wird dadurch verschärft, dass jede Prozessorarchitektur (x86, amd64, arm, ...) stark unterschiedliche Optimierungen integriert/erlaubt. Aus diesem Grund soll der zu entwickelnde CPU-Simulator nicht für eine a priori gewählte Prozessorarchitektur implementiert werden, sondern die Prozessorarchitektur soll frei wählbar sein. In Forschung und Praxis wird hierzu eine relationale Beschreibung von Prozessorarchitekturen verwendet, die unser CPU-Simulator ebenfalls nutzen soll.

Projektseite

Weitere Information sind der Projektseite zu entnehmen: ➥ zur Projektseite.

Betreuer

Betreut wird das Projekt durch Roland Meyer, Peter Chini, und Sebastian Wolff. Ansprechpartner sind Peter Chini und Sebastian Wolff.