| 摘要 |
The cross-site scripting detection method (2700) inputs a web page application program into a virtual machine. Output of the virtual machine produces bytecode and a control flow graph. A state transition graph encoder uses the bytecode and control flow graph to produce transition, initial, and property (Τ,Ι,Ρ) state information. The Τ,Ι,Ρ state information is then parsed by a parser. Output of the parser is fed to a reachability verifier that produces a verified flag (OK) or alternatively a positive counter-example (CEX). The CEX is transformed into the web page application program and fed as HTML to a browser which checks for feasibility of a XSS find. A feasibility indication suggests a true positive find of the XSS malicious code. An infeasibility indication suggests a false positive find upon which, via feedback of the infeasibility indication, the reachability verifier is retuned to refine the solution. |
