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

11Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Chen, S., Pattabiraman, K., Kalbarczyk, Z., & Iyer, R. K. (2004). Formal reasoning of various categories of widely exploited security vulnerabilities using pointer taintedness semantics. In IFIP Advances in Information and Communication Technology (Vol. 147, pp. 83–99). Springer New York LLC. https://doi.org/10.1007/1-4020-8143-x_6

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free