TY - GEN
T1 - Formal reasoning of various categories of widely exploited security vulnerabilities using pointer taintedness semantics
AU - Chen, Shuo
AU - Pattabiraman, Karthik
AU - Kalbarczyk, Zbigniew
AU - Iyer, Ravi K.
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
KW - Equational logic
KW - Pointer taintedness
KW - Program semanties
KW - Security vulnerability
KW - Static analysis
UR - http://www.scopus.com/inward/record.url?scp=84902507067&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84902507067&partnerID=8YFLogxK
U2 - 10.1007/1-4020-8143-x_6
DO - 10.1007/1-4020-8143-x_6
M3 - Conference contribution
AN - SCOPUS:84902507067
SN - 9781475780161
T3 - IFIP Advances in Information and Communication Technology
SP - 83
EP - 99
BT - Security and Protection in Information Processing systems - IFIP 18th World Computer Congress, TC11 19th International Information Security Conference, SEC 2004
PB - Springer
T2 - IFIP TC11 19th International Information Security Conference, SEC 2004
Y2 - 22 August 2004 through 27 August 2004
ER -