In this paper we have discussed the application of the Simplex method in checking software safety - the application in automated detection of buffer overflows in C programs. This problem is important because buffer overflows are suitable targets for hackers' security attacks and sources of serious program misbehavior. | Yugoslav Journal of Operations Research Vol 19 (2009), Number 1, 133-148 DOI: USING SIMPLEX METHOD IN VERIFYING SOFTWARE SAFETY 1 Milena VUJOŠEVIĆ-JANIČIĆ milena@ Filip MARIĆ filip@ Dušan TOŠIĆ dtosic@ Faculty of Mathematics, University of Belgrade, Received: December 2007 / Accepted: June 2009 Abstract: In this paper we have discussed the application of the Simplex method in checking software safety - the application in automated detection of buffer overflows in C programs. This problem is important because buffer overflows are suitable targets for hackers' security attacks and sources of serious program misbehavior. We have also described our implementation, including a system for generating software correctness conditions and a Simplex based theorem prover that resolves these conditions. Keywords: Simplex method, software safety, buffer overflows. 1. INTRODUCTION The Simplex method is considered to be one of the most significant algorithms of the last century 2 . It is a method for solving the linear optimization problem [4] and its worst case complexity is exponential in the number of variables [11]. However, it is very efficient in practice and converges in polynomial time for many input problems, 1 This work was partially supported by Serbian Ministry of Science grant 144030. 2 For instance, the journal Computing in Science and Engineering listed it as one of the top 10 algorithms of the century. 134 M. Vujošević-Janičić, F. Marić, D. Tošić / Using Simplex Method in Verifying including certain classes of randomly generated problems ([17], [9]). Apart from the basic Simplex method for the optimization problem, there are many other variants, including the decision variant that decides if a set of linear constraints is satisfiable or not. The Simplex method has a wide range of applications, in different sorts of optimization problems, but also in software and hardware verification. In this .
