			Buffer Overflow Checking
			    David Larochelle
			     15 August 2001


This is a preliminary guide to the buffer overflow checking in LCLint
Version 3.0.  This alpha version contains additional checking not
documented in the manual for LCLint 2.5.

Although this document provides a quick introduction for the new
features of LCLint it is not intended as a substitute for the LCLint
manual.  We recommend that users unfamiliar with LCLint consult the
LCLint user guides in addition to this document.

The types of errors which LCLint reports can be controlled flags.
Theses flags can be set on the commands line or in .lclintrc files.  A
flags by giving LCLint the +flagname option on the command line or in a
.lclintrc file where flagname is the name of the flag.  Similarly flags
are unset with -flagname.

Overview
========

LCLint detects buffer overflow errors by generating precondition and
postcondition constraints at the expression level.  We resolve
constraints using post conditions from previous statements.  We generate
an error message for any constraints which we are unable to resolve at
the top of a function.

All checking takes place within functions.  Interprocedural properties
are checked using annotations.  Annotated versions of the standard
libraries are provided innerally.

The new annotations allow programmers to explicitly state function
preconditions and postconditions using requires and ensures clauses.  We
can use these clauses to describe assumptions about buffers that are
passed to functions and constrain the state of buffers when functions
return.  For the analyses described here two kinds of assumptions and
constraints are used: maxSet, and maxRead.

When used in a requires clause, the maxSet annotation describes
assumptions about the lowest and highest indices of a buffer that may be
safely used as an lvalue (e.g., on the left-hand side of an assignment).
For example, consider a function with an array parameter a and an
integer parameter i that has a precondition requires maxSet(a) >= i.
The analysis assumes that at the beginning of the function body, a[i]
may be used as an lvalue.  If a[i+1] were used before any modifications
to the value of a or i, LCLint would generate a warning since the
function preconditions are not sufficient to guarantee that a[i+1] can
be used safely as an lvalue.  Arrays in C start with index 0, so the
declaration char buf[MAXSIZE] generates the constraints maxSet(buf) =
MAXSIZE - 1 and minSet(buf) = 0.  Similarly, the maxRead constraint
indicates the maximum indices of a buffer that may be read safely.  The
value of maxRead for a given buffer is always less than or equal to the
value of maxSet.  In cases where there are elements of the buffer have
not yet been initialized, the value of maxRead may be lower than the
value of maxSet.

Checking is controlled by the following flags.  If the arraybounds flag
is set LCLint will report potential array bounds.  THIS FLAG MUST BE SET
IN ORDER FOR BUFFER OVERFLOW ERRORS TO BE REPORTED.  There are a number
of additional options which can be used to fine tune checking.

If the +arrayboundsread is set LCLint will report cases in which an
index past the end of an array or buffer is read.  The default is to
only report cases in which data is written.  Out of bounds reads are
less dangerous than out of bounds writes but are still security
problems.

The following are used to fine tune the checking.  If the
constraintlocation flag is set LCLint will include the expression which
causes LCLint to generate the unresolved constraint in an error message.
We recommend this options.  The orconstraint is used to perform slightly
more accurate checking by using disjuction internally.  The performance
cost is minimal so we recommend this option.

Handling spurious messages
==========================

LCLint will occasionally report spurious error messages.  If you see an
error message that you believe to be incorrect first see if you can
correct the problem by adding additional precondition annotations.  For
function with no preconditions LCLint assumes that the function is safe
under all conditions.  Also consider rewriting the code.  Code that is
hard for LCLint to understand is often hard was humans to understand as
well.  You may want to improve the readability and clarity is the code.

If you are sure that the message is spurious you can suppress the
message.  Adding the /*@i@*/ annotation to a line causes LCLint to
suppers all errors generated by the line.  Flags can also be set and
unset within a program.  /*@-flagname@*/ sets a flag to
false. /*@+flagname@*/ sets a flag to true and /*@=flagname@*/ returns a
flag to its previous state.

For example /*@-arroundboundsread@*/ str2[i] = str[i];
/*@=arroundboundsread@*/ would suppress error involving out of bounds
reads for the code fragment.

Frequently Asked Questions
==========================

I have a function with many buffer overflows but LCLint only reports one
error?

LCLint tries to avoid printing redundant error messages.  We don't print
two constraints if satifying one constraint would satisify another.

LCLint crashes or complains about a bug?

Please report the problem to lclint-bug@cs.virginia.edu

Where can I find more information about LCLint?

The LCLint web site http://lclint.cs.virginia.edu contains a lot of
useful documentation, including a paper describing the LCLint extensions
for buffer overflow checking.  The lclint web site also contains
information on lclint mailing lists.






