Bit-level type systems for assembly languages

Abstract

Typsysteme helfen uns auf mehreren Wegen dabei, Software zu schreiben: Sie sind eine Art Sicherheitsnetz und machen es schwieriger, aus Versehen unsichere oder fehlerhafte Programme zu schreiben. Typen sind auch eine Form der Dokumentation und ein Vertrag zwischen mehreren Parteien. Manche Typsysteme sind so weit fortgeschritten, dass sie sogar Vorschläge machen können, wie eine Lücke in einem unfertigen Programm gefüllt werden könnte. Fortschrittlichere Typsysteme findet man üblicherweise in Hochsprachen, während hardwarenahe Sprachen oft untypisiert sind. Um Typsysteme und ihre Vorteile auch in hardwarenahen Sprachen nutzen zu können, ist es also wünschenswert, nicht nur die Befehle einer Hochsprache zu übersetzen, sondern auch ihre Typen. Ein Typsystem für eine Assembly-Sprache muss also Möglichkeiten bieten, die gewünschten Eigenschaften der Typen darzustellen, und zwar vorzugsweise auf allgemeine Weise, und nicht speziell auf eine bestimmte Quellsprache zugeschnitten. Diese Arbeit handelt weniger von der Übersetzung von Typen. Stattdessen soll folgende Forschungsfrage beantwortet werden: „Wie kann ein Typsystem einzelne Bits, aber auch Gruppen von Bits verarbeiten und sicherstellen, dass diese korrekt verarbeitet werden?“ Zunächst definieren wir Fragen, die sich mit grundlegenden Eigenschaften einer Sprache und der Erstellung von Software befassen. Danach wird ein Prototyp eines Assemblers für eine Teilmenge des Arm A64 Befehlssatzes beschrieben. Dieser soll ein einfaches Typsystem aufweisen, in dem die kleinste Einheit das Bit ist. Es sollen Werkzeuge zur Verfügung stehen, um Typen bis zur kleinsten Einheit zu definieren und maximale Kontrolle zu erhalten. Im dritten Schritt werden die zuvor gestellten Fragen anhand des Prototypen beantwortet. Zu guter Letzt wird die Forschungsfrage anhand der erhaltenen Ergebnisse beantwortet. Es lässt sich schließen, dass das vorgeschlagene Typsystem implementiert werden kann und es dem Benutzer erlaubt, verschiedene Varianten geläufiger Typsystemfeatures zu implementieren. Einige eher unübliche Features und Sicherheitschecks für spezielle Anwendungen, welche aber üblicherweise in typisierten Programmiersprachen nicht zu finden sind, können ebenfalls implementiert werden. Die Definition eines Programms und seiner Typen kann jedoch einen größeren Aufwand erfordern als gewöhnlich. Weiters kann die Zeit, die für die Typüberprüfung benötigt wird, ausarten, wenn man nicht genügend Sorgfalt walten lässt.

Type systems help us to write software in various ways: they act as safety nets and make it harder to accidentally write unsafe or incorrect programs. Types are also a form of documentation and a contract between different parties. Some type systems have advanced to a stage where they may even suggest source code to fill holes in an unfinished program. But the more advanced features of type systems are usually only found in high-level languages, while low-level languages like assembly are often untyped. In order to introduce type systems and all their benefits to lower level languages, we may thus wish to translate not only the instructions of a high-level language, but also its types. A type system for an assembly language, then, needs to be able to express the desired properties about types, preferably in a general fashion, rather than in a way that is specifically tailored to one specific source language. In this thesis, we are not concerned so much with the transformation of types, but with the following main research question: “How can a type system handle individual as well as grouped bits and verify that they are processed correctly?” First, we define a set of questions about basic features of a language, and how these features can be used to write software. Second, a prototype assembler for a subset of the Arm A64 instruction set is described. This assembler shall feature a simple type system in which the smallest unit is the bit. The goal is to give the user the tools to define types which are defined down to the smallest unit, giving maximum control. In the third step, this prototype is used to find answers to the questions, which were defined earlier. Finally, the main research question is answered by considering the results that were gained. The final conclusion is that a type system like the one proposed may indeed be implemented and allows the user to express different variations of common type system features. Some rather uncommon features and special purpose safety checks, which are usually not found in typed programming languages, can be implemented as well. The definition of programs with their types may require more effort than in other languages, and if appropriate care is not taken, the time spent on type checking may get out of hand.