Beyond Bug-Finding: Sound Program Analysis for Linux

Zachary Anderson, Eric Brewer, Jeremy Condit, Rob Ennals, David Gay, Matthew Harren, George Necula, and Feng Zhou

Abstract

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.

Details

Publication typeInproceedings
Published inHot Topics in Operating Systems (HotOS '07)
PublisherUSENIX
> Publications > Beyond Bug-Finding: Sound Program Analysis for Linux