03.03.2021, 14:00 Uhr
Durchführung per Videokonferenz
(Corona-Situation)
Titel: „New Symbolic Execution Pass for the CASM Language“
Kurzfassung:
Heutzutage ist es wichtig, dass Software korrekt arbeitet, da sie oft auch in sicherheitskritischen
Bereichen verwendet wird. Eine Methode zur Beschreibung von Software sind
Abstract State Machines (ASM). ASMs sind eine Erweiterung von Finite State Machines
(FSM) und sind formal definiert. Da sie auf mathematischen Grundlagen basieren, ist es
möglich, bestimmte Eigenschaften mittels formalen Methoden zu beweisen. Es müssen
jedoch nicht nur die modellierten Systeme fehlerfrei sein, sondern auch die Compiler, welche
verwendet werden, um die abstrakte Repräsentation in eine ausführbare Datei zu übersetzen.
Diese dürfen keine Fehler einbringen. Translation Validation ist eine Möglichkeit zu
zeigen, dass ein bestimmter Compilier-Vorgang fehlerfrei ist. Für Translation Validation
wird ein mathematisches Modell der Input Spezifikation und des Outputs erstellt und
gezeigt, dass die Modelle ident sind.
Diese Arbeit ist der erste Schritt in Richtung Translation Validation im Corinthian
Abstract State Machine (CASM) Compiler, indem es ein Framework präsentiert, welches
eine in CASM geschriebene ASM in ihre Repräsentation in der TPTP Sprache übersetzt.
Die Arbeit basiert auf einem von Lezuo [48] vorgestellten Ansatz. Die TPTP Sprache ist
als Input für Automated Theorem Prover (ATP) Systeme entworfen. Die Transformation
unterstützt concolic execution. Um sicherzustellen, dass dabei numerische Funktionen nicht
symbolischen Werten zugewiesen werden, wird in dieser Arbeit ein neues System vorgestellt,
welches vor der Transformation das Auftreten solcher Zuweisungen prüft. Falls derartige
Zuweisungen existieren, wird die entsprechende Funktion von numerisch zu symbolisch
umgewandelt. Außerdem wird eine direkte Transformation von TPTP zu einem Model für
den Satisfiablity Modulus Theories (SMT) Solver Z3 vorgestellt.