Web交互的挑战与前景

理论计算机科学电子笔记157（2006）41-46www.elsevier.com/locate/entcsWeb验证：前景与挑战Shriram Krishnamurthi克里希那穆提1，2计算机科学系关闭WI，USA摘要Web为编程语言设计和验证以及它们的交叉点提出了新颖而有趣的问题。本文提供了一个关于这一主题的工作线程的个人纲要。关键词：Web应用程序，时态验证，访问控制，程序分析1、什么是网站？“网站”一词包含着一种隐藏的歧义。一个站点是一个静态的实体，被看作是一个程序源，还是一个动态的实体，通过用户行为的镜头来观看？这种区别对分析和验证网站的意义产生了重大影响。所有传统的静态和动态分析之间的权衡都适用：静态分析可以量化所有程序行为，但通常不那么具体;动态分析只能相对于它所检查的行为提供更多的保证，但额外的上下文信息通常可以产生更多信息的答案。由于Web交互的性质，这种区别在Web上可能更重要。1 这项工作部分由NSF资助CCR-0305949和CCF-0447509。2电子邮件：sk@cs.brown.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.04442S. Krishnamurthi/Electronic Notes in Theoretical Computer Science 157（2006）412Web交互在控制台甚至GUI应用程序中，用户不能选择后退或前进，不能克隆窗口并提交来自两个克隆的响应，等等，这些用户交互功能将Web应用程序与许多其他类型的交互程序区分开来。事实上，许多网站都因为对这种交互的糟糕处理而臭名昭著。例如，在一些旅游网站上，查看酒店列表，在新窗口中查看一个选择，在另一个新窗口中查看第二个选择，然后切换回预订第一家酒店，将导致预订第二家酒店[5]。Web应用程序不仅必须对这些操作的可能性敏感，而且必须经常在没有浏览器帮助的情况下检测它们（浏览器不会报告每个用户操作）。此外，呈现平台的可用性很可能会激发创新，这意味着浏览器的集合以及交互行为的集合将随着时间的推移而增长。这使得网站分析特别令人兴奋和具有挑战性。3网站验证我的工作主要集中在Web程序的静态分析上。具体来说，我从两个互补的角度研究了Web应用程序。所有这些工作都是由构建一个强大的应用程序的愿望驱动的，除了作为研究问题的生成器之外，3.1驾驶应用具体的应用程序是CONTINUE[7，9]，一个基于Web的应用程序，会议论文管理。 CONTINUE在精神上类似于几个程序在这种类型中（尽管它在用户界面质量上投入了相当多的资金），所以熟悉其中一个应用程序对于在高层次上理解它是足够的。它具有许多其他会议应用程序中没有的几个有用功能，包括征求子评论，帮助主席分配任务以及更改用户身份。我的目标是创建一个应用程序，不仅是可用的，但也已经验证了沿尽可能多的维度，因为足够的可靠性。毕竟，当一个社区将创建论文作为研究的表达作为主要目标时，安全处理这些论文应该被认为是关键任务！S. Krishnamurthi/Electronic Notes in Theoretical Computer Science 157（2006）41433.2时间行为Web应用程序必须满足许多时态规范。例如，在一个旅游预订网站上，用户期望他们预订的酒店与他们选择的酒店相同--即使他们选择沿途调查其他在虚拟书店中，用户可能有一个他们或者至少是商店我希望每一本放在购物车里的书都是在最后结账时购买的。(In事实上，实际的财产将更加微妙：购买的书籍必须是所有那些放在购物车中，随后没有被移除的书籍，创造了额外的时间量化水平。在C continue中有几个类似的“合理”行为的期望时态属性的陈述自然建议使用模型检查器[1]。这在实践中证明有些复杂。例如，一个简单的模型检查的使用不会捕获第2节中提到的一些交互引起的错误。为什么不呢？因为从Web应用程序构建的自然模型无法捕获用户可以通过浏览器执行的许多行为;通俗地说，Web应用程序的源代码中没有任何地方说，建立精确模型的问题进一步受到了对多种Web交互进行解释的问题的阻碍。浏览器不仅提供了过多的选择，甚至流行的浏览器也有不同的功能集--这为了支持浏览器的许多交互功能，我们采用了先前的工作，提出了Web交互的核心模型[5]。这个模型提供了一个小的Web原语集，这些原语足以对所有已知的Web交互形式进行建模，并且还应该涵盖许多新的形式。基于这种抽象，我们一直在研究构建一个能够处理Web微妙之处的模型检查器的问题[10]。请注意，这不是一个只针对Web特定交互的模型检查器，而是一个也会考虑Web交互的模型检查器：也就是说，如果程序违反了独立于任何Web交互的属性，检查器也会发现这些属性。本作品中的属性语言很微妙，因此很有趣。具体来说，属性需要能够引用网页的元素。为了索引这些元素，我们避免解析HTML（一个费力不讨好的活动！）以及使用静态距离坐标（这将太脆弱）。相反，我们希望开发人员使用CSS样式表（CSS）标记来标记各个页面元素.这些不仅是大多数开发人员词汇表的一部分44S. Krishnamurthi/Electronic Notes in Theoretical Computer Science 157（2006）41以突出视觉效果。虽然这些想法在科学上并不深刻，但我相信它们对于成功部署正式方法至关重要。3.3信息安全和可见性一个针对时间行为的程序在会议服务器中节目组成员该看的评论可以看，不该看的不能看。这些属性通常属于访问控制的范畴。一旦我们发现了CONTINUE中的实际信息访问错误（这些错误已经被修复！），我们已着手研究访问控制政策的规范和验证。由于Web上信息的广泛可用性，访问控制获得了新的普及。特别是，由于许多Web应用程序是数据库上的接口，并且在不同的环境中向不同的用户提供相同的数据，因此访问控制越来越多地成为基于角色的。像XACML[3]这样的工业标准，实际上是一种基于规则的语言，被用来描述这些策略，它们的评估引擎也被用来验证这些策略。我们在这一领域的工作[2]集中在XACML的一个受限（但仍然有用）子集的两个问题上。首先，自然是一个政策是否满足某些属性集的问题;这是传统的验证问题。第二个更有趣。鉴于这些策略语言的简单性，很容易修补问题并快速检查新策略是否在特定输入上执行了预期的操作。然而，补丁可能会暴露私人数据，或使必要的信息不可用。这些政策语言的声明性质加剧了这种危险，因为变化可能产生非常非本地的影响。因此，简单的句法差异不再足够;用户需要某种形式的语义差异。这是我们工作要解决的第二个问题。值得注意的是，围绕信息访问的问题-特别是泄漏的危险-为静态分析提供了一个令人信服的理由：没有审查人员希望听到他们的机密评论由于缺乏良好的测试用例而被泄露。通过假阳性肯定是繁重的;为了有效，这种成本必须保持最小。然而，这是一个静态分析可以提供的普遍量化保证值得合理成本的例子。S. Krishnamurthi/Electronic Notes in Theoretical Computer Science 157（2006）41454Web程序关注Web程序（作为静态实体）会带来一个有趣的微妙之处。为了遵守Web的无状态特性，Web应用程序的结构传统上被此外，重要的信息是使用隐藏字段和其他传统上被静态分析忽略的通道进行通信的。因此，传统的静态分析将近似大量的重要信息（特别是属性中提到的值）。由此产生的模型对进一步分析毫无用处。毫不奇怪，读者分析的问题同样困扰着开发者。因此，最近有一种趋势是在源程序中使用基于延续的原语，它可以在编译后由专门的服务器[6，12]或传统的服务器[11]处理。例如，这意味着词法绑定在源代码中保持原样，而不是转换为隐藏字段或其他外部存储。通过避免这种程序反转，这种形式的源程序因此是更好的输入，现有的程序分析。5若干研究问题在这一领域有许多开放的研究问题。以下只是一个小的和折衷的抽样。其中一些最有趣的是与访问控制有关。例如，大多数访问控制验证工作只处理策略。但要真正有效，它还必须考虑程序相对于策略的行为。(In在一个极端的情况下，如果应用程序严格地咨询策略引擎，但总是忽略它的响应，那么再多的策略验证也没用。虽然这种特殊的行为可能看起来很极端，但在测试过程中并不是不可想象的，缺乏好的测试套件将无法发现这个原型未能从脚本成长为程序的所有地方。访问控制策略还需要解决这些应用程序的临时行为。虽然一些研究已经研究了时间策略，但尚不清楚这些结果如何适用于结构化程度较低的Web世界，其中程序可能有多个入口点，用户可以参与程序无法阻止的复杂交互。Web应用程序的另一个重要方面是它们越来越不再“在Web上”。越来越多的网站现在广泛使用客户端脚本语言，特别是JavaScript，以实现-46S. Krishnamurthi/Electronic Notes in Theoretical Computer Science 157（2006）41大量用户操作。特别是，尽管JavaScript的使用往往局限于回显浏览器操作或在通过网络传输数据之前执行一致性检查，但现在应用程序源代码的重要部分与页面一起下载。这为跨语言分析带来了挑战和机遇。致谢我感谢几位合作者，我有幸与他们一起我特别感谢Pete Hopkins，他帮助CONTINUE从一个非常好的原型转变为一个真正的产品。甚至他的bug都比大多数人的程序更有趣引用[1] Clarke，E.，O. Grumberg和D. Peled，[2] Fisler，K.，S. 克里希纳穆尔蒂湖A. Meyerovich和M.C. Tschantz，访问控制策略的验证和变更影响，国际软件工程会议，2005年。[3] Godik，S.和T.M. （编辑），可扩展访问控制标记语言，版本1.1（2003）。[4] Graham，P.，超越平均值（2001），http://www.paulgraham.com/avg.html。[5] 格 劳 恩 克 山 口 T. ， R. B. Findler ， S.Krishnamurthi 和 M.Felleisen ， Modeling Webinteractions，in：European Symposium on Programming，2003，pp.238-252.[6] 格劳恩克山口T.，S. Krishnamurthi，S.van der Hoeven和M.Felleisen，Programming theWebwith High-Level Programming Languages，欧洲编程研讨会，2001年。122-136.[7] Hopkins，P.W.，在Web应用程序中使用send/suspend/dispatch启用复杂的UI，在：计划讲习班，2003年。[8] 休斯，J.，将单子推广到箭头，计算机编程科学37（2000），pp。67比111[9] Krishnamurthi，S.，的继续服务器，在：研讨会上的实际问题，声明性语言，2003年，pp。2比16[10] Licata，D.R. 和S.Krishnamurthi，《交互式Web程序》，载于：IEEE自动化软件工程国际研讨会，2004年，pp.164-173。[11] 马修斯，J.，R. B. Findler，P.T. Graunke，S.Krishnamurthi和M.Felleisen，Automaticallyrestructuring programs for the Web，Automated Software Engineering：An InternationalJournal（2003）。[12] 奎内克角，浏览器对评估器的影响，或者继续对Web服务器进行编程，在：ACM SIGPLAN函数式编程国际会议，2000年，pp. 23-33号。