JOC_基于UML和模型检测的安全模型验证方法.pdf

第32卷第4期计算机学报Vol.32No.4
2009年4月CHINESEJOURNALOFCOMPUTERSApr.2009

基于UML和模型检测的安全模型验证方法

1),2)2)
程亮张阳
1)(中国科学技术大学电子工程与信息科学系合肥230027)
2)(中国科学院软件研究所信息安全国家重点实验室北京100190)

摘要安全策略的形式化分析与验证随着安全操作系统研究的不断深入已成为当前的研究热点之一.文中在总
结前人工作的基础上,首次提出一种基于UML和模型检测器的安全模型验证方法.该方法采用UML将安全策略
模型描述为状态机图和类图,然后利用转换工具将UML图转化为模型检测器的输入语言,最后由模型检测器来验
证安全模型对于安全需求的满足性.作者使用该方法验证了DBLP和SLCF模型对机密性原则的违反.

关键词安全操作系统;系统操作安全;安全策略模型;形式化验证;模型检测;UML
中图法分类号TP309DOI号:10.3724/SP.J.1016.2009.00699

AVerificationMethodofSecurityModelBasedonUMLandModelChecking

CHENGLiang1),2)ZHANGYang2)
1)(DepartmentofElectronicEngineeringandInformationScience,UniversityofScienceandTechnologyofChina,Hefei230027)
2)(StateKeyLaboratoryofInformationSecurity,InstituteofSoftware,ChineseAcademyofSciences,Beijing100190)

AbstractAsthedevelopmentofsecurityoperatingsystem,theformalanalysisandverification
ofthesecuritymodelshasbeenoneofthehottesttopicsnow.Anewmethodtoverifythecor
rectnessofsecuritymodelsisproposedinthispaperbasedonthestudyofpredecessors!work,
whichmadeuseoftheUnifiedModelingLanguage(UML)andmodelchecking.Thisapproach
firstusedtheUMLtospecifythesecuritymodelintheformoffinitestatemachinediagramsand
theclassdiagrams,andthentranslatedtheseUMLdiagramstotheinputlanguageofmodel
checkers.Anditusedthemodelcheckertoverifythemodel!scorrectnessortheviolationofse
curitypropertiesforthelaststep.Theauthorsdemonstratetheviolationofconfidentialityofthe
DBLPandSLCFmodelbythenewapproach.

Keywordssecurityoperatingsystem;securitymodel;formalverification;modelchecking;
UML

层规范进行一致性的证明[4].然而,由于安全模型都
1引言是采用形式化方法进行描述的,对于实际的软件开
发者来说,直接采用形式化安全模型作为他们的开
安全策略模型的形式化分析与验证一直是安全发任务是件很困难的事情.因此,需要一种机制帮助
操作系统研发中的重点问题[13].国标GB17859软件开发者或者系统管理员在软件设计阶段理解、
1999在第五级中明确要求了需要对安全模型和顶验证和实施安全模型以及相关策略.事实上,在软件

收稿日期:20081126;最终修改稿收到日期:20090115.本课题得到国家八六三高技术研究发展计划项目基金(2007AA01Z465,
2006AA01Z433,2007AA01Z475,2007AA01Z414)资助.程亮,男,1982年生,博士研究生,主要研究方向为安全操作系统及验证.
Email:[e-mail].张阳,女,1971年生,博士,主要研究方向为操作系统安全.
700计算机学报