[splint.git] / readmeSecurityChecking.txt

Security Checking readme. 

This document is meant to describe some of the new options in LCLint which enable security checking.  This alpha version contains additional checking not documented in the manual for LCLint 2.5.0

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.

Buffer Overflows

This section describes options which allow LCLint to detect potential array bounds error.

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