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 classes of vulnerabilities is pointer taintedness. A pointer is said to be tainted if a user input can directly or indirectly be used as a pointer 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 library functions 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 classes 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.
This work is supported in part by a grant from Motorola Inc. as part of Motorola Center for Communications, in part by MURI Grant N00014–01–1–0576, and in part by NSF CCR 00–86096ITR.
Chapter PDF
References
D. Evans and D. Larochelle. Improving Security Using Extensible Lightweight Static Analysis. In IEEE Software, Jan/Feb 2002
B. Chess. Improving Computer Security Using Extended Static Checking. IEEE Symposium on Security and Privacy 2002
J. A. Goguen and G. Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, 1996, ISBN 0–262-07172-X
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer and C. Talcott The Maude 2.0 System. In Proc. Rewriting Techniques and Applications, 2003, 2003.
J. Xu, Z. Kalbarczyk and R. K. Iyer. Transparent Runtime Randomization for Security. To appear in Proc. Symposium on Reliable and Distributed Systems, 2003.
D. Wagner, J. Foster, E. Brewer, and A. Aiken. A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. Network and Distributed System Security Symposium (NDSS 2000).
U. Shankar, K. Talwar, J. Foster, and D. Wagner. Detecting Format String Vulnerabilities With Type Qualifiers. 10th USENIX Security Symposium, 2001.
C. Cowan, C. Pu, D. Maier, et al. Automatic Detection and Prevention of Buffer-Overflow Attacks. 7th USENIX Security Symposium, San Antonio, TX, January 1998.
A. Baratloo, T. Tsai, N. Singh, Transparent Run-Time Defense Against Stack Smashing Attacks, Proc. USENIX Annual Technical Conference, June 2000.
S. Chen, Z. Kalbarczyk, J. Xu, R. K. Iyer. “A Data-Driven Finite State Machine Model for Analyzing Security Vulnerabilities”. in IEEE International Conf. on Dependable Systems and Networks, 2003.
Introduction to equational logic. http://www.cs.cornell.edu/Info/People/gries/Logic/Equational.html
S. Chen, K. Pattabiraman, Z. Kalbarczyk, R. K. Iyer. Formal Reasoning of Various Categories of Widely Exploited Security Vulnerabilities By Pointer Taintedness Semantics (Full Version). http://www.crhc.uiuc.edu/~shuochen/pointer_taintedness
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
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: Deswarte, Y., Cuppens, F., Jajodia, S., Wang, L. (eds) Security and Protection in Information Processing Systems. SEC 2004. IFIP — The International Federation for Information Processing, vol 147. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8143-X_6
Download citation
DOI: https://doi.org/10.1007/1-4020-8143-X_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-8016-1
Online ISBN: 978-1-4020-8143-9
eBook Packages: Springer Book Archive