In modern websites, stored Cross-Site Scripting (XSS) is the most dangerous XSS vulnerability, which can store payloads in the web system and be triggered directly by the victim. Database (DB) as the most commonly used storage medium for data on websites is therefore also the most common place where stored XSS occurs. Due to the modularity of modern programming architectures, the complex underlying database operations will often be encapsulated and abstracted as a Data Access Layer (DAL) to provide unified data access services to the business layer. The heavy use of Object-Oriented (OO) and dynamic language features involved in the encapsulation makes it increasingly challenging for static taint analysis tools to understand how tainted data flows between the source code and the exact locations in database.

A large number of PHP applications suffer from Cross-Site Scripting (XSS) attacks every year. Static taint analysis is a prevalent way to detect taint-style vulnerabilities like XSS. However, the precision of current tools suffers severely due to dynamic features of PHP programs and the incomplete recognition of user-defined sanitizers, which lead to false negatives and a large number of false positives. In this paper, we present PAT, a PHP static Analysis Tool for effective XSS vulnerability detection. A new concept of “inner” source and sink is introduced for the first time to shorten the taint paths needed to be traced statically, which therefore mitigates the broken path problem induced by dynamic language features to a certain extent. A sanitizer-centric approach is proposed to automatically identify them. Moreover, PAT leverages both data flow analysis and NLP technique to accurately identify user-defined sanitizers with a precision 82.8%. Lastly, PAT performs a classical taint analysis with the enhanced taint specifications (i.e., sources, sinks and sanitizers). Evaluations on 5 large, real-world PHP web applications and 5 popular WordPress plugins show that PAT performs better in XSS detection compared with 3 existing tools. Besides, 8 zero-day bugs are detected and confirmed by the developers.

Mining from simulation data has been introduced as an effective solution to assertion generation for the design under verification (DUV) in prior work. As the simulation data is inherently incomplete, the quality of mined assertions is to be measured. In this paper, we propose a Belief-failRate framework to evaluate the success possibility of mined assertions, by taking both occurrences of free variable assignments and conflicts of absent scenarios into consideration. Meanwhile, a success possibility guided assertion constraining method is given to improve the quality of generated assertions. Experimental results show that assertions with high ranking using the proposed Belief-failRate framework are likely to have high possibility to be true assertions. Furthermore, guided by the success possibility, the proposed assertion constraining procedure can find assertions that cover new design functionality.

Property coverage is an important way to evaluate the completeness of model checking. Most of the property coverage metrics are based on mutation coverage, obtained by mutating the design and checking the property's ability to detect the mutation. Due to the complexity of computing mutation coverage in model checking, the previous methods resort to some approximate algorithms which tend to give pessimistic estimation of state coverage, and can only deal with a limited subset of Computation Tree Logic (CTL). In this paper, we present an improved algorithm to compute mutation coverage for arbitrary CTL formulas with high accuracy. Experimental results show that the proposed algorithm can identify a great number of covered states missed by a previous method. Meanwhile, the extension to the complete CTL set makes it easy to write all kinds of properties to describe the features of the design better.