英语原文共 17 页，剩余内容已隐藏，支付完成后下载完整资料
Java Servlet和JSP的静态分析（节选）
克里斯蒂安·柯克高（Christian Kirkegaard）和安德斯·莫勒（AndersMoslash;ller）
丹麦奥尔胡斯大学金砖四国{ck, amoeller}@brics.dk
摘要: 我们提出了一种静态推理方法，用于对使用Java Servlet和JSP开发的Web应用程序的行为进行推理。 具体来说，我们要解决以下问题：确保所有输出都是格式正确的有效XML，并确保XHTML表单字段和会话状态的一致性。 我们的方法基于在JWIG和Xact项目中较早开发的程序分析技术的集合，并结合了平衡的上下文无关语法的工作。 总之，这为有关输出流的推理和应用程序控制流提供了必要的基础。
- 介绍
Java Servlets [15]和JSP（JavaServer Pages）[16]构成了Web应用程序开发中广泛使用的平台。 使用这些技术或相关技术开发的应用程序通常被构造为程序片段（servlet或JSP页面）的集合，这些片段接收用户输入，产生HTML或XML输出并与数据库进行交互。 这些片段通过生成页面中的表单和链接进行连接，使用部署描述符将URL声明性地映射到程序片段。 这种构造应用程序的方式给程序员带来了许多挑战。 特别是，在编译时必须确保以下理想的特性：
–所有输出应采用格式正确且有效的XML（例如，根据XHTML 1.0的架构）；
–由一个生成XHTML页面的程序片段产生的形式和字段应始终与负责接收用户输入的另一个程序片段所期望的形式和字段相匹配和一个程序片段期望存在的–session属性应该始终在会话中预先设置。
我们的目标是开发一种程序分析系统，该程序可以自动检查给定Web应用程序的这些属性。
下一页显示的小示例程序说明了可能出现的许多挑战中的一些。
该程序包含两个servlet：一个名为Entry的条目，它会生成一个带有用户在其中输入名称的表单的XHTML页面，一个名为Show的表达式，它会根据来自外部数据库的信息接收用户输入并作为另一个XHTML页面生成答复。
– 为了使程序按预期工作，程序员必须考虑许多方面，即使对于如此小的程序，也要考虑以下问题：
– printHeader产生的所有打开的开始标记是否与printFooter产生的结束标记匹配？
– getAttribute（“ timestamp”）是否总是返回合法的字符串作为XML字符数据吗？ （例如，“ lt;”不应出现在此处）
– Enter生成的表单操作URL实际上是否指向Show servlet？ （这取决于操作和方法属性的值以及部署描述符映射）
–执行Show servlet时是否始终存在参数NAME？ （检查此项需要了解导致该servlet的XHTML页面中表单字段的存在）
–显示时，属性时间戳是否始终显示在会话状态中servlet执行了吗？ （否则，将出现空引用）
为了静态地回答这样的问题，必须清楚地了解哪些字符串片段被打印到输出流以及如何在应用程序中连接servlet。 目前，程序员为了获得对程序正确性的确信而求助于非正式推理和不完整的测试。
我们的贡献如下：
-
- 我们展示了如何获取上下文无关的语法，该语法使用Java字符串分析的一种变体保守地近似servlet / JSP应用程序的可能输出[6]。
- 在字符串分析的基础上，我们使用Knuth [12]的平衡语法理论以及Mohri和Nederhof [14]的语法逼近理论来检查输出是否始终是格式正确的XML。
- 在格式检查的基础上，我们展示了如何将平衡的上下文无关文法转换为XML图，然后使用现有算法相对于XML模式对其进行验证[8]。
- 通过分析XML图中出现的表单和链接元素以及应用程序的部署描述符，我们解释了如何获取应用程序的servlet间控制流图。
- 基于对控制流的了解，我们给出派生分析的示例，以检查表格字段和会话状态是否一致使用。
- 相关工作。我们没有意识到先前尝试静态分析上述Java Servlet和JSP应用程序方面的尝试。最紧密相关的工作是Minamide [13]的工作，他将字符串分析与PHP的HTML验证相结合。在[13]中，[6]中的技术的一种变体用于从PHP程序中生成上下文无关的语法。 HTML验证通过提取和检查样本文档或通过考虑执行
- 仅深度有限的文档，这既不会导致声音也不完整的分析结果。
- XML数据与上下文无关的语法之间还有其他有趣的联系，特别是Berstel和Boasson [3]和Bruggmannmann-Klein和Wood [4]的著作。论文[3]使用Knuth的结果检查了给定上下文无关语法的XML格式正确性的某些方面，但是并没有采取完整的步骤来验证有效性。论文[4]仅考虑了与格式正确的XML文档相对应的语法，而我们的方案涉及任意上下文无关的语法，需要检查它们的格式正确性和有效性。
- servlet间的控制流分析与Web服务的工作流和业务协议密切相关。在工作流语言和Web服务组合语言的设计中投入了大量精力，用于在Web应用程序开发的设计阶段对属性进行建模和分析（例如WS-BPEL [2]和YAWL [18]）。我们的工作在某种意义上补充了这一点，即我们当前的分析能够逆向现有Web应用程序的源代码中的工作流（尽管这不是本文的重点）。这与过程挖掘[7]有关，但是使用源代码而不是系统日志，从而获得保守的结果。
- 如前所述，我们的技术基于我们先前在JWIG和Xact上的工作。 JWIG [5]是用于Web应用程序开发的基于Java的框架，其中会话控制流是显式的，而XHTML页面则以结构化的方式构建，从而可以对有效性和表格一致性进行静态分析。 Xact [10]是用于表达XML转换的一种相关语言。 XML的概念
- 对我们的分析系统至关重要的图形来自这些项目
- （由于历史原因，它们也被称为摘要图）– XML图是一组潜在的无限XML结构的表示
- 可能会出现在正在运行的JWIG或Xact程序中。论文[8]描述了一种相对于以XML模式编写的模式验证XML图的算法。
概述。在第2节中，我们首先描述如何分析输出流并产生与上下文无关的语法，该语法近似于给定Web应用程序的可能输出。第3节介绍格式正确性检查和平衡语法的构造。然后在第4节中，我们将展示如何将平衡语法转换为XML图并检查相对于XML模式的有效性。
第5节描述了基于XML图和部署描述符的servlet间控制流图的构造。我们还概述了如何使用XML图和控制流信息来检查表单字段和会话状态的使用一致性。最后，在第6节中，我们讨论了实施整个分析系统的挑战和考虑因素，以及对性能和精度的期望。
技术报告[9]中提供了更多详细信息，我们在其中概述了Knuth用于检查上下文无关语法语言平衡的算法，解释了我们对Knuth用于构建平衡语法的算法的扩展，并考虑了分析的准确性。
- 分析输出流
Servlet通过将字符串值写入特殊的输出流来将数据发送到其客户端，该输出流由Web服务器为每个请求分配。我们的分析必须跟踪这些输出流，并跟踪写入它们的所有字符串值。对于给定的Web应用程序，该分析为每个servlet入口点生成一个上下文无关的语法，该语法的语言保证包含在运行时可能写到相应输出流的所有数据。
为了跟踪字符串值，我们首先按照[6]中的描述运行Java字符串分析，并使用每次写入，打印和附加调用的参数作为热点来对输出流进行附加。对于每次调用，结果都是一种常规语言，其中包含在这些程序点处可能出现的所有可能的字符串值。在字符串分析中，输出流的后续分析是String-Buffers的变体[6]。在这两种情况下，基本问题都是要跟踪可能对某些对象执行的侧面执行操作的可能顺序。但是，在输出流上仅存在类似于追加的操作，并且由于append是关联操作，因此这使得处理过程间数据流在我们的案例中稍微简单一些。
对于Web应用程序中的每种方法，我们生成一个流图，其中边表示控制流，并且节点具有以下种类：
–append：与输出流上的write，print或append操作相对应的append操作，其中参数是由初步字符串分析所产生的字符串值的常规语言给出的；
–调用：一种方法调用，携带有关其可能目标的信息；
–nop：连接点（例如，while语句或方法出口）。
即使对于单个servlet，构造这样的流图也不是一件容易的事。 Java语言带来了许多挑战，例如虚拟方法分派，异常以及通过实例字段和数组进行数据传输。另外，Java标准库允许流对象以不同的方式嵌套（使用BufferedStream，PrintWriter等）。幸运的是，大多数艰苦的工作都可以使用Soot框架[17]完成，就像在我们早期的Soot [6,5,10]应用程序中一样。我们还需要跟踪相关的输出流，但这可以通过Soot的别名分析功能轻松完成。 Servlet API中的请求分配机制可以类似地处理。
作为示例，我们从第1节中获得了示例程序的图1所示的流图。
我们使用以下有关上下文无关文法的术语。上下文自由语法（CFG）G是一个四元组（V，Sigma;，S，P），其中V是非终结字母，Sigma;是终结字母（在我们的语法中，Sigma;是Unicode字母），Vcap;Sigma;=empty;， Ssube;V是一组起始非终结点，而P是一个有限点形式为A→theta;的一组生产，其中Aisin;V和theta;isin;U lowast;，使用U表示组合字母Vcup;Sigma;。当A→theta;在P中时，我们写出alpha;Aomega;rArr;alpha;theta;omega;，并且alpha;，omega;isin;U lowast;和rArr; 和rArr;lowast;分别是rArr;的传递闭包和反射传递闭包。 G的语言定义为：
图1.示例程序的流程图
我们在此将追加节点描述为四舍五入的框，调用节点是正方形，nop节点是圆形，虚线边缘表示方法边界。
L(G) = {x isin; Sigma;lowast; | exist;s isin; S : s rArr; x}。 非终结点A的语言是：LG(A) = {x isin; Sigma;lowast; | A rArr; x} 。 从上下文中推断出G时，有时会省略G中的下标G。
给定一个流图，我们得出CFG G =（V，Sigma;，S，P），其中每个流图节点n与一个非终端Nn isin; V相关，这样L(Nn)是可以从n开始输出的字符串集。
对于一个边到m且标签为L的附加节点n，我们添加一个乘积Nn → RLNm，其中RL是L的线性子语法的起始非终结符；
对于具有后继m的调用节点n和节点t表示的可能的目标方法，我们添加Nn→NtNm； 和对于具有后继m的nop节点n，我们加上Nn→Nm，对于不具有n的节点后继者，我们加Nn →pound;。起始非终端是与servlet入口点相对应的非终端。
例子. 示例流图的语法具有V = {N1，...，N16，R3，R8，R12，R15}，并且P包含以下乘积：
- 使用平衡语法检查格式正确
此阶段的目标是检查给定的CFG G（G）中的所有字符串是否都是格式正确的XML文档。我们通过忽略XML注释，处理指令，实体引用以及空元素的紧凑形式（例如lt;brgt; lt;/brgt;可以写为lt;br/gt;）来简化表示，并且假定所有属性以name =“ value”形式编写。
此阶段分多个步骤进行，这些步骤考虑了格式正确的不同方面。但是，首先，我们需要能够轻松识别语法语言中两个字符lt;/的出现。我们通过简单的初步语法转换来实现这一目标-在不更改语法语言的情况下-消除了形式为Aalpha;lt;omega;的产生式omega; isin; V Ulowast; and; / isin; FIRST(omega;) or omega; rArr;lowast;and;/ isin; FOLLOW (A)。 （例如，[1]定义FIRST和FOLLOW。）从这里开始，lt;/视为单个字母符号。为了能够识别语法中的XML结构，我们定义了语法产生的六种特殊形式：
在此，C表示非终结符，称为内容非终结符，其产生全部以元素形式，文本形式或内容序列形式出现，而A表示非终结符，称为属性非终结符，其产生形式全部为属性形式，属性序列形式 或空白表格。 T代表非语言不包含空格且不包含lt;，gt;或=符号的终端，W表示非终结符，其语言由非空空格X组成，表示其语言不包含lt;的非终结符，并且V表示与X相同，不同之处在于它也排除了“。”我们说，如果每个起始非终结符sisin; S都是内容非终结符，则CFG处于标记形式。我们的目标是转换G 转换成标签形式的等效语法，并检查各种形式要求。
-
- 步骤1：获得平衡的语法
现在，我们将lt;（标记为开始标记的开始）作为左括号，将lt;/（标记为结束标记的开始）视为右括号。 L(G)格式正确的必要条件是，该视图中的语言是平衡的。 （如果 x isin; L，则语言L是均衡的。）要检查此属性，我们只需应用Knuth给我们一个等价的完全
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[409957]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
