At the Source

It's Worth It

Adding comments to Splint source code sounds unproductive, but remember that Splint only criticizes what it deems to be unusual – that is, what a third party reading the source code would also stumble over. By the way, after a few months, even the program's author practically becomes a third party. Moreover, the Splint comments make you aware of where the pitfalls lie. Once seen and documented, they can also be avoided.

The comments are reminiscent of Hoare logic, a formal program verification method. The developer defines preconditions, a computational step, and an end condition. The final condition must be derived from the precondition by the calculation step. If you want to read about this in more detail, you can find the original article online [10].

This very formal approach has limited suitability for many application programs, but it is a good school of thought, because it forces you not "simply" to convert the individual program steps into code form, but really to rethink them.

RATS Catcher

If you find Splint too finicky and detailed, try domesticating RATS (rough auditing tool for security) [11]. Instead of concrete warnings, the tool gives more general hints on critical code locations. You can install RATS with the classic five-step sequence:

unzip rough-auditing-tool-for-security-master.zip
cd rough-auditing-tool-for-security-master
./configure
make
make install # if so desired

Listing 7 shows the RATS output at warning level 3 (-w3; compare with Listing 3 for Splint -strict reporting). If the tool only resides in the current directory and has not been installed, the path to rats-c.xml, which describes typical C errors, must be passed in with the -d option.

rats -w3 example1.c
Entries in c database: 310
Analyzing example1.c
example1.c:7: High: fixed size local buffer
Extra care should be taken to ensure that character arrays that are allocated on the stack are used safely. They are prime targets for buffer overflow attacks.
example1.c:8: High: strcpy
Check to be sure that argument 2 passed to this function call will not copy more data than can be handled, resulting in a buffer overflow.
example1.c:9: High: printf
Check to be sure that the non-constant format string passed as argument 1 to this function call does not come from an untrusted source that could have added formatting characters that the code is not prepared to handle.
Total lines analyzed: 11
Total time 0.000192 seconds
57291 lines per second

RATS messages help developers find the critical points in the code, and the explanations are quite understandable, especially with regard to security problems. However, Splint additionally points out further problems in the source code, beyond known security risks. Splint's checks are also more substantial. In comparison, the corrected program version in Listing 5 provokes two warnings from RATS, both false positives, triggered by the "fixed buffer size" and strncpy() detection features.

Where false positives raise their heads, the risk of overlooking genuine problems becomes more real. The resulting impression of having done everything possible in terms of security is fatal, of course. On the positive side, however, RATS can rightly claim that it is able to check code in many programming languages.

Commercial Coverity

Coverity is not free software, but it is well known for its detection capabilities in the open source scene. Coverity [12] is a commercial tool for static code analysis of C, C++, C#, and Java programs. It comes in a local variant and as a cloud service. The extent to which the cloud service is compatible with your own corporate policy and legal requirements such as GDPR is something you have to decide for yourself.

If you manage an open source project that is recognized by the manufacturer, you can use the cloud branch [13] to perform code analysis free of charge. The service is used by the Linux kernel project, and since this testing began, the code quality has increased significantly, as measured by the number of findings.