Automata-based symbolic string analysis for vulnerability detection

详细信息    查看全文

• 作者：Fang Yu (1)
  Muath Alkhalaf (2)
  Tevfik Bultan (2)
  Oscar H. Ibarra (2)
  
• 关键词：String analysis ; Automated verification ; Web application security ; Vulnerability analysis
• 刊名：Formal Methods in System Design
• 出版年：2014
• 出版时间：February 2014
• 年：2014
• 卷：44
• 期：1
• 页码：44-70
• 全文大小：972 KB
• 作者单位：Fang Yu (1)
  Muath Alkhalaf (2)
  Tevfik Bultan (2)
  Oscar H. Ibarra (2)
  
  1. Department of Management Information Systems, National Chengchi University, Taipei, Taiwan
  2. Department of Computer Science, University of California Santa Barbara, Santa Barbara, USA
  
• ISSN：1572-8102

文摘

Verifying string manipulating programs is a crucial problem in computer security. String operations are used extensively within web applications to manipulate user input, and their erroneous use is the most common cause of security vulnerabilities in web applications. We present an automata-based approach for symbolic analysis of string manipulating programs. We use deterministic finite automata (DFAs) to represent possible values of string variables. Using forward reachability analysis we compute an over-approximation of all possible values that string variables can take at each program point. Intersecting these with a given attack pattern yields the potential attack strings if the program is vulnerable. Based on the presented techniques, we have implemented Stranger, an automata-based string analysis tool for detecting string-related security vulnerabilities in PHP applications. We evaluated Stranger on several open-source Web applications including one with 350,000+ lines of code. Stranger is able to detect known/unknown vulnerabilities, and, after inserting proper sanitization routines, prove the absence of vulnerabilities with respect to given attack patterns.