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

摘要

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