夾板如何執行污點分析

我在我的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 (/*@[email protected]*/ char *fmt, ...); 
char *fgets (char *s, int n, FILE *stream) /*@ensures tainted [email protected]*/ ; 
char *strcat (/*@[email protected]*/ char *s1, char *s2) /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ ; 
void strncpy (/*@[email protected]*/ 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：（在功能主要） prg001.c：6：1：格式字符串參數printf不是編譯時常量： a 格式參數在編譯時未知。這可能導致安全漏洞，因爲參數不能被類型檢查。（使用 -formatconst禁止警告） prg001.c：3：14：未使用參數argc 功能體中未使用函數參數。如果需要參數用於類型兼容性或未來計劃，請使用/ @未使用@ /參數聲明中的。（使用-paramuse抑制警告）

完成檢查--- 2碼警告

沒有輸出任何污點分析的跡象。有人可以幫助我如何使用Splint完成污點分析。

謝謝

來源

2012-09-29 Romaan

我還測試了從fgets函數中輸入字符數組並打印它。但輸出沒有關於污點的線索 – Romaan

問題出在splint.xh文件中。我將printf更改爲printfxxx，它工作正常。這意味着標準定義覆蓋了我的.xh文件。這解決了我的問題 – Romaan

問題出在splint.xh文件。

我將printf更改爲printfxxx，它工作正常。

這意味着標準定義覆蓋了我的.xh文件。這解決了我的問題，現在夾板輸出污染變量和污染流。

來源

2012-10-06 07:29:19 Romaan

夾板如何執行污點分析

回答

相關問題