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

Verification of pattern driven system security design

作　　者：郑小宇 刘冬梅[1] 杜益宁 周子健 邱玫媚 朱鸿 ZHENG Xiao-yu;LIU Dong-mei;DU Yi-ning;ZHOU Zi-jian;QIU Mei-mei;ZHU Hong(School of Computer Science and Engineering,Nanjing University of Science and Technology,Nanjing 210094,China;School of Engineering,Computing and Mathematics,Oxford Brookes University,Oxford OX33 1HX,UK)

机构地区：[1]南京理工大学计算机科学与工程学院,江苏南京210094 [2]Oxford Brookes大学工程、计算和数学学院,英国牛津OX331HX

出　　处：《计算机工程与科学》2020年第7期1197-1207,共11页Computer Engineering & Science

基　　金：国家自然科学基金(61502233,61402229);江苏高校“青蓝工程”;中央高校基本科研业务费专项资金(30916011328);欧盟移动云计算FP7项目MONICA(PIRSES-GA-2011-295222)。

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]