Abstract: Buffer overflow has become one of the major sources of program flaws. All of the existing solutions for detec- ting buffer overflow have serious drawbacks that hinder their wider adoption by practitioners. In this paper, we re- searched those solutions,analyzed their advantages and disadvantages. We presented a model for buffers in the program related operations. At last we designed a buffer overflow detecting approach based on model checking. A prototype was also developed to verify this method.

Key words: Buffer overflow, Model checking, Artificial analysis