Diploma thesis:

Control Flow Graph based Constraint Evaluation

Motivation:

A "control flow graph" is a data structure that represents an abstract model of a program's functionality. The nodes of this graph are the instruction statements of the program; the vertices are the possible execution paths that connect one instruction to its successors. Sophisticated static analysis of source code often traverses this graph to establish properties of the program that might lead to insecure conditions.

An observation: Many statements in a program can be used to construct constraints which are independent from the program's state.

Example:

                   
    if (a > 0)
    /        \
   /          \ 
then {...}   else {...}	
 [a>0]	       [a <=0]

In this example [a>0] is a constraint, that is true at least for the first node in the "then"-sub tree of the "if"-statement.

Goal:

The goal of this thesis is to (co-)establish a sound system of constraint types and a method of evaluating these constraints (minimizing, combining, etc.) as well as a prototypic implementation of a software tool to construct the constraint system from a control flow graph.

Details:

The theoretical part of the thesis (the development of the constraint system and the connected algorithms) will be done in close cooperation with the thesis' executive supervisors (i.e. Martin J. and/or Daniel S.). The implementation is expected to be done solely by the student.

Contact:

If you are interested, please contact Martin Johns or Daniel Schreckling.

Note: The thesis can be written in German or English.