Enhancing abstraction and symbolic execution for shape analysis of C-programs operating on linked lists

Abstract

Diese Arbeit beschreibt Verbesserungen für das statische Analysetool Broom. Broom analysiert Programmteile eines C-Programmes und beweist, dass es frei von Speicherfehlern ist. Im Besonderen ist Broom in der Lage, Programme, die mit verschiedenen Varianten von verketteten Listen arbeiten, zu analysieren. Falls Broom das Eingabeprogramm als sicher klassifiziert, erzeugt es für jede Funktion eine Menge an Zusicherungen, die in einer bestimmten Form von Separation Logic definiert werden.Broom ist derzeit noch ein Prototyp und die Komplexität der Listen, die analysiert werden können, ist begrenzt. Deshalb wurde der Abstraktionsalgorithmus von Broom im Rahmen dieser Arbeit so erweitert, dass er auch Listen unterstützt, bei denen jeder Knoten einen Zeiger auf ein gemeinsames Objekt hat. Diese Verbesserung ist praktisch relevant, da diese Listen gerne in systemnahen Code verwendet werden. Darüber hinaus beschäftigt sich diese Arbeit mit dem Problem der Explosion des Zustandsraumes bei der Analyse komplexerer Funktionen. Es wurde in weiterer Folge eine Prozedur implementiert, die diesen Zustandsraum so beschneidet, dass die Zahl der Zusicherungen für eine Funktion signifikant reduziert wird. Besipielsweise führt diese Verbesserung dazu, dass die Zahl der Zusicherungen, die für eine Funktion, die über eine verschachtelte Liste iteriert, von 400 auf zwei reduziert wird. Als Konsequenz konnte die Dauer der Analyse des entsprechenden Codes auf vier Minuten reduziert werden,während die Analyse vor der Implementierung der Verbesserungen praktisch unmöglich war.

This thesis describes improvements of the static analyser Broom. Broom can analyse fragments of programs written in the programming language C proving the absence of memory bugs. Specifically, the tool supports programs operating on different kinds of linked lists. If Broom considers the input program as safe, it generates for each function a set of contracts, which are defined in a special flavour of Separation Logic. Broom is still a prototype and the complexity of the lists that can be analysed is limited.To this end we extended Broom’s abstraction procedure such that also lists with pointers to shared non-global heap objects, which are common in system code, can be analysed. Additionally we tackled the state space explosion problem, which may occur when Broom analyses more complex functions. We implemented a pruning strategy that significantly reduces the number of contracts for these functions. This improvement allowed us to reduce the number of contracts that would be generated for a function traversing a nested list from over 400 to two. This results in an analysis of the respective code within approximately four minutes while analysing this code was practically infeasible before the pruning was implemented.