夹板如何进行污点分析答案

【问题标题】：splint how to perform taint analysis夹板如何进行污点分析
【发布时间】：2012-09-20 22:05:14
【问题描述】：

如何使用 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 完成污点分析。

谢谢

【问题讨论】：

我还通过从 fgets 函数将输入输入到 char 数组并打印它来进行测试。但是输出没有关于污点的线索
问题出在 splint.xh 文件上。我将 printf 更改为 printfxxx 并且效果很好。这意味着标准定义正在覆盖我的 .xh 文件。这解决了我的问题

标签： c analysis static-code-analysis splint taint

【解决方案1】：

问题出在 splint.xh 文件上。

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

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

【讨论】：