夹板如何执行Taint分析

Question

如何使用夹板进行污染分析？

我在我的Ubuntu 12.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 @*/ ;

.

还创建了具有下面的内容的夹板内容：

    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是示例输入，“拆分”是指致法致法。所有文件都在当前目录中。

我收到的输出是：

夹板3.1.2 --- 2012年8月21日

prg001.c :(在功能主要） prg001.c：6：1：格式字符串参数到printf不是编译时间常数： 一种 格式参数在编译时未知。这可以导致安全性 漏洞，因为争论不能键入选中。 （用 -FormatConst禁止警告） prg001.c：3：14：未使用参数ARGC 函数参数不使用该功能的主体。如果是争论 类型兼容性或未来计划需要，使用/ @ / 论证宣言。 （使用-Paramuse禁止警告）

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

输出中没有任何污染分析。有人可以帮助我如何使用夹板完成Taint分析。

感谢

Answer 1

问题在于splint.xh文件。

我将printf更改为printfxxx，它工作正常。

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