模式驱动的系统安全性设计的验证

随着万维网和移动计算技术的广泛应用,系统安全性得到了越来越多的关注,使用安全模式对系统安全解决方案进行设计并验证是提升系统安全性的一种有效途径。现有方法根据系统安全需求选择适用的安全模式,在此基础上将模式组合为系统的安全解决方案,并通过模型检测方法验证其安全性。但是,这些方法往往将方案看作整体进行验证,忽略了内部安全模式的组合细节,难以在包含大量模式的复杂系统中定位缺陷。提出一种模式驱动的系统安全性设计的验证方法,首先使用代数规约语言SOFIA描述安全模式及其组合,以构建系统安全解决方案的形式化模型;然后将SOFIA规约转换为Alloy规约后,使用模型检测工具验证模式组合的正确性和系统的安全性。案例研究表明,该方法能够有效地验证系统安全解决方案的正确性。

Verification of pattern driven system security design

With the wide use of the World Wide Web and mobile computing technology, system security has received more and more attentions. Using security models to design and verify system security solutions is an effective way to improve the system security. The existing methods select the applicable security patterns according to the security requirements of the system and then combine the patterns into a system security solution. The security is verified by the model detection method. However, these methods often regard the scheme as a whole for verification, ignoring the combination details of internal security patterns, and it is difficult to locate defects in a complex system containing a large number of patterns. A verification method for pattern-driven system security design is proposed. Firstly, the algebraic protocol language SOFIA is used to describe the security model and its combination to build a formal model of the system security solution. Secondly, the SOFIA protocol is converted to the Alloy protocol, and the model checking tool is used to verify the correctness of the pattern combination and the security of the system. A case study demonstrates that this method can effectively verify the correctness of system security solution.