--- /dev/null
+VerbEnvDir { texttt }
--- /dev/null
+*.aux
+*.log
+*.pdf
--- /dev/null
+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)
--- /dev/null
+\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}
--- /dev/null
+#include "stdafx.h"\r
+#include "stdio.h"\r
+#undef __analysis_assume\r
+#include <CodeAnalysis\SourceAnnotations.h>\r
+\r
+#define BUF_SIZE 100\r
+#define STR_SIZE 200\r
+\r
+void zeroing();\r
+\r
+char *my_alloc(size_t size)\r
+{\r
+ //FIXED\r
+ char *ch = (char *)calloc(size, 1);\r
+ if (ch == NULL){\r
+ perror("malloc");\r
+ exit(EXIT_FAILURE);\r
+ }\r
+ return ch;\r
+}\r
+\r
+bool input([SA_Post(Tainted=SA_Yes)] _Out_cap_c_(BUF_SIZE) char *buf)\r
+{\r
+ //FIXED\r
+ return (gets_s(buf, BUF_SIZE) != NULL) ? true : false;\r
+}\r
+\r
+[returnvalue:SA_Post(Tainted=SA_Yes)] char *do_read()\r
+{\r
+ //FIXED\r
+ char *buf = my_alloc(STR_SIZE);\r
+ printf("Allocated a string at %p", buf);\r
+ if(!input(buf)){\r
+ puts("Error!");\r
+ exit(EXIT_FAILURE);\r
+ }\r
+ if (buf[0] == '\0')\r
+ printf("empty string");\r
+ return buf;\r
+}\r
+\r
+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)\r
+{\r
+ memcpy(buf2,buf1,STR_SIZE);\r
+ buf2[STR_SIZE-1] = NULL; // null terminate, just in case\r
+}\r
+\r
+int execute([SA_Pre(Tainted=SA_No)] _In_count_c_(BUF_SIZE) char *buf)\r
+{\r
+ return system(buf); // pass buf as command to be executed by the OS\r
+}\r
+\r
+void validate([SA_Pre(Tainted=SA_Yes)][SA_Post(Tainted=SA_No)] _Inout_count_c_(BUF_SIZE) char *buf)\r
+{\r
+ // This is a magical validation method, which turns tainted data\r
+ // into untainted data, for which the code not shown.\r
+ //\r
+ // A real implementation might for example use a whitelist to filter\r
+ // the string.\r
+}\r
+\r
+_Check_return_ int test_ready()\r
+{\r
+ // code not shown\r
+ return 1;\r
+}\r
+\r
+int APIENTRY WinMain(HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLine, int nCmdShow)\r
+{\r
+ char *buf1 = do_read();\r
+ char *buf2 = my_alloc(BUF_SIZE);\r
+ zeroing();\r
+ //FIXED\r
+ if(test_ready() != 0){\r
+ printf("Test not ready\n");\r
+ exit(EXIT_FAILURE);\r
+ }\r
+ //FIXED\r
+ validate(buf1);\r
+ execute(buf1);\r
+\r
+ char* buf3 = do_read();\r
+ copy_data(buf3, buf2);\r
+ //FIXED\r
+ validate(buf2);\r
+ execute(buf2);\r
+\r
+ char *buf4 = do_read();\r
+ //FIXED\r
+ validate(buf4);\r
+ execute(buf4);\r
+}\r
+\r
+// *****************************************************************\r
+\r
+void zero(_Out_cap_(len) int *buf, int len)\r
+{\r
+ int i;\r
+ //FIXED\r
+ for(i = 0; i < len; i++)\r
+ buf[i] = 0;\r
+}\r
+\r
+void zeroboth(\r
+ _Out_cap_(len) int *buf, int len,\r
+ _Out_cap_(len3) int *buf3, int len3)\r
+{\r
+ int *buf2 = buf;\r
+ int len2 = len;\r
+ zero(buf2, len2);\r
+ zero(buf3, len3);\r
+}\r
+\r
+void zeroboth2(_Out_cap_(len3) int *buf, int len, _Out_cap_(len) int *buf3, int len3)\r
+{\r
+ zeroboth(buf, len3, buf3, len);\r
+}\r
+\r
+void zeroing()\r
+{\r
+ int elements[200];\r
+ int oelements[100];\r
+ //FIXED\r
+ zeroboth2(elements, 100, oelements, 200);\r
+}\r
repositories / ss1617.git / commitdiff