Abstract Parsing: Static analysis of dynamically generated string output

该项目提供了一种自动化的、基于形式化方法的方法和工具，可以在执行之前分析和验证动态生成html、XML和SQL文档的PHP、Perl或Javascript程序。这种文档生成器程序在万维网上很常见，并且以生成结构不良、有缺陷和危险的文档而臭名昭著，这些文档会导致随后的服务器错误或安全漏洞。该方法集成了mlr (k)解析、数据流分析和程序安全等技术来综合程序分析。给定生成文档的程序（例如，PHP脚本）和文档语言的上下文无关的引用语法(例如：（用于HTML的语法），分析工具为参考语法生成一个LR(k)解析器，并应用数据流分析来分析程序并预测程序生成的文档的上下文无关语法结构。该工具计算抽象解析堆栈，这是一种新颖的创新结构，用于编码生成的文档的上下文无关结构。接下来，该工具应用形式语义技术从抽象解析堆栈中计算其上下文敏感的语义，即动态生成文档的含义。动态生成的文档通常与用户提供的输入组合在一起，这些输入可能是错误的或恶意的。分析对抽象解析堆栈进行注释，以确定用户输入可能出现的位置，语义分析跟踪用户输入对文档含义的影响。

This project provides an automated, formal-methods-based methodology and toolthat analyzes and validates, in advance of its execution,PHP, Perl, or Javascript programs that dynamically generateHMTL, XML, and SQL documents.Such document-generator programs are common to the World Wide Web and arenotorious for generating ill-structured, faulty, and dangerousdocuments that cause subsequent server errors or security breaches.The methodology integrates techniques fromLR(k)-parsing, data-flow analysis, and program securityto synthesize the program-analysis.Given the program (e.g., a PHP script) that generates documents and given thecontext-free reference grammar for the document language(e.g., a grammar for HTML),the analysis tool generates an LR(k) parser for the reference grammarand applies a data-flow analysis to analyze the program andpredict the context-free grammatical structure of thedocuments to be generated by the program.The tool computes abstract parse stacks, a novel and innovative structurethat encodes a generated document's context-free structure.Next, the tool applies formal semantics techniques to compute froman abstract parse stack its context-sensitive semantics, that is, themeaning of the dynamically generated document.Dynamically generated documents are often assembledwith user-supplied input, which can be erroneous or malicious.The analysis annotates the abstract parse stacks to identitywhere user input might appear,and the semantic analysis tracks the influenceof the user input upon the document's meaning.