splint how to perform taint analysis

Question

How to perform Taint Analysis using Splint?

I have installed Splint on my Ubuntu 12.04. Created a small test case as below:

#include<stdio.h>
#include<string.h>
int main(int argc, char *argv[]) {
    char a[10];
    strncpy(a,argv[1],10);
    printf(a);
    return 0;
}

Also created splint.xh file with the following contents:

int printf  (/*@untainted@*/ char *fmt, ...);
char *fgets (char *s, int n, FILE *stream) /*@ensures tainted s@*/ ;
char *strcat (/*@returned@*/ char *s1,  char *s2) /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ ;
void strncpy (/*@returned@*/ char *s1,  char *s2, size_t num)    /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ ;

Also created splint.mts file with the below contents:

    attribute taintedness
       context reference char *
       oneof untainted, tainted
       annotations
         tainted reference ==> tainted
         untainted reference ==> untainted
                       transfers
         tainted as untainted ==> error "Possibly tainted storage used where untainted required."
       merge
          tainted + untainted ==> tainted
       defaults
          reference ==> tainted
          literal ==> untainted
          null ==> untainted
    end

Then finally ran the splint tool with the command:

    splint -mts splint prg001.c

Where prg001.c is the sample input, "splint" refers to splint.mts and splint.xh file. All the files are in the current directory.

The output I received is:

Splint 3.1.2 --- 21 Aug 2012

prg001.c: (in function main) prg001.c:6:1: Format string parameter to printf is not a compile-time constant: a 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) prg001.c:3: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 --- 2 code warnings

There is no hint of any taint analysis in the output. Can someone please help me on how to get the taint analysis done using Splint.

Thanks

Answer 1

The problem was with splint.xh file.

I change the printf to printfxxx and it worked fine.

This implied that standard definition was overwriting my .xh file. This solved my problem and now the splint outputs tainted variables and the flow of taint.