汚染分析を実行する方法

Question

Splintを使用して汚染解析を行う方法？

私は私の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 @*/ ;

.

以下の内容で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ツールを実行しました：

    splint -mts splint prg001.c

.

ここで、prg001.cがサンプル入力である場合、「splint」はsplint.mtsとsplint.xhファイルを指します。すべてのファイルは現在のディレクトリにあります。

受信した出力は次のとおりです。

Splint 3.1.2 --- 2012年8月21日

PRG001.C :(機能メイン） PRG001.C：6：1：FORMAT STRING PRINTFのコンパイル時定数ではありません。 A. formatパラメータはコンパイル時には知られていません。これはセキュリティにつながる可能性があります 引数を入力することができないため、引数を調べることができないため、脆弱性。 （使用する 警告を禁止するためのフォーマットコンテンスト PRG001.C：3：14：パラメータargcは使用されていません 関数パラメータは関数の本文では使用されません。議論なら タイプの互換性または将来の計画に必要な場合は、/ @unused @ /内 引数宣言（警告を禁止するために - パラミュースを使用してください）

最新の検査--- 2コード警告

出力内の汚染解析のヒントはありません。誰かがSplintを使って汚染分析を行う方法について私を助けてください。

ありがとう

Answer 1

問題はsplint.xhファイルを含むものでした。

PRINTFをPRINTFXXXに変更してうまく機能しました。

これは、標準の定義が私の.xhファイルを上書きされていたことを暗示しました。これは私の問題を解決し、今や副作用の成果と汚染された変数と汚染の流れ。