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

摘要：

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

关键词：安全设计模式、代数规约、形式化验证、模型检测

所属期刊栏目：42

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金;江苏高校"青蓝工程";中央高校基本科研业务费专项资金;欧盟移动云计算 FP7项目MONICA

在线出版日期：2020-07-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1197-1207