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.