Detecting buffer overflows for C like programs using CLP

Surinder Jain
University of Sydney

Buffer overflows caused by array out of bound accesses are a major
security vulnerability in system software written in C/C++. We
describe a technique that employs constraint logic programming to find
bugs such as buffer overflows in C-like programs represented as
control flow graphs. The technique is complete over finite variable
domains as it is does not have false-negatives, and does not produce
false positives.

For an array access, we instrument the program by introducing a new
boolean variable whose truth value indicates whether a buffer overflow
occurs. After instrumenting the program, we slice the program for this
newly introduced variable, translate the slice to a non-deterministic
language (NDL) program, translate the non-deterministic program to a
constraint logic program (CLP), and solve the constraint logic
program. Solution to the constraint logic program using a solver
proves the existence of a buffer overflow.

In this talk we sketch some of the proofs to show that the
translations from imperative program to NDL and then NDL to CLP are
semantically correct which is the major theoretical contribution of
this work.