Next: Run-time Techniques.
Up: 6 Related Work
Previous: Type Qualifiers.
Many authors have noted that static analysis can be a useful tool for
detecting bugs. For instance, LCLint  uses dataflow
analysis to search for common errors in C programs; Engler et al.'s
Meta-level Compilation  statically simulates the
behavior of a user-defined finite state machine and has been
successful at finding many new bugs; and the Extended Static Checking
system (ESC)  uses theorem proving to verify the validity of
annotated Java source code.
These systems have been very successful at detecting many common bugs.
However, they are not well suited to detecting format string vulnerabilities,
for two reasons. First, they focus primarily on local properties,
string vulnerabilities often arise due to global mishandling of strings.
Second, many of them (e.g., ESC and, to a lesser degree, LCLint)
require extensive annotations from the user, which we would like to avoid.
Our type-based techniques address these challenges directly.