| 威胁驱动的Web应用On-The-Fly导航模型验证方法 |
| |
| 引用本文： | 胡立立,缪淮扣,陈圣波,梅佳,高洪皓. 威胁驱动的Web应用On-The-Fly导航模型验证方法[J]. 应用科学学报, 2011, 29(1): 83-92. DOI: 10.3969/j.issn.0255-8297.2011.01.015 |
| |
| 作者姓名： | 胡立立 缪淮扣 陈圣波 梅佳 高洪皓 |
| |
| 作者单位： | 1. 上海大学计算机工程与科学学院，上海2000722. 上海市计算机软件评测重点实验室，上海201112 |
| |
| 基金项目： | 国家自然科学基金，国家"973"重点基础研究发展计划基金，上海市自然科学基金，上海市科委项目基金，上海市重点学科建设项目基金 |
| |
| 摘 要： | 以Web应用为代表的网络软件安全性受到业界的广泛关注，对具有复杂交互行为的Web应用安全性建模和验证是一个挑战. 该文提出一种威胁驱动的Web应用On-the-Fly导航模型验证方法，采用威胁驱动方法从规格说明中设计和抽取用于性质检验的安全性质，利用模型检测工具NuSMV对建立的模型进行验证. 实验结果表明该方法可以减少搜索空间并在一定程度上避免状态空间爆炸.
|
| 关 键 词： | On-The-Fly验证；Web应用；安全性 |
| 收稿时间： | 2010-10-15 |
| 修稿时间： | 2010-11-08 |
Threat-Driven On-The-Fly Verification of Navigation Model for Web Applications |
| |
| HU Li-li,MIAO Huai-kou,CHEN Sheng-bo,MEI Jia,GAO Hong-hao. Threat-Driven On-The-Fly Verification of Navigation Model for Web Applications[J]. Journal of Applied Sciences, 2011, 29(1): 83-92. DOI: 10.3969/j.issn.0255-8297.2011.01.015 |
| |
| Authors: | HU Li-li MIAO Huai-kou CHEN Sheng-bo MEI Jia GAO Hong-hao |
| |
| Affiliation: | 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 |
| |
| 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. |
| |
| Keywords: | on-the-fly verification Web application security property |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《应用科学学报》浏览原始摘要信息 |
|
点击此处可从《应用科学学报》下载全文 |
