[splint.git] / BUFFERCHECKING

			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.
Commit	Line	Data
15b3d2b2	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