Formal reasoning of various categories of widely exploited security vulnerabilities using pointer taintedness semantics

Abstract

This paper is motivated by a low level analysis of various categories of severe security vulnerabilities, which indicates that a common characteristic of many c1asses of vulnerabilities is pointer taintedness. Apointer is said to be tainted if a user input can directly or indirectly be used as apointer value. In order to reason about pointer taintedness, a memory model is needed. The main contribution of this paper is the formal definition of a memory model using equational logic, which is used to reason about pointer taintedness. The reasoning is applied to several Iibrary fimctions to extract security preconditions, which must be satisfied to eliminate the possibility of pointer taintedness. The results show that pointer taintedness analysis can expose different c1asses of security vulnerabilities, such as format string, heap corruption and buffer overflow vulnerabilities, leading us to believe that pointer taintedness provides a unifying perspective for reasoning about security vulnerabilities. © 2004 by Springer Science+Business Media Dordrecht.