9                   Buffer Sizes

Buffer overflow errors are a particularly dangerous type of bug in C programs.  They are directly responsible for about half of all security attacks [Larochelle01].  For performance reasons, C does not perform run time bounds checking.  Referencing storage outside allocated regions can cause memory corruption and lead to strange behavior.  Moreover, buffer overflow bugs are particularly insidious because they can go undetected in testing or normal use, but usually result in security critical bugs.  Reads beyond the end of a buffer can cause the program to leak information.  Writes beyond the end a buffer (buffer overflows) can usually be exploited make the program run arbitrary code.  Attackers can exploit these programming bugs to replace the return address on the stack and place arbitrary code in memory thereby gaining full access to the machine.  Splint is able to detect many memory bounds errors.[12] 

9.1            Checking Accesses

Splint models blocks of contiguous memory using two properties: maxSet and maxRead.  Given a buffer b, maxSet(b) denotes the highest address beyond b that can be safely used as an lvalue.  For the declaration char buf[MAXSIZE] we have maxSet(buf) = MAXSIZE - 1.  Similarly, maxRead denotes the highest index of a buffer that can be safely used an rvalue.  It is inappropriate to read an uninitialized element or beyond the NUL terminator of a null terminated buffer.

When a buffer is accessed as an lvalue, Splint generates a precondition constraint involving the maxSet property.  When a buffer is accessed as an rvalue, Splint generates a precondition constraint involving the maxRead property.  For the expression *ptr, Splint generates the constraints maxSet(ptr) >= 0 or maxRead(ptr) >= 0 depending on whether ptr is used as an lvalue or rvalue.  Similarly, for accesses of the form ptr[i], splint generates the constraints maxSet(ptr) >= i or maxRead(ptr) >= i.  If +boundswrite is set, Splint warns if it is unable to resolve a constraint involving maxSet. If +boundsread is set, Splint warns about unresolved maxRead constraints also.

Splint generates postconditions for statements to help resolve precondition constraints.  When a buffer is written to we know that an element of a buffer is initialized and is safe to read.  We generate the postcondition maxRead(ptr) >= 0 if the buffer is accessed using *ptr or maxRead(ptr) >= i if the buffer is accessed using ptr[i].  Splint generates additional postconditions for a variety of C constructs.  For assignment statements, Splint generates a postcondition equating the two operands.  Splint also generates post condition constraints for the maxSet value of fixed sized arrays.

9.2            Annotating Buffer Sizes

Function declarations may include requires and ensures clauses that specify assumptions about buffer sizes for function preconditions.  They are interpreted like requires and ensures clauses for simple memory states (see Section 7.5) but can be more expressive.  When a function with a requires clause is called, the call site must be checked to satisfy the constraints implied by the requires clause.  Similarly, an ensures clause can be used to specify function post conditions.  If the +checkpost flag is set, Splint warns if it cannot verify that a function implementation satisfies its declared postconditions.

Constraints can contain function parameters as well as global variables and integer constants. The unary operators, maxSet and maxRead which correspond to the properties described above are also supported.  Multiple predicates may be conjoined using /\. 

For example, the standard library annotates strcpy:

void /*@alt char * @*/strcpy

(/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)

/*@modifies *s1@*/

/*@requires maxSet(s1) >= maxRead(s2) @*/

      /*@ensures maxRead(s1) == maxRead (s2) @*/;    

The requires clause indicates that the buffer passed as s1 must be large enough to hold the string passed as s2.  The ensures clause specifies that maxRead of s1 after the call is equal to maxRead of s2.  In cases where the size of s2 is unknown, programs should use strncpy, annotated as:

void /*@alt char * @*/ strncpy

   (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,

  size_t n)

  /*@modifies *s1@*/     

  /*@requires maxSet(s1) >= ( n - 1 ); @*/

  /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n;@*/;

The syntax for buffer size constraint clauses is:

constraint   Þ (requires | ensures) consExpr relOp consExpr

relOp        Þ == | > | >= | < | <=

consExpr  Þ consExpression binOp consExpr | unaryOp (consExpr ) | term

binOp       Þ + | -

unaryOp   Þ maxSet | maxRead

term          Þ identifier | literal | result

9.3            Less Stringent Checking

For some programs, Splint's standard bounds checking produces an unacceptably high number of warnings. Because of this, Splint now prioritizes warnings using a simple heuristic. The flags likely-bounds, likely-bounds-writes, and likely-bounds-read are similar to bounds,bounds-write, and bounds-read, but they only cause Splint to produce warnings for what it determines are likely bounds errors. Splint classifies an unresolved constraint as a likely bounds error if it can reduce the constraint to a numerical inconsistency such as 5 >= 10. Warnings for these constraints are more likely to be legitimate -- indicating real bugs or the lack of annotations. Additionally, when these warnings are false positives, it is easier for humans to recognize them as spurious. These flags generate significantly fewer errors (an order of magnitude in some cases), and the errors generated are easier to understand. However, this does not come without cost. The checking is significantly less precise and is likely to miss real errors.

9.4            Warnings

Since bounds checking is more complex than other checks done by Splint, memory bounds warnings contain extensive information about the unresolved constraint.  Warning messages for unresolved constraints contain both the original constraints and the simplified form of the constraint which cannot be resolved.  If the constraint was derived from a function precondition, the original precondition is included in the error message.  If the +showconstraintlocation flag is set, the message includes the expression that the constraint is derived from.  The +showconstraintparens flag directs Splint to display fully parenthesized constraints in warnings to remove ambiguity.

Consider the code excerpt below containing a trivial out-of-bounds write:

int buf[10];

buf[10] = 3;

Splint warns:

setChar.c:5:4: Likely out-of-bounds store:
    buf[10] = 3

    Unable to resolve constraint: requires 9 >= 10

    needed to satisfy precondition: requires maxSet(buf @ setChar.c:5:4) >= 10

Splint has simplified the constraint from the requires clause to 9 >= 10 by substituting for the known value of maxSet(buf) and generated a warning because 9(the highest index of buf that may be safely written to) is not greater than or equal to 10.

A more realistic example is shown Figure 21.  The function updateEnv is a naïve implementation of a function to copy an environmental variable.  There is no standard restriction on the length of the return value of getenv so this can cause a buffer overflow.  A safe version of updateEnv (such as updateEnvSafe in Figure 21) would ensure that the buffer is large enough to hold the environment variable string before copying.

The requires clause means Splint will report a warning if a call to updateEnvSafe passed in a buffer as str that is not big enough to hold the value passed as strSize characters.

In many cases, functions will have multiple unresolved constraints which are similar.  For example, if a subsequence statement writes to the next element of a buffer.  Usually all these constraints represent all real problems or are all spurious.  If the +redundantconstraints flag is set, Splint reports even apparently redundant warning messages.  Otherwise, if satisfying one unresolved constraint would imply satisfying another, Splint only prints a warning message for the stronger constraint.

The +functionpost flag is useful for determining if array bounds warnings are spurious.  If this flag is set, Splint will print the constraints that it established at the end of the function.  If the warnings are spurious, localized control comments can be used to suppress them.

Next: 10. Extensible Checking
Return to Contents