2

如何使用 Splint 进行污点分析？

我已经在我的 Ubuntu 12.04 上安装了 Splint。创建了一个小测试用例，如下所示：

#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 函数体中未使用函数参数。如果类型兼容性或未来计划需要参数，请在参数声明中使用 / @unused@ /。（使用 -paramuse 禁止警告）

完成检查 --- 2 个代码警告

输出中没有任何污点分析的提示。有人可以帮助我了解如何使用 Splint 完成污点分析。

谢谢

4

1 回答 1

1

问题出在 splint.xh 文件上。

我将 printf 更改为 printfxxx 并且效果很好。

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

于 2012-10-06T07:29:19.970 回答