BUFFERCHECKING

   1                         Buffer Overflow Checking
   2                             David Larochelle
   3                              15 August 2001
   4
   5
   6 This is a preliminary guide to the buffer overflow checking in LCLint
   7 Version 3.0.  This alpha version contains additional checking not
   8 documented in the manual for LCLint 2.5.
   9
  10 Although this document provides a quick introduction for the new
  11 features of LCLint it is not intended as a substitute for the LCLint
  12 manual.  We recommend that users unfamiliar with LCLint consult the
  13 LCLint user guides in addition to this document.
  14
  15 The types of errors which LCLint reports can be controlled flags.
  16 Theses flags can be set on the commands line or in .lclintrc files.  A
  17 flags by giving LCLint the +flagname option on the command line or in a
  18 .lclintrc file where flagname is the name of the flag.  Similarly flags
  19 are unset with -flagname.
  20
  21 Overview
  22 ========
  23
  24 LCLint detects buffer overflow errors by generating precondition and
  25 postcondition constraints at the expression level.  We resolve
  26 constraints using post conditions from previous statements.  We generate
  27 an error message for any constraints which we are unable to resolve at
  28 the top of a function.
  29
  30 All checking takes place within functions.  Interprocedural properties
  31 are checked using annotations.  Annotated versions of the standard
  32 libraries are provided innerally.
  33
  34 The new annotations allow programmers to explicitly state function
  35 preconditions and postconditions using requires and ensures clauses.  We
  36 can use these clauses to describe assumptions about buffers that are
  37 passed to functions and constrain the state of buffers when functions
  38 return.  For the analyses described here two kinds of assumptions and
  39 constraints are used: maxSet, and maxRead.
  40
  41 When used in a requires clause, the maxSet annotation describes
  42 assumptions about the lowest and highest indices of a buffer that may be
  43 safely used as an lvalue (e.g., on the left-hand side of an assignment).
  44 For example, consider a function with an array parameter a and an
  45 integer parameter i that has a precondition requires maxSet(a) >= i.
  46 The analysis assumes that at the beginning of the function body, a[i]
  47 may be used as an lvalue.  If a[i+1] were used before any modifications
  48 to the value of a or i, LCLint would generate a warning since the
  49 function preconditions are not sufficient to guarantee that a[i+1] can
  50 be used safely as an lvalue.  Arrays in C start with index 0, so the
  51 declaration char buf[MAXSIZE] generates the constraints maxSet(buf) =
  52 MAXSIZE - 1 and minSet(buf) = 0.  Similarly, the maxRead constraint
  53 indicates the maximum indices of a buffer that may be read safely.  The
  54 value of maxRead for a given buffer is always less than or equal to the
  55 value of maxSet.  In cases where there are elements of the buffer have
  56 not yet been initialized, the value of maxRead may be lower than the
  57 value of maxSet.
  58
  59 Checking is controlled by the following flags.  If the arraybounds flag
  60 is set LCLint will report potential array bounds.  THIS FLAG MUST BE SET
  61 IN ORDER FOR BUFFER OVERFLOW ERRORS TO BE REPORTED.  There are a number
  62 of additional options which can be used to fine tune checking.
  63
  64 If the +arrayboundsread is set LCLint will report cases in which an
  65 index past the end of an array or buffer is read.  The default is to
  66 only report cases in which data is written.  Out of bounds reads are
  67 less dangerous than out of bounds writes but are still security
  68 problems.
  69
  70 The following are used to fine tune the checking.  If the
  71 constraintlocation flag is set LCLint will include the expression which
  72 causes LCLint to generate the unresolved constraint in an error message.
  73 We recommend this options.  The orconstraint is used to perform slightly
  74 more accurate checking by using disjuction internally.  The performance
  75 cost is minimal so we recommend this option.
  76
  77 Handling spurious messages
  78 ==========================
  79
  80 LCLint will occasionally report spurious error messages.  If you see an
  81 error message that you believe to be incorrect first see if you can
  82 correct the problem by adding additional precondition annotations.  For
  83 function with no preconditions LCLint assumes that the function is safe
  84 under all conditions.  Also consider rewriting the code.  Code that is
  85 hard for LCLint to understand is often hard was humans to understand as
  86 well.  You may want to improve the readability and clarity is the code.
  87
  88 If you are sure that the message is spurious you can suppress the
  89 message.  Adding the /*@i@*/ annotation to a line causes LCLint to
  90 suppers all errors generated by the line.  Flags can also be set and
  91 unset within a program.  /*@-flagname@*/ sets a flag to
  92 false. /*@+flagname@*/ sets a flag to true and /*@=flagname@*/ returns a
  93 flag to its previous state.
  94
  95 For example /*@-arroundboundsread@*/ str2[i] = str[i];
  96 /*@=arroundboundsread@*/ would suppress error involving out of bounds
  97 reads for the code fragment.
  98
  99 Frequently Asked Questions
 100 ==========================
 101
 102 I have a function with many buffer overflows but LCLint only reports one
 103 error?
 104
 105 LCLint tries to avoid printing redundant error messages.  We don't print
 106 two constraints if satifying one constraint would satisify another.
 107
 108 LCLint crashes or complains about a bug?
 109
 110 Please report the problem to lclint-bug@cs.virginia.edu
 111
 112 Where can I find more information about LCLint?
 113
 114 The LCLint web site http://lclint.cs.virginia.edu contains a lot of
 115 useful documentation, including a paper describing the LCLint extensions
 116 for buffer overflow checking.  The lclint web site also contains
 117 information on lclint mailing lists.
 118
 119
 120
 121
 122
 123