2

Splintを使用して汚染分析を実行するにはどうすればよいですか？

Ubuntu12.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 に答える