Splint provides mechanisms for defining new checks and annotations using metastate definitions. User-defined checks can be used to check and document properties not supported by the provided checks. [13]
A large class of useful checks can be described as constraints on attributes associated with program objects or the global execution state. Unlike types, however, the values of these attributes can change along an execution path. Splint provides a general language that lets users define attributes associated with different kinds of program objects as well as rules that both constrain attributes’ values at interface points and specify how attributes change.
Because user-defined attribute checking is integrated with normal checking, Splint’s analysis of user-defined attributes can take advantage of other analyses, such as alias and nullness analysis.
To define an attribute, create a metastate file (.mts) that defined the possible values and transfer rules of the attribute. Attributes can either be associated with a particular kind of program object (for example, all char *’s) or with the global state (whether or not the network has been initialized). The –mts <file> flag is used to direct Splint to read a metastate file (which will be found on the LARCH_PATH with default extension .mts).
An example attribute definition is shown in Figure 22. It defines the taintedness attribute for recording whether or not a char * came from a possibly untrustworthy source. Knowing whether a value is possibly hostile is useful for preventing several security vulnerabilities including format string bugs.[14] (A simpler way to detect format vulnerabilities is to warn for any format string that is unknown at compile time. Splint provides this checking, issuing a warning if the +formatconst flag is set and finds any unknown format strings at compile time. This can produce spurious messages, however, because there might be unknown format strings that are not vulnerable to hostile input.)
The first three lines of the attribute definition define the taintedness attribute associated with char * objects, which can be in one of two states: untainted or tainted. The context clause gives a context selector for which objects have the attribute. In this case, reference char * means that every reference that is a char * has an associated taintedness attribute. Other contexts include parameter (only parameter declarations), literal (only string or number literals), and null (only known NULL values). Attribute can also be defined that are not associated with any particular object, but instead are associated with the global state of a program execution. The global keyword is used before attribute to define a global attribute.
The oneof clause introduces two identifiers for representing the taintedness value: untainted for references that are not derived from untrustworthy input, and tainted for references that may contain hostile data.
The annotations clause defines two new annotations that may be used to describe taintedness assumptions. In this case, the annotations match the names of the value choices, but they may be any identifier. The clause tainted reference ==> tainted defines the tainted annotation that may be used on a reference to indicate that it has tainted state.
|
attribute taintedness context reference char * oneof untainted, tainted annotations tainted reference ==> tainted untainted reference ==> untainted transfers tainted as untainted ==> error "Possibly tainted storage used where untainted required." merge tainted + untainted ==> tainted defaults reference ==> tainted literal ==> untainted null ==> untainted end Figure 22. Taintedness Attribute |
The transfers clause defines rules for state changes and warning when objects are passed as parameters, returned, or assigned to externally visible references. The rule, tainted as untainted ==> error "Possibly tainted storage used where untainted required.", means it is an error to pass a tainted value as a parameter that has untainted taintedness. All other transfers are implicitly permitted, and leave the passed storage in the same state as before the transfer. We may also use a transfers clause to indicate that the reference changes state after a transfer. A losereference clause (not used in taintedness) is similar to a transfers clause, except it is used to provide rules for when a reference to storage is lost, either by leaving the scope in which it was declared, returning from a function, or assigning it to a new value.
The merge clause defined rules for combining state along paths. The clausemerge tainted + untainted ==> tainted indicates that combining tainted and untainted objects produces a tainted object. Thus, if a reference is tainted along one control path and untainted along another control path, checking assumes that it is taintedafter the two branches merge. It is also used to merge taintedness states in function specifications (see the strcat example in the next section). We can also define error combinations so that a warning is reported if the states on different paths are incompatible.
The defaults clause specifies default values used for declarators without explicit attribute annotations. We choose default values to make it easy to start checking an unannotated program. Here we assume unannotated references are tainted and Splint will report a warning where unannotated references are passed to functions that require untainted parameters. The warnings indicate either a format bug in the code or a place where an untainted annotation should be added. Running Splint again after adding the annotation will propagate the newly documented assumption through the program.
The full grammar for metastate definitions is given in Appendix C.
The annotations defined by metastate definitions can be used like normal annotations. The context specifier for an annotation indicates where it may be used. For the taintedness example, we can use tainted and untainted as annotations wherever only could be used. This includes ensures and requires clauses, which allows us to specify functions that modify state associated with metastate definitions. The syntax <expr> :<attribute> is used to refer to the value of the user-defined attribute for expression <expr>.
It is often necessary to extend the library specifications with metastate annotations. We don’t want to have different versions of the library for different metastate annotations, so instead Splint provides a mechanism for adding annotations separately using an .xh file. For the taintedness example, we do this by providing annotated declarations in the tainted.xh file. Example specifications in this file include:
int printf (/*@untainted@*/ char *fmt, ...);
char *fgets (char *s, int n, FILE *stream) /*@ensures tainted s@*/ ;
char *strcat (/*@returned@*/ char *s1, char *s2)
/*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/
The strcat specification uses /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ to indicate that the taintedness of s1 after strcat returns is the result of merging the taintedness of s1 and s2 before the call. Because the parameters lack annotations, they are implicitly tainted according to the default rules and either untainted or tainted references can be passed as parameters to strcat. The ensures clause means that after strcat returns the first parameter (and the result, because of the returned annotation on s1) will be tainted if either passed object was tainted. Splint merges the two taintedness states using the attribute definition rules—hence, if the s1 parameter is untainted and the s2 parameter is tainted, the result and first parameter will be tainted after strcat returns.
Next: 11. Macros
Return to Contents