Towards a Hybrid Framework for Detecting Input Manipulation Vulnerabilities

Input manipulation vulnerabilities such as SQL Injection, Cross-site scripting, Buffer Overflow vulnerabilities are highly prevalent and pose critical security risks. As a result, many methods have been proposed to apply static analysis, dynamic analysis or a combination of them, to detect such security vulnerabilities. Most of the existing methods classify vulnerabilities into safe and unsafe. They have both false-positive and false-negative cases. In general, security vulnerability can be classified into three cases: (1) provable safe, (2) provable unsafe, (3) unsure. In this paper, we propose a hybrid framework-Detecting Input Manipulation Vulnerabilities (DIMV), to verify the adequacy of security vulnerability defenses for input manipulation vulnerabilities by integrating formal verification with vulnerability prediction in a seamless way. The verification part takes into account sink predicates and effect of domain and custom specifications for detecting input manipulation vulnerabilities. Proving from specification is used as far as possible. Cases that cannot be proved are then predicted from the signatures mined. Our evaluation shows the practicality of the proposed framework.