Date Added: Aug 2009
Verification of string manipulation operations is a crucial problem in computer security. The authors present a new symbolic string verification technique that can be used to prove that vulnerabilities that result from improper string manipulation do not exist in a given program. They formally characterize the string verification problem as the reachability analysis of string systems, programs that contain only string variables and allow a limited set of operations on them. They show that string analysis problem is undecidable with even three variables if branch conditions that compare different variables are allowed. They develop a sound symbolic analysis technique for string verification that over-approximates the reachable states of the string system.