Memory violation detection method in binary code

In this paper memory violation detection method is considered. This method is applied to program binaries without requiring debug information. It allows to find such memory violations as out-of-bound read or write. The technique is based on dynamic analysis and symbolic execution. Instead of representing input buffer as a symbolic variable of fixed size, we track only the prefix of buffer symbolically and a special symbolic variable that represents the length of input buffer. The symbolic length variable allows to interpret functions with known semantics such as string library or memory allocation functions. While interpreting these functions using symbolic length variables we assert some constraints on buffer bounds. Such constraints allow to find memory violations. If violation is located, concrete values of buffer prefix and final input buffer length are provided. To apply this method to binary code we have to recover buffer bounds. So we developed some methods that recover buffer bounds in heap and stack memory. We present a tool implementing the method. We used this tool to find 11 bugs in both Linux and Windows programs, 7 of which were undocumented at the time this paper was written. This tool was able to detect known Heartbleed vulnerability which couldn't be found by simple fuzzers in crash absence.