]>
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 |