Fakultät Wirtschaftsinformatik und Angewandte Informatik

Lehrstuhl Softwaretechnik und Programmiersprachen

Abschlussarbeiten zu Praktischen Aspekten der Automatischen Softwareanalyse

 

Context

Ongoing research at the Software Engineering and Programming Languages Research Group concerns the development of a software verification tool, called SOCA. Our tool identifies complex memory-safety violations, e.g., invalid pointer accesses, by symbolically executing paths of a compiled program within an abstract memory model.

The basic analysis method is by translating program paths into bit-vector constraint systems that are annotated with assertions, for each heap cell and pointer dereferenced along a path. A decision procedure for efficiently solving bit-vector problems is then employed as the execution and verification engine.

Extensive case studies on the Linux kernel and its device drivers indicate that SOCA scales well for real-world programs.

MSc Abschlussarbeit / Diplomarbeit:

Developing & Implementing a Property Specification Language for SOCA

While the majority of properties that can be verified using our SOCA tool are currently hard-coded memory-safety properties, we are looking for ways to extend this towards generic properties that are presented to the tool in terms of a temporal specification by the user.

A simple example of such a specification would be that the functions lock() and unlock() must be called alternatingly. Model-checking tools such as SLAM and BLAST already support this kind of specification. However, for most practical purposes, these simple specifications are not enough since functions usually have parameters that have to be taken into account and that must thus be expressible within property specifications. This is especially difficult when the

program to be verified is only available in its compiled representation and when parameters are accessed via indirect addressing.

The goal of this project is to evaluate existing languages for specifying temporal safety properties in software model checking, to either adapt or develop a specification language that fits our requirements, and to integrate that language into the SOCA tool.

We are looking for an MSc or Diplom student with interest in program analysis and good programming skills.

MSc Abschlussarbeit / Diplomarbeit:

Developing & Implementing a GDB Front-End for SOCA

One of the shortcomings of our SOCA tool is that, despite being able to identify interesting memory-safety problems in compiled programs, there is not yet a concise way of presenting these problems to the tool's user.

On the positive side, we can easily provide a path from the considered program's entry point to an offending instruction, including an initial heap configuration that will cause the program to exhibit the erroneous behaviour. On the negative side, all parts of the heap configuration that are not directly relevant will not be present in our path, whence the path cannot be used directly as a test input that would make the program crash.

The goal of this project is to explore possibilities of improving the usability of our tool by either generating complete test inputs for error traces, or by synthesising a "core file" of the crashed program. In either case, an integration into our SOCA tool and the GNU debugger (gdb) is desired.

We are looking for an MSc or Diplom student with interest in program analysis and good programming skills.

BSc Abschlussarbeit: SOCA GUI Development

The goal of this project is to develop a user interface for our SOCA tool. Apart from providing a graphical front-end for selecting input files, output files and parameters, the user interface shall also provide an easily comprehensible indication of the progress SOCA made so far. This includes a visualisation of control-flow graphs and paths that have already been explored, as well as applying coverage metrics to provide an overall indication of the analysis progress and exhaustiveness. Using debug information present in the compiled program being analysed, the visualisation should not be restricted to

assembly statements but also include the actual source code of the program and linked-in libraries.

We are looking for a BSc student with strong programming skills and experience in using debugging tools.

Contacts

Prof. Dr. Gerald Lüttgen

Jan Tobias Mühlberg