关键词: 循环安全, 静态分析, 符号执行, 路径搜索, 归纳函数

Abstract: Loop is a common structure in programs and improperly using loop is one of the most important reasons resulting in security problems, making detecting loop security problem is important and valuable. As the path state explosion and loop modeling problems in binary code, statically analyzing of loop security is extremely challenging, and traditional methods are unable to solve these problem. In this paper, we proposed a detecting method for loop security problems based on binary static analyzing，having the ability of detecting out of bound memory access in loop and infinite loop problem. Firstly, we present an accurate extracting and recovering method of loop factors in binary based on analyzing of loop structure and then multiple path explore strategies are utilized to solving the path state explosion and sorting problem. Moreover, we propose a function summary method based on static concrete execution to solving constraints growing problem caused by induction function invoking in loops. Finally, we proposed an inductive analysis method based on loop predicates to detect insecure loop in binary. We have applied our methods on ten real world programs and compared with Angr. The experimental results turn out that our method is capable of detecting more loop problems than Angr.

Key words: loop security, static analysis, symbolic execution, path searching, induction function