Automated termination analysis of C programs

Hensel, Jera; David, Cristina; Giesl, Jürgen

doi:10.18154/RWTH-2023-10177

Automated termination analysis of C programs

Hensel, Jera^RWTH*

2023 & 2024

Verantwortlichkeitsangabevorgelegt von Jera Hensel, Master of Science

ImpressumAachen : RWTH Aachen University 2023

Umfang1 Online-Ressource : Illustrationen

ReiheAachener Informatik-Berichte (AIB) ; 2023,04

Dissertation, RWTH Aachen University, 2023

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2024

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)^RWTH* ; David, Cristina (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2023-10-12

Online
DOI: 10.18154/RWTH-2023-10177
URL: https://publications.rwth-aachen.de/record/972440/files/972440.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
LLVM (frei) ; c-programs (frei) ; non-termination (frei) ; symbolic execution (frei) ; termination analysis (frei) ; termination proofs (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Das Terminierungsverhalten eines Programms ist eine entscheidende Eigenschaft, die sowohl die Korrektheit als auch die Sicherheit des Programms mitbestimmt. Nichtterminierung und auch unerwünschte Terminierung können zu schwerwiegenden Folgen wie Systemabstürzen und Sicherheitslücken führen. Daher interessieren wir uns für Verfahren, Terminierung von Programmen zu beweisen oder zu widerlegen, um Softwaresysteme zuverlässiger und sicherer zu machen. Die Analyse von C-Programmen ist dabei besonders herausfordernd, da C Konzepte höherer Programmiersprachen mit Zeigern und expliziter Speicherverwaltung kombiniert. In dieser Dissertation erweitern wir einen Ansatz, dessen Stärken in der Terminierungsanalyse von C-Programmen mit Speicherallokation und expliziter Zeigerarithmetik liegen, der aber bisher auf eher kleine, nicht rekursive Programme ohne rekursive Datenstrukturen beschränkt war, bei denen Integer-Variablen als unbeschränkte ganze Zahlen interpretiert wurden. Dieser Ansatz verwendet symbolische Ausführung mit Abstraktion, um das analysierte Programm in ein Integer-Transitionssystem (ITS) zu überführen, welches die Eigenschaft hat, dass Terminierung des ITSs Terminierung des C-Programms impliziert. Anschließend können bestehende Analysetechniken für ITSe verwendet werden, um die Terminierung des Programms zu beweisen. Um die oben genannten Einschränkungen aufzuheben, entwickeln wir neue Verfahren, die nur Anpassungen der Regeln für die symbolische Ausführung sowie der Abstraktionsmethoden erfordern, die anschließend aber die gleiche Überführung in ITSe ermöglichen wie zuvor. Darüber hinaus untersuchen wir, inwiefern derselbe Ansatz für Nichtterminierungsbeweise genutzt werden kann. Alle Erweiterungen sind in unserem Tool AProVE implementiert und werden mithilfe von Vergleichen mit anderen führenden Terminierungsanalyse-Tools evaluiert. Die wesentlichen Beiträge dieser Arbeit sind: (1) Wir stellen ein Verfahren zur Anpassung der bytegenauen symbolischen Ausführung an die Behandlung von Bitvektoren vor. Außerdem diskutieren wir eine Erweiterung des Verfahrens, um die Komplexität von Programmen mit Bitvektoren zu analysieren. (2) Um eine modulare Analyse zu ermöglichen, entwickeln wir eine Methode zur Abstraktion des Laufzeitkellers. Dadurch können symbolische Ausführungen von Hilfsfunktionen innerhalb der Analyse wiederverwendet werden. Unser Verfahren ermöglicht ebenfalls die Behandlung von rekursiven Funktionen. (3) Wir erweitern die Ausdruckskraft von Speicherinvarianten um Invarianten, die die Form, einige Inhalte und die Speicheranordnung von dynamischen Listen beschreiben, und zeigen, wie diese automatisch hergeleitet, angepasst und genutzt werden können, um Terminierung von Programmen mit Listen zu beweisen. (4) Wir diskutieren drei Ansätze zur Analyse von Nichtterminierung und erweitern diese um die Generierung eines nichtterminierenden Beispiel-Pfades durch das gegebene C-Programm.

The termination behavior of a program is a crucial property when reasoning about its correctness and safety. Non-termination and also undesired termination can lead to serious consequences such as system crashes and security vulnerabilities. Therefore, we are interested in techniques to (dis)prove termination of programs to make software systems more secure and reliable. Analyzing the termination behavior of C programs is especially challenging since C combines concepts of higher programming languages with pointers and explicit memory management. In this thesis, we extend a termination analysis approach that is especially powerful for C programs with memory allocation and explicit pointer arithmetic, but which was limited to rather small non-recursive programs without recursive data structures, where all integers were interpreted as unbounded (mathematical) integers. This approach uses symbolic execution with abstraction to convert the analyzed program to an integer transition system (ITS) with the property that termination of this ITS implies termination of the C program. Thus, after this transformation, existing techniques for ITSs can be applied to prove termination of the program. We lift the above mentioned restrictions by new techniques that only require adaptions of the symbolic execution rules and the abstraction methods, but use the same transformation to ITSs as before. Moreover, we investigate how this approach can be modified to prove non-termination. We implemented all extensions in our tool AProVE and evaluate them in comparison with other leading termination tools. The main contributions of this thesis are: (1) We present a technique to adapt byte-accurate symbolic execution to the handling of bitvectors. Furthermore, we discuss how this technique can be used to analyze the runtime complexity of bitvector programs. (2) We develop a method to abstract from call stacks during symbolic execution, allowing a more modular analysis by re-using symbolic executions of auxiliary functions. With this technique, we can also analyze recursive functions. (3) We extend the expressiveness of memory invariants by invariants that describe the shape, some of the contents, and the memory arrangement of dynamically allocated lists and show how these invariants are automatically inferred, adapted, and used during symbolic execution in order to prove termination of programs with lists. (4) We discuss three approaches to analyze non-termination and extend these approaches to produce a non-terminating path through the C program as a violation witness for termination.

OpenAccess:
PDF
(additional files)