From efa58ef316a8c29ae0ba899136c5dee6c88f9910 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 21 Sep 2016 09:33:39 +0200 Subject: [PATCH 1/1] Initial commit --- prefast/.chktexrc | 1 + prefast/.gitignore | 3 + prefast/Makefile | 11 ++ prefast/MartLubbers_answers.tex | 54 ++++++++++ prefast/MartLubbers_prefast_exercise.cpp | 125 +++++++++++++++++++++++ 5 files changed, 194 insertions(+) create mode 100644 prefast/.chktexrc create mode 100644 prefast/.gitignore create mode 100644 prefast/Makefile create mode 100644 prefast/MartLubbers_answers.tex create mode 100644 prefast/MartLubbers_prefast_exercise.cpp diff --git a/prefast/.chktexrc b/prefast/.chktexrc new file mode 100644 index 0000000..aa8ac8f --- /dev/null +++ b/prefast/.chktexrc @@ -0,0 +1 @@ +VerbEnvDir { texttt } diff --git a/prefast/.gitignore b/prefast/.gitignore new file mode 100644 index 0000000..3eec47d --- /dev/null +++ b/prefast/.gitignore @@ -0,0 +1,3 @@ +*.aux +*.log +*.pdf diff --git a/prefast/Makefile b/prefast/Makefile new file mode 100644 index 0000000..c6c449f --- /dev/null +++ b/prefast/Makefile @@ -0,0 +1,11 @@ +DOCUMENTS:=MartLubbers_answers +PDFLATEXFLAGS:=-halt-on-error +PDFLATEX:=pdflatex $(PDFLATEXFLAGS) + +all: $(addsuffix .pdf,$(DOCUMENTS)) + +%.pdf: %.tex + $(PDFLATEX) $< + +clean: + $(RM) -v $(addprefix $(DOCUMENTS).,pdf log aux) diff --git a/prefast/MartLubbers_answers.tex b/prefast/MartLubbers_answers.tex new file mode 100644 index 0000000..4f42887 --- /dev/null +++ b/prefast/MartLubbers_answers.tex @@ -0,0 +1,54 @@ +\documentclass[a4paper]{article} + +\usepackage[british]{babel} +\usepackage[british]{isodate} +\usepackage{geometry} + +\title{Program Analysis with \emph{PREfast} and \emph{SAL}} +\date{\printdate{21.9.2016}} +\author{Mart Lubbers (s4109503)} + +\begin{document} +\pagenumbering{gobble} +\thispagestyle{empty} +\clearpage +\maketitle +\begin{enumerate} + \item\emph{PREfast tries to check annotations at compile time. Suppose that + we have a way to check the annotations at runtime. (Actually, it is not + so straightforward to do this at runtime, for all annotations, but + let's assume it is possible.) Name one advantage and two disadvantages + of doing these checks at runtime instead of doing them at compile-time. + (Hint: there are very generic advantages and disadvantages when it + comes to runtime vs compile-time checking.)} + + An advantage is that you can inspect the actual value of the variable + and check whether the buffer is big enough. (Assuming the tool keeps + track of the buffersize). + A disadvantage would be the overhead that is added to the program. + Checking all these things at runtime costs processor time and will + result in slower programs. + Lastly, another disadvantage is that it is difficult to check all + runtime configurations when using dynamic buffer sizes, so that will + mean that you require a very big testset which you have to design then. + In other words; you have to the same work twice, once while annotating + and once writing a testset. + \item\emph{Sometimes PREfast only warns about problems \textbf{after} you + add annotations. For example, the tool does not complain about + \texttt{zero()} until after you add an annotation about the size of + \texttt{buf}. An alternative tool design would be to produce a warning + about \texttt{zero()} if there are no annotations for it. (The warning + would then not so much be that there is a potential buffer overflow + problem, but rather that the tool does not have enough information to + determine whether there is a buffer overflow or not.) Can you give a + plausible explanation why PREfast has been designed so that it does not + complain about such unannotated methods?} + + It might very well be that a lot of the functions handling buffers are + not in any way in danger of causing a buffer overflow and therefore the + tool will spew out way to many warnings and it then forces the user to + do excessive annotating just to get rid of warning that are not + dangerous in the first place. +\end{enumerate} + +\end{document} diff --git a/prefast/MartLubbers_prefast_exercise.cpp b/prefast/MartLubbers_prefast_exercise.cpp new file mode 100644 index 0000000..219bf87 --- /dev/null +++ b/prefast/MartLubbers_prefast_exercise.cpp @@ -0,0 +1,125 @@ +#include "stdafx.h" +#include "stdio.h" +#undef __analysis_assume +#include + +#define BUF_SIZE 100 +#define STR_SIZE 200 + +void zeroing(); + +char *my_alloc(size_t size) +{ + //FIXED + char *ch = (char *)calloc(size, 1); + if (ch == NULL){ + perror("malloc"); + exit(EXIT_FAILURE); + } + return ch; +} + +bool input([SA_Post(Tainted=SA_Yes)] _Out_cap_c_(BUF_SIZE) char *buf) +{ + //FIXED + return (gets_s(buf, BUF_SIZE) != NULL) ? true : false; +} + +[returnvalue:SA_Post(Tainted=SA_Yes)] char *do_read() +{ + //FIXED + char *buf = my_alloc(STR_SIZE); + printf("Allocated a string at %p", buf); + if(!input(buf)){ + puts("Error!"); + exit(EXIT_FAILURE); + } + if (buf[0] == '\0') + printf("empty string"); + return buf; +} + +void copy_data([SA_Pre(Tainted=SA_Yes)]_In_count_c_(STR_SIZE) char *buf1, [SA_Post(Tainted=SA_Yes)] _Out_cap_c_(STR_SIZE) char *buf2) +{ + memcpy(buf2,buf1,STR_SIZE); + buf2[STR_SIZE-1] = NULL; // null terminate, just in case +} + +int execute([SA_Pre(Tainted=SA_No)] _In_count_c_(BUF_SIZE) char *buf) +{ + return system(buf); // pass buf as command to be executed by the OS +} + +void validate([SA_Pre(Tainted=SA_Yes)][SA_Post(Tainted=SA_No)] _Inout_count_c_(BUF_SIZE) char *buf) +{ + // This is a magical validation method, which turns tainted data + // into untainted data, for which the code not shown. + // + // A real implementation might for example use a whitelist to filter + // the string. +} + +_Check_return_ int test_ready() +{ + // code not shown + return 1; +} + +int APIENTRY WinMain(HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLine, int nCmdShow) +{ + char *buf1 = do_read(); + char *buf2 = my_alloc(BUF_SIZE); + zeroing(); + //FIXED + if(test_ready() != 0){ + printf("Test not ready\n"); + exit(EXIT_FAILURE); + } + //FIXED + validate(buf1); + execute(buf1); + + char* buf3 = do_read(); + copy_data(buf3, buf2); + //FIXED + validate(buf2); + execute(buf2); + + char *buf4 = do_read(); + //FIXED + validate(buf4); + execute(buf4); +} + +// ***************************************************************** + +void zero(_Out_cap_(len) int *buf, int len) +{ + int i; + //FIXED + for(i = 0; i < len; i++) + buf[i] = 0; +} + +void zeroboth( + _Out_cap_(len) int *buf, int len, + _Out_cap_(len3) int *buf3, int len3) +{ + int *buf2 = buf; + int len2 = len; + zero(buf2, len2); + zero(buf3, len3); +} + +void zeroboth2(_Out_cap_(len3) int *buf, int len, _Out_cap_(len) int *buf3, int len3) +{ + zeroboth(buf, len3, buf3, len); +} + +void zeroing() +{ + int elements[200]; + int oelements[100]; + //FIXED + zeroboth2(elements, 100, oelements, 200); +} -- 2.20.1