a method for searching of c++ string accesses with an incorrect index

Since C++ is a commonly used programming language that is also in wide use for programming the mobile OS such as Tizen the static analysis of C++ programs is in high demand. The article is devoted to searching the accesses to C++ strings with an incorrect index. As opposed to the buffer overflows in C, this kind of defect in rarely detected by industrial static analyzers due to complexity of its modeling. In the work, we formalize the criteria of this defect and propose the formal modeling rules of C++ string-related methods and a number of STL functions. These rules allow modeling of string length and access index. The rules for summary-based inter-procedural analysis are introduced as well. The article simulates only the length of a string to provide a compromise between the search precision and the volume of data processing. A checker based on these modeling rules is implemented for the Clang Static Analyzer - a symbolic execution static analyzer for C++ code. This checker was tested on the C++ code of Android OS and OS Tizen user-mode packages (totally about 20 million strings of code). The results of an eye-inspection of warnings produced by this checker prove its precision, which is appropriate for industrial static analyzer: nearly 70.