Individual Project 1: Program Analysis with PREfast and SAL

Learning objectives

Goals of the project are

• to appreciate - if it wasn't clear from the lectures - some of the many things that can go wrong in a C(++) program;
• to understand the capabilities and the limitations of an (almost) state-of-the-art static analysis tool;
• to understand the trade-offs in the design and in the use of such a tool.

Handing in the assignment

• a file called "YourName_prefast_exercise.cpp" with your modified and annotated C++ code, i.e. part I, and
• a text file YourName_answers.txt or PDF file YourName_answers.pdf with your answers to the questions in part II

NB FOLLOW THESE INSTRUCTIONS TO THE LETTER WHEN HANDING STUFF IN

• make sure your full name and student number is also included in both these files, so that if we print them we know whose they are!
• Preferably, don't zip, tar, gzip, compress, or bzip the attachments! Bandwidth is cheaper than our labour in unzipping stuff. But some mail servers seem to reject .cpp attachments nowadays, so you may have to. I
• No .doc or other formats apart from PDF and plaintext!

Installing PREfast

The assignment - Part I - Using the tool

Running PREfast, by compiling with the option /analyze, should produce 7 warnings: C4996, C6386, C6011, C6217, C6282, C6273, C6031. If you don't get the C4996 warning, the command line option /W 3 is probably missing; you have to include that, as in cl /analyze /W 3 prefast_exercise.cpp

Once that, works follow the steps below:

1. Get rid of the warnings in prefast_exercise.cpp that PREfast gives, by fixing the code. Mark places where you changed the code with a comment //FIXED to keep track of the changes you made.

   Keep the changes to the code minimal; the code is completely silly, no need to completely rewrite it.

2. Annotate all buffers that are passed as parameters (i.e. all parameters of type char* or int*), to specify whether they are read from and/or written to, and specify their lengths. This means you have annotate them
   • with _In_count_(...) if they are only read from;
   • with _Out_cap_(...) if they are only written from;
   • with _Inout_count_(...) if they are both read from and written from (but I don't think you need that).
   If the length is a compile-time constant, such as 55 or BUF_SIZE, rather than a program variable, you need another suffix c_. So, for example, you can annotate a buffer with _Out_cap_(len) or with _Out_cap_c_(BUF_SIZE). (Why this extra c_ is needed for constants is a mystery to me.)

   There is no need to annotate the size of the argument of execute, as its size does not really matter.

   Fix any new warnings this produces.

3. Similarly, annotate the buffers returned as results by my_alloc and do_read to specify their size, using the annotations _Ret_cap_(...) or _Ret_cap_c_(...).

   Fix any new warnings this produces.

4. As last step, we will add tainting annotations to trace any input passing from input to execute without passing through the validation operation, and add calls to the validation routine validate in the right places to fix any problems with missing input validation. The steps for this are explained in more detail below.

   To do this, first

   • annotate the first parameter of input with [SA_Post(Tainted=SA_Yes)], which specifies that this parameter will be tainted as postcondition, and
   • annotate the parameter of execute with [SA_Pre(Tainted=SA_No)] to specify the precondition that this parameter should not be tainted.

   So you get

      HRESULT input([SA_Post(Tainted=SA_Yes)] _Out_... char *buf) {...
   
      int execute([SA_Pre(Tainted=SA_No)] _In_ char *buf) {...
   

   Now annotate all the procedures that may handle or produce tainted data using pre- and/or postconditions as above. These procedures are:

   • do_read, as it calls input, which produces tainted data;
   • copy_data, as it is used to copy data coming from do_read, which is tainted.

   To specify that the return value of a function is tainted, declare it as

      [returnvalue:SA_Post(Tainted=SA_Yes)] char* somefunction() { ...
   

   PREfast should now produce warnings C6029, when it spots that the program is passing tainted data to the function execute().
   Add calls to the validation routine validate in the right places to make such warnings disappear.

   As you may notice, PREfast's tainting analysis is not reliable unless you annotate all procedures that may handle tainted data correctly.

The assignment - Part II - Reflection

1. PREfast tries to check annotations -- and hence the properties they express -- at compile time. An alternative approach would be to check this at runtime. Two different aspects for which this could be done are 1) bounds-checking and 2) tainting & missing input validation. This would require some additional information to be tracked at runtime: For bounds-checking this could involve something like fat pointers to check access out of bounds at runtime; For tainting one would also have to mark data as being tainted.

   Name two advantages and two disadvantages of doing these checks at runtime instead of doing them at compile-time. (I can think of two each. Hint: also think of generic advantages and disadvantages when it comes to runtime vs compile-time checking. Maybe you can think of more?)

2. Sometimes PREfast only warns about problems after you add annotations. For example, the tool does not complain about zero() until after you add an annotation about the size of buf. An alternative tool design would be to produce a warning about 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?

More information for this project

• C(++): to look up what system calls such as gets, gets_s, memcpy, printf, system, ... do, see the online C reference or C++ reference specs.

• Secure coding in C(++): CERT publishes guidelines for this: CERT C coding standard and CERT C++ coding standard. You should not have to look at these for this assignment. But note that if you're ever going to write C(++) code, you will have to.

• SAL: There is a lot of information on SAL on the Microsoft website. But beware, the syntax of SAL keeps changing, so stick to the syntax listed above in the exercises, which is SAL version 2008/2009, as this syntax works with the version of PREfast that we provide.

  If you want to know more about SAL in the latest version, see SAL 2.0 version 2013. The first version of SAL dates back to 2005: SAL version 2005.

  Peter Gutmann's Experiences with SAL/PREfast has some nice discussion and suggestions on how to use PREfast and SAL in practice.