Paper Info
Title
Symbolic String Verification: An Automata-Based Approach
Abstract
We present an automata-based approach for the verification of string operations in PHP programs based on symbolic string analysis. String analysis is a static analysis technique that determines the values that a string expression can take during program execution at a given program point. This information can be used to verify that string values are sanitized properly and to detect programming errors and security vulnerabilities. In our string analysis approach, we encode the set of string values that string variables can take as automata. We implement all string functions using a symbolic automata representation (MBDD representation from the MONA automata package) and leverage efficient manipulations on MBDDs, e.g., determinization and minimization. Particularly, we propose a novel algorithm for language-based replacement. Our replacement function takes three DFAs as arguments and outputs a DFA. Finally, we apply a widening operator defined on automata to approximate fixpoint computations. If this conservative approximation does not include any badpatterns (specified as regular expressions), we conclude that the program does not contain any errors or vulnerabilities. Our experimental results demonstrate that our approach works quite well in checking the correctness of sanitization operations in real-world PHP applications.
Year
DOI
Venue
2008
10.1007/978-3-540-85114-1_21
SPIN
Keywords
Field
DocType
automata-based approach,static analysis technique,symbolic string analysis,string analysis approach,string expression,string operation,symbolic string verification,mona automata package,string variable,string analysis,string value,string function,static analysis,regular expression
String searching algorithm,Regular expression,Programming language,Computer science,Correctness,Theoretical computer science,String interpolation,scanf format string,String metric,String (computer science),String operations
Conference
Volume
ISSN
Citations 
5156
0302-9743
45
PageRank 
References 
Authors
2.00
16
4
Name
Order
Citations
PageRank
Fang Yu117510.47
Tevfik Bultan22481157.95
Marco Cova3142571.19
Oscar H. Ibarra43235741.44