Zachary Anderson, Eric Brewer, Jeremy Condit, Rob Ennals, David Gay, Matthew Harren, George Necula, and Feng Zhou
It is time for us to focus on sound analyses for our critical systems software—that is, we must focus on analyses that ensure the absence of defects of particular known types, rather than best-effort bug-finding tools. This paper presents three sample analyses for Linux that are aimed at eliminating bugs relating to type safety, deallocation, and blocking. These analyses rely on lightweight programmer annotations and run-time checks in order to make them practical and scalable. Sound analyses of this sort can check a wide variety of properties and will ultimately yield more reliable code than bug-finding alone.
|Published in||Hot Topics in Operating Systems (HotOS '07)|
All copyrights reserved by USENIX 2007