Testing Program for Security using Symbolic Execution and Exception Injection

Symbolic execution is one of the most popular automated testing techniques for program verification and test case generation. It assures exhaustive path  coverage by generating and resolving path constraints on each branch, effectively covering untested paths or gray areas that often lead to security vulnerabilities. Thus, symbolic execution is recognized as one of the most effective techniques for uncovering code vulnerabilities. Here, we consider special case of security vulnerabilities, which are raised due to improper error handling, such as resource leakage, program crash and program inconsistency. Finding these vulnerabilities during application development will check misuse of applications and hence will add more quality to the application. In this paper, authors propose a framework Symexc that tests and verifies if such vulnerabilities exist in the program using symbolic execution and exception injection. Further, the paper demonstrates the implementation of the framework, followed by its validation on some java programs.