Information Flow Control in Program Dependence Graphs

When verifying software for security, traditional software analysis methods are often insufficient. Our software analysis system ValSoft/Joana uses dataflow-analysis and deductive methods to detect and analyze relevant information flow in programs.

This project develops techniques that detect all illicit information flow in security relevant software. Our goal is to develop analyses that

• guarantee security, i.e. miss no information leak
• analyze established languages, like C or Java
• process larger software systems with acceptable effort
• offer maximal precision, such that very few false alarms are generated

Program dependence graphs form the basic technology for our analyses. These graphs precisely represent all information flow within a program. To classify the sensitivity of data, input and output channels of a program are annotated with security levels. ValSoft/Joana determines using a data flow analysis on the program dependence graph whether data of a certain security level may illicitly reach an unauthorized user of the system. If the analysis detects a possible information leak, it can be further inspected with path conditions: Path conditions represent the precise conditions for information flow between two given statements in a program.

The ValSoft/Joana project offers the following functionality:

• Construction of program dependence graphs for C and Java programs, and their security analysis
• Computation of path conditions for C and Java programs
• User interface and visualization of results in the IDE Eclipse. Illicit data flow is highlighted directly in the source code.

Funded by DFG. Previously funded by BMBF.

Previous work was done at the University of Passau, as well as the Technical University of Braunschweig in cooperation with Physikalisch-Technischen Bundesanstalt and the company LINEAS.

Participants

Publications