Detecting vulnerabilities in C programs using trace-based testing

Security testing has gained significant attention recently due to frequent attacks against software systems. This paper presents a trace-based security testing approach. It reuses test cases generated from previous testing methods to produce execution traces. An execution trace is a sequence of program statements exercised by a test case. Each trace is symbolically executed to produce program constraints and security constraints. A program constraint is a constraint imposed by program logic on program variables. A security constraint is a condition on program variables that must be satisfied to ensure system security. A security flaw exists if there is an assignment of values to program variables that satisfies the program constraint but violates the security constraint. This approach detects security flaws even if existing test cases do not trigger them. The novelty of this method is a test model that unifies program constraints and security constraints such that formal reasoning can be applied to detect vulnerabilities. A tool named SecTAC is implemented and applied to 14 benchmark programs and 3 open-source programs. The experiment shows that SecTAC quickly detects all reported vulnerabilities and 13 new ones that have not been detected before.