Шина, как выполнить анализ заражения

Question

Как выполнить анализ Taint с использованием Splint?

Я установил 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 -mts splint prg001.c

Где prg001.c - пример ввода, "splint" относится к файлу splint.mts и splint.xh. Все файлы находятся в текущем каталоге.

Вывод, который я получил:

Шина 3.1.2 --- 21 августа 2012

prg001.c: (в функции main) prg001.c:6:1: параметр строки формата в printf не является константой времени компиляции: параметр Format неизвестен во время компиляции. Это может привести к уязвимостям безопасности, поскольку аргументы не могут быть проверены по типу. (Используйте -formatconst для блокировки предупреждения) prg001.c:3:14: Параметр argc не используется Параметр функции не используется в теле функции. Если аргумент необходим для совместимости типов или будущих планов, используйте /@ unused @/ в объявлении аргумента. (Используйте -paramuse, чтобы запретить предупреждение)

Закончена проверка --- 2 предупреждения кода

Там нет никакого намека на какой-либо анализ порчи в выводе. Может кто-нибудь, пожалуйста, помогите мне о том, как сделать анализ порчи, используя Splint.

Спасибо

Answer 1

Проблема была с файлом splint.xh.

Я изменил printf на printfxxx, и он работал нормально.

Это подразумевало, что стандартное определение переписывало мой файл.xh. Это решило мою проблему, и теперь шина выводит испорченные переменные и поток порчи.