Splint for C Programmers

Like JSLint, Splint [9] for C offers thorough code analysis. Listing 2 shows a deliberately broken sample program. The potential buffer overflow in line 8 and the format string vulnerability in line 9 are even noticeable in a quick manual review. However, GCC compiles the source code and creates an executable program without putting up much of a fight. Figure 2 confirms how broken the program is.

01  #include <strings.h>
02  #include <stdio.h>
03
04  #define BUFSIZE 10
05  int main(int argc, char * argv [])
06    {
07      char buffer [BUFSIZE];
08      strcpy(buffer, argv[1]);
09      printf(buffer);
10    } // end main()

Figure 2: Disaster is imminent with this sample program.

Before Splint can show whether it can identify the bugs, you need to go through classic steps of downloading, unpacking, compiling, and perhaps installing:

tar -xzf splint-3.1.2.src.tgz
cd splint-3.1.2
./configure
make
make install # if so desired

After winning this battle, Splint needs to know where it can find the header file details. If you omit the install step, they will be in the lib subdirectory, which results in the possible path:

export LARCH_PATH=home/<user>/code/splint-3.1.2/lib/

Some distributions also keep the current Splint binaries in their repositories.

Now, you're ready to go:

/bin/splint -strict example1.c

Listing 3 shows the output and thus the full extent of the digital horror story. Splint uncompromisingly reveals any sloppiness; in fact, it outputs seven warnings, which is far more than gcc -Wall (i.e., output all warnings) shows in Listing 4.

splint -strict example1.c
Splint 3.1.2 --- 11 May 2019
example1.c: (in function main)
example1.c:9:5: Format string parameter to printf is not a compile-time
                   constant: buffer
  Format parameter is not known at compile-time.  This can lead to security
  vulnerabilities because the arguments cannot be type checked. (Use
  -formatconst to inhibit warning)
example1.c:9:5: Called procedure printf may access file system state, but
                   globals list does not include globals fileSystem
  A called function uses internal state, but the globals list for the function
  being checked does not include internalState (Use -internalglobs to inhibit
  warning)
example1.c:9:5: Undocumented modification of file system state possible from
                   call to printf: printf(buffer)
  report undocumented file system modifications (applies to unspecified
  functions if modnomods is set) (Use -modfilesys to inhibit warning)
example1.c:10:4: Path with no return in function declared to return int
  There is a path through a function declared to return a value on which there
  is no return statement. This means the execution may fall through without
  returning a meaningful result to the caller. (Use -noret to inhibit warning)
example1.c:8:5: Possible out-of-bounds store: strcpy(buffer, argv[1])
    Unable to resolve constraint:
    requires maxRead(argv[1] @ example1.c:8:20) <= 9
     needed to satisfy precondition:
    requires maxSet(buffer @ example1.c:8:12) >= maxRead(argv[1] @
    example1.c:8:20)
     derived from strcpy precondition: requires maxSet(<parameter 1>) >=
    maxRead(<parameter 2>)
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
example1.c:8:20: Possible out-of-bounds read: argv[1]
    Unable to resolve constraint:
    requires maxRead(argv @ example1.c:8:20) >= 1
     needed to satisfy precondition:
    requires maxRead(argv @ example1.c:8:20) >= 1
  A memory read references memory beyond the allocated storage. (Use
  -boundsread to inhibit warning)
example1.c:5:14: Parameter argc not used
  A function parameter is not used in the body of the function. If the argument
  is needed for type compatibility or future plans, use /*@unused@*/ in the
  argument declaration. (Use -paramuse to inhibit warning)
Finished checking --- 7 code warnings

gcc -Wall example1.c
example1.c:9:12: warning: format string is not a string literal (potentially insecure) [-Wformat-security]
    printf(buffer);
           ^~~~~~
example1.c:9:12: note: treat the string as an argument to avoid this
    printf(buffer);
           ^
           "%s",
1 warning generated.

Bug Report

The first warning is a reference to the potential format string vulnerability in line 9 of Listing 2. This oversight is not difficult for a QA software tool to detect; because this printf() function requires two parameters, passing only one user-controlled parameters is dangerous. An attacker could simply pass in a format string to printf(), as shown in Figure 2. Printf then looks for data on the stack and tries to read out nonexistent data. With a few tricks, an attacker could thus also overwrite the stack content.

The solution is simple: printf() always needs at least one fixed format string and, if applicable, the strings to be used there. The correct version of line 9 is thus:

printf("%s", buffer)

The second, new warning points to untidy style: main() is declared with an integer type return value, with no return statement in the control flow. If main() does not see a return value, it can lead to unpleasant surprises.

The third warning that Splint issues is about the buffer overflow. Splint failed to see how the programmer had prevented writing beyond the array boundaries of the buffer variable. Although Splint complains about this in a fairly circumstantial way, it is describing the potential overflow. The solution is strncpy(). By the way, this function was added to the ISO C standard in 1990 and is definitely mature enough by now for programmers to use it by default.

In the same line, Splint detects another error: a possible out-of-bounds read. What happens if a call is made without any further parameters? Instead of checking argc first, the program simply assumes there is a parameter. If you try this, you run into another segmentation fault. The last warning also indicates this error: argc was declared as a function parameter, but never used.

If you regularly run Splint against your programs, it will quickly discover small careless errors, and you will be warned of major problem. This approach should be standard, because this type of quality assurance effectively prevents vulnerabilities.

Teaching Splint

Splint might warn you about something, because it lacks the information to assess your code correctly. However, you can fix such warnings by adding comments to the source code. A corrected version of Listing 2 is shown in Listing 5 with control information that keeps Splint from outputting some warnings.

01  #include <strings.h>
02  #include <stdio.h>
03
04  #define BUFSIZE 10
05  int main(int argc, char * argv [])
06    /*@requires maxRead(argv) >= 1 @*/
07    /*@-modfilesys@*/
08    {
09      /*@-initallelements@*/
10      char buffer [BUFSIZE] = {'\0'};
11      /*@+initallelements@*/
12      if ( ( argc > 0 )  && (argv != NULL) )
13        {
14          strncpy(buffer, argv[1], (size_t) (BUFSIZE-1));
15          printf("%s\n",buffer);
16        }
17      return 0;
18    } // end main()

The clues for Splint are bundled in C comments that start and end with at signs (@; e.g., see line 6). Here, the programmer promises that at least argv[1] exists, which puts pay to the out-of-bounds read warning. Line 12 does check for argc, as promised.

Line 7 assures Splint that no filesystem operations are planned, thus alleviating its worries about the printf() in line 15, which has now also been enriched by a proper format string. Line 10 is shorthand that fills the entire array with ASCII 0. Splint does not understand this syntax and would complain that not all elements of the array are filled, but line 9 disables this warning. To make sure Splint continues to examine the rest of the code, line 11 switches monitoring back on again. A plus or minus before the value does the trick.

In line 14, an explicit type conversion has been added – otherwise Splint would complain about the wrong data type. By the way, a classic programming error is taken into account here: C terminates strings with a binary zero, which consumes 1 byte in the buffer; that is, a maximum of nine readable characters fit into a 10-character buffer.

If you want to try this out, have a look at Listing 6, which includes all the required Splint instructions but still provokes an explicit warning (Figure 3).

01 #include <stdio.h>
02 #include <string.h>
03 #define BUFSIZE 10
04
05 int main(/*@unused@*/ int argc,
06          /*@unused@*/ char * argv []
07         )
08   /*@-modfilesys@*/
09   {
10     /*@unused@*/
11     char pwd[18] = "It is top secret!";
12     /*@-initallelements@*/
13     char target [BUFSIZE] = { '\0' };
14     /*@+initallelements@*/
15     char source [17] = "0123456789ABCDEF";
16
17     printf("source: %s\ntarget: %s\n",source,target);
18     strncpy(target, source, (size_t) BUFSIZE );
19     printf("source: %s\ntarget: %s\n",source,target);
20     return 0;
21   }

Figure 3: Splint warns the programmer of a likely out-of-bounds error.