Abstract

Dynamic code analysis attempts to find errors or vulnerabilities while a program is executing on a real or virtual processor. The objective of dynamic analysis is to reduce debugging time by automatically pinpointing and informing on errors as they occur. The use of dynamic analysis tools can reduce the need for the developer to recreate the precise conditions under which an error, a vulnerability or a security flow occurs. This paper presents a formal approach to detect software vulnerabilities in C programs relying on formal models of vulnerabilities causes called “Vulnerability Detection Conditions” (VDCs). These models provide a formal interpretation of a vulnerability to facilitate its automatic detection using dynamic code analysis tool. To illustrate our approach, a prototype tool TestInv-Code has been developed. It allows to detect the presence of vulnerabilities by checking the VDCs on the execution trace of the studied C program. By traces we mean here the disassembled instructions that are being executed. The tool has been applied on an open source application XINE that contains a known vulnerability to demonstrate its effectiveness.