资源描述：
《JOC_基于UML和模型检测的安全模型验证方法.pdf》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。
1、第32卷第4期计算机学报Vol.32No.42009年4月CHINESEJOURNALOFCOMPUTERSApr.2009基于UML和模型检测的安全模型验证方法1),2)2)程亮张阳1)(中国科学技术大学电子工程与信息科学系合肥230027)2)(中国科学院软件研究所信息安全国家重点实验室北京100190)摘要安全策略的形式化分析与验证随着安全操作系统研究的不断深入已成为当前的研究热点之一.文中在总结前人工作的基础上,首次提出一种基于UML和模型检测器的安全模型验
2、证方法.该方法采用UML将安全策略模型描述为状态机图和类图,然后利用转换工具将UML图转化为模型检测器的输入语言,最后由模型检测器来验证安全模型对于安全需求的满足性.作者使用该方法验证了DBLP和SLCF模型对机密性原则的违反.关键词安全操作系统;系统操作安全;安全策略模型;形式化验证;模型检测;UML中图法分类号TP309DOI号:10.3724/SP.J.1016.2009.00699AVerificationMethodofSecurityModelBasedonUMLandModelC
3、hecking1),2)2)CHENGLiangZHANGYang1)(DepartmentofElectronicEngineeringandInformationScience,UniversityofScienceandTechnologyofChina,Hefei230027)2)(StateKeyLaboratoryofInformationSecurity,InstituteofSoftware,ChineseAcademyofSciences,Beijing100190)Abstr
4、actAsthedevelopmentofsecurityoperatingsystem,theformalanalysisandverificationofthesecuritymodelshasbeenoneofthehottesttopicsnow.Anewmethodtoverifythecorrectnessofsecuritymodelsisproposedinthispaperbasedonthestudyofpredecessors!work,whichmadeuseoftheUn
5、ifiedModelingLanguage(UML)andmodelchecking.ThisapproachfirstusedtheUMLtospecifythesecuritymodelintheformoffinitestatemachinediagramsandtheclassdiagrams,andthentranslatedtheseUMLdiagramstotheinputlanguageofmodelcheckers.Anditusedthemodelcheckertoverifyth
6、emodel!scorrectnessortheviolationofsecuritypropertiesforthelaststep.TheauthorsdemonstratetheviolationofconfidentialityoftheDBLPandSLCFmodelbythenewapproach.Keywordssecurityoperatingsystem;securitymodel;formalverification;modelchecking;UML[4]层规范进行一致性的证
7、明.然而,由于安全模型都1引言是采用形式化方法进行描述的,对于实际的软件开发者来说,直接采用形式化安全模型作为他们的开安全策略模型的形式化分析与验证一直是安全发任务是件很困难的事情.因此,需要一种机制帮助[13]操作系统研发中的重点问题.国标GB17859软件开发者或者系统管理员在软件设计阶段理解、1999在第五级中明确要求了需要对安全模型和顶验证和实施安全模型以及相关策略.事实上,在软件收稿日期:20081126;最终修改稿收到日期:20090115.本课题得到国家八六三高技术研究
8、发展计划项目基金(2007AA01Z465,2006AA01Z433,2007AA01Z475,2007AA01Z414)资助.程亮,男,1982年生,博士研究生,主要研究方向为安全操作系统及验证.Email:chengliang@is.iscas.ac.cn.张阳,女,1971年生,博士,主要研究方向为操作系统安全.700计算机学报2009年设计开发领域中,UML语言已成为实际上的设计公式,工作效率比较低.与分析面向对象软件系统的
