Static analysis

Static analysis is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to dynamic analysis, which basically means testing the software by running it on sample cases in the hope of exercising a bug.

How it works in a nutshell

Let us try Pagai, one of our tools, on this C program (an admittedly artificial example):

int f() {
	int i = 0;
	int j = 0;

	while (i < 50) {
		j = 0;
		while (j < 50) {
			i++;
			j++;
		}
		i = i-j+1;
	}
	return i+j;
}

The tool can be asked to output an annotated program as follows:

int f() {
	int i = 0;
	int j = 0;

	/* invariant:
	50 + -1 * j >= 0
	-1 * j + 50 * i >= 0
	j + -1 * i >= 0
	*/
	while (i < 50) {
		j = 0;
		/* invariant:
		50 + -1 * j >= 0
		-1 * j + i >= 0
		49 + j + -1 * i >= 0
		j >= 0
		*/
		while (j < 50) {
			i++;
			j++;
		}
		i = i-j+1;
	}
	/* invariant:
	-50 + i = 0
	-50 + j = 0
	*/
	return i+j;
}

The comments marked as invariants are properties that are true throughout the execution (thus “invariants”). Technically, they are inductive invariants because they are shown to be true throughout a program execution by mathematical induction.

The way our static analysis tool work is by deriving such properties, then showing that they entail user-specified assertions or other properties of interest. The user may also specify some assumptions about the environment of the program (library functions whose source code is not provided, external inputs...).

Caveats

Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it cannot occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide false negatives — failing to point some issue that the tool is claimed to detect.

This sounds too good to be true, and you may think there should be a catch. There are actually several.

The main one is that a tool cannot be both sound and complete — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — false positives or false alarms. This is unavoidable, as it is a consequence of mathematical properties of computable functions (the mathematical constructs underlying computer programs), more precisely of Rice's theorem.

Another issue is that research tools, and also some commercial tools, often make simplifying assumptions about computer programs so as to make matters easier. For instance, the tool may assume that all integer computations operate over mathematical integers (ℤ), or that all floating-point computations operate over mathematical reals (ℝ). It may also assume some cleanliness about memory usage and pointer arithmetic. Tools such as Astrée or PolySpace try to be faithful to machine models in this respect.

Finally, an analyzer is a complex piece of software, which means that it most probably contains bugs. This is why the VERASCO project, a sister project of CompCert, is building a tool that is proved correct using the Coq proof assistant. Due to the sheer difficulty of such a task, however, VERASCO is looking to build into this tool only established static analysis techniques, while STATOR aims at developing cutting-edge approaches and algorithms.