Developing a large software system is a rather difficult task. One of the many problems that can occur is represented by the presence of security vulnerabilities. A security vulnerability is a software bug that can be exploited by a malicious user through the supplied input, in order to gain control over the system on which the software runs.
These kinds of vulnerabilities can produce a lot of damage including losing confidential data and great amounts of money. A simple security vulnerability is represented by the buffer overflow which could allow the attacker to remotely execute code on the machine running the software.
There are many famous examples of exploits (programs that exploit the security vulnerabilities) like the Microsoft JPEG GDI+ vulnerability, the Microsoft SQL Slammer Worm that have caused a lot of damage to the attacked applications.
To prevent these situations, software verification tools perform checks both statically and dynamically in order to find the security vulnerabilities. Usually performing this checks is very time consuming and because security vulnerabilities are the user in- put dependent bugs, an approach to minimize the cost of software verification is using taint analysis to determine the points in the analyzed programs that can be influenced by user input.
In this paper we introduce a static analysis technique for performing taint analysis . This analysis is used to determine the parts of the program dependent on user input and can be used as a starting point in any bug finding tool.
We provide a theoretical basis for our analysis, by building a taint analysis type system and proving that it is sound, and is also a tool that implements the theoretical notions as a plug-in for the Frama-C platform. The paper will also show how to use the results of the taint analysis in order to perform automatic test generation for the analyzed programs.
To read this external content in full download the complete paper from the author on line at the Google code archives.