Polyspace Code Prover is a commercial software verification tool. I exchanged many emails and four phone calls with Mathworks in order to convince them to give me a one-month free trial. Unlike my usual toolset, it is not “free as in freedom”, it is free as in “have fun with those FlexLM bugs, bwahaha”. But, I’m a pragmatist.

PCP can be used to verify C, C++ or Ada code. It is mostly aimed at embedded software development. Contrary to the fears of the Mathworks sales team, it can be used to verify server software. Over the last few days, I’ve used it to find several bugs in PHP’s exif extension. It is awesome and probably smarter than me. It didn’t take long for it to start telling me things about the code that I didn’t know.

The general workflow is:

• Choose a smallish (~2000 line) module
• Polyspace automatically generates stubs to represent all undefined functions, and generates a main() function which calls all exported (i.e. non-static) functions
• Analysis generates hundreds of “orange” checks
• You then refine the stub and main generation, and tweak the source as necessary, in order to reduce the number of orange checks
• The remaining orange checks can be acknowledged with saved comments on the analysis.

PCP describes orange checks as “unproven code”, but that terminology downplays their severity. An orange check can be a blatant bug, for example:

char * p = malloc(1);
*p = 'x';

PCP knows that malloc() can fail and return NULL, and will flag the dereference orange, to point out that you haven’t checked for that.

The fact that PCP is mostly intended for embedded systems is fairly obvious. Stubs for standard library functions are provided, but POSIX functions such as stat() are missing and need to be written by the user. Perhaps the biggest weakness is its string handling. For example, its sprintf() stub is essentially:

int sprintf(char *s, const char *format, ...)
{
	int length;
	int i;
	ASSERT_IS_VALID_STRING(format);
	length = _polyspace_random_int();
	if (length < 0) {
		length = 0;
	}
	for (i=0; i < length; i++) {
		s[i] = _polyspace_random_char();
	}
	s[length] = 0;
	return length;
}

This is, of course, a gross simplification of this fraught function, and leaves plenty of room for uncaught segfaults.

PCP has a system for customising automatic generation of stub functions, called DRS. I didn’t have much luck with it — I found that progress was much faster when I just wrote the stub functions in C, following examples from polyspace/verifier/cxx/cinclude/__polyspace__stdstubs.c . DRS focuses on specifying valid ranges for numbers, which wasn’t a particularly useful approach for my test case.

Getting started with Polyspace Code Prover

PCP has some stupid defaults which you need to be careful with:

• When adding include paths, “add recursively” is checked by default. You really don’t want to add /usr/include recursively. Those include paths are equivalent to -I options to gcc, except without system defaults. They need to be non-recursive and correctly ordered.
• “Target processor type” defaults to i386 on an x86-64 system
• Check Behavior > Overflow computation mode: should be “wrap-around”, to match the compiler.
• Precision: These options control the run time and model complexity. I’ve found precision level 1 and verification level 0 to be sufficient for initial exploration, and a run at that level takes a mere 40 minutes for my exif.c test case. A run to verification level 4 took about 10 processor-hours and maybe 1.5 GB per core of RAM. It’s probably good to have a long-running configuration prepared so that you can quickly start it to run overnight before you leave your computer for the day.

Some bugs I found:

• It doesn’t seem to like assignment expressions, for example in the condition of an if statement. Well, who can blame it, I don’t like them either. The affected assignments were ignored.
• It miscounted the length of a string literal containing null bytes. I couldn’t reproduce it in an isolated test case.
• The engine sometimes failed with “Maximum number of users for PolySpace_Bug_Finder_Engine reached”. The solution for this was rm /dev/shm/sem.mw*.
• The FlexNet binaries in etc/glnxa64 had the wrong ELF interpreter, so attempting to run them would fail with “file not found”. You can identify the interpreter with objdump -j .interp -s lmutil and then symlink it to your actual interpreter, e.g. ln -s /lib/x86_64-linux-gnu/ld-2.15.so /lib64/ld-lsb-x86-64.so.3

It’s not for the faint hearted. But, with patience, you can test code in a way which is mostly orthogonal to human code review, unit testing and fuzz testing. Powerful static analysis tools like PCP could make a valuable contribution to security testing of server code.