This paper shows how system-speci c static analysis can nd security errors that violate rules such as \integers from untrusted sources must be sanitized before use" and \do not dereference user-supplied pointers." In our approach, programmers write system-speci c extensions that are linked into the compiler and check their code for errors. We demonstrate the approach's e ectiveness by using it to nd over 100 security errors in Linux and OpenBSD, over 50 of which have led to kernel patches. An unusual feature of our approach is the use of methods to automatically detect when we miss code actions that should be checked.
Ken Ashcraft, Dawson R. Engler