English

应用科学学报 ›› 2011, Vol. 29 ›› Issue (1): 83-92.doi: 10.3969/j.issn.0255-8297.2011.01.015

• 计算机科学与应用 • 上一篇    下一篇

威胁驱动的Web应用On-The-Fly导航模型验证方法

胡立立1;2， 缪淮扣1;2， 陈圣波1;2， 梅佳1， 高洪皓1   

  1. 1. 上海大学计算机工程与科学学院，上海200072
    2. 上海市计算机软件评测重点实验室，上海201112
  • 收稿日期:2010-10-15 修回日期:2010-11-08 出版日期:2011-01-26 发布日期:2011-01-25
  • 通信作者: 缪淮扣，教授，博导，研究方向：软件形式化验证，E-mail: hkmiao@shu.edu.cn
  • 作者简介:缪淮扣，教授，博导，研究方向：软件形式化验证，E-mail: hkmiao@shu.edu.cn
  • 基金资助:

    国家自然科学基金(No.60673115, No.60970007)；国家“973”重点基础研究发展计划基金(No.2007CB310800)；上海市自然科学基金(No.09ZR1412100)；上海市科委项目基金(No.10510704900)；上海市重点学科建设项目基金(No.J50103)资助

Threat-Driven On-The-Fly Verification of Navigation Model for Web Applications

HU Li-li1;2, MIAO Huai-kou1;2, CHEN Sheng-bo1;2, MEI Jia1, GAO Hong-hao1   

  1. 1. School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China
    2. Shanghai Key Laboratory of Computer Software Testing and Evaluating, Shanghai 201112, China
  • Received:2010-10-15 Revised:2010-11-08 Online:2011-01-26 Published:2011-01-25

PDF

1884

被引次数

6

摘要：

 以Web应用为代表的网络软件安全性受到业界的广泛关注，对具有复杂交互行为的Web应用安全性建模和验证是一个挑战. 该文提出一种威胁驱动的Web应用On-the-Fly导航模型验证方法，采用威胁驱动方法从规格说明中设计和抽取用于性质检验的安全性质，利用模型检测工具NuSMV对建立的模型进行验证. 实验结果表明该方法可以减少搜索空间并在一定程度上避免状态空间爆炸.

关键词: On-The-Fly验证；Web应用；安全性

Abstract:

Security of network software such as Web applications has drawn much attention in the industry.Modeling and verifying Web applications involving intricate interactions are a challenge to software developers.In this paper, we propose a threaten-driven approach to model and verify the on-the-fly navigation model of Web applications. Security properties are extracted from the model based on the threaten-driven method. Using the model checking tool NuSMV, we have verified the model. The experimental results indicate that the proposed approach can avoid state space explosion to a certain extent.

Key words: on-the-fly verification, Web application, security property

中图分类号: