夹板如何进行污秽分析

Question

如何用夹板进行污秽分析？

我在我的Ubuntu12.04上安装了夹板。创建了一个小型测试用例，如下所示：

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

还创建了具有以下内容的splint.xh文件：

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 @*/ ;

还创建了具有以下内容的splint.mts文件：

    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

最后，使用以下命令运行夹板工具：

    splint -mts splint prg001.c

其中prg001.c是示例输入，"splint“指的是splint.mts和splint.xh文件。所有文件都在当前目录中。

我收到的输出是：

3.1.2 -2012年8月21日

prg001.c：(在函数main中) prg001.c:6:1:格式字符串参数到printf不是编译时常量:格式参数在编译时不知道。这可能导致安全漏洞，因为无法检查参数的类型。(使用-formatconst抑制警告) prg001.c:3:14:参数argc不使用函数参数不在函数体中使用。如果参数是类型兼容性或未来计划所需的，请在参数声明中使用/@ use @/。(使用-paramuse抑制警告)

检查完毕-2个代码警告

输出中没有任何污点分析的迹象。有人能帮我用夹板做污物分析吗？

谢谢

Answer 1

问题在于splint.xh文件。

我将printf改为printfxxx，它运行良好。

这意味着标准定义覆盖了我的.xh文件。这解决了我的问题，现在夹板输出受污染的变量和污点流。