Modular checking for buffer overflows in the large

Abstract

We describe an ongoing project, the deployment of a modular checker to statically find and prevent every buffer overflow in future versions of a Microsoft product. Lightweight annotations specify requirements for safely using each buffer, and functions are checked individually to ensure they obey these requirements and do not overflow. Our focus is on the incremental deployment of this technology: by layering the annotation language, using aggressive inference techniques, and slicing warnings by checker confidence, teams must pay only part of the cost of annotating a program to achieve part of the benefit, which provides incentive for further annotation. To date over 400,000 annotations have been added to specify buffer usage in the source code for this product, of which over 150,000 were automatically inferred, and over 3,000 potential buffer overflows have been found and fixed.