SymWalker: Symbolic Execution in Routines of Binary Code

Detecting vulnerabilities in binary codes is one of the most difficult problems due to the lack of type information and symbols. We propose a novel tool to perform symbolic execution inside the routines of binary codes, providing easy static analysis for vulnerability detection. Compared with existing systems, our tool has four properties: first, it could work on binary codes without source codes; second, it employs the VEX language for program analysis, thus having no side effects; third, it could deliver high coverage by statically executing on control flow graphs of disassembly codes; fourth, two security property rules are summarized to detect the corresponding vulnerabilities, based on which a convenient interface is provided for developers to detecting vulnerabilities, such as buffer overflow, improper memory access, and etc. Experimental results on real software binary files show that our tool could efficiently detect different types of vulnerabilities.