基于接口精化的广义无干扰性研究-论文.pdf

《基于接口精化的广义无干扰性研究-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、计算机研究与发展DOI：10．7544／issn1OOO一1239．2015．20140306JournalofComputerResearchandDevelopment52(7)：1631—1641，2015基于接口精化的广义无干扰性研究孙聪习宁高胜。张涛李金库马建峰(西安电子科技大学网络与信息安全学院西安710071)。(中央财经大学信息学院北京102206)(suneong@xidian．edu．cn)AGeneralizedN0n—interferenceBasedonRefinementofInterfacesSunCong，XiNing，G

2、aoSheng，ZhangTao，LiJinku，andMaJianfeng(School0fCyberEngineering，XidianUniversity，X’an710071)(School0fJformation，CentralUniversityofFinanceandEconomics。Beijing102206)AbstractInthedesignandimplementationofcomplicatedcomponent—basedsoftwares，thesecurityrequirementsonthewholesystemar

3、ehardtoachieveduetothedifficultyonenforcingthecompositionalityofthesecurityproperties．Thespecificationandverificationofsecuritypropertiesarethecriticalissuesinthedevelopmentofcomponent—basedsoftwares．Inthispaper，wefocusonthegeneralizationonthesecuritylatticeovertheinformationflow

4、securitypropertiesenforceableonthecomponent—basedsoftwares．Thepreviousdefinitionsoftheinformationflowsecuritypropertiesinthecomponent—baseddesignarerestrictedonthebinarysecuritylatticemode1．Inthiswork。weextendtheinterfacestructureforsecuritytothegeneralizedinterfacestructureforse

5、curity(GISS)．Wedefine3refinementrelationandusethisrelationtogiveanon—interferencedefinition(SME—NI)based．ontheprincipleofsecuremulti—execution．Thisisthefirstapplicationofsecuremulti—executionontheinformationflowsecurityverificationofcomponent—basedsystems．Thenewdefinitionofnon—in

6、terferencecanbeadaptedtoanyfinitesecuritylatticemodels．TheCoqproofassistantisusedtoimplementthecertifiedlibraryforinterfaceautomata，aswellasthedecisionprocedurefortherefinementrelation．TheexperimentalresultsshowthecharacteristicsofSME—NIandthevalidityofdecisionprocedure．Keywordsi

7、nformationflowsecurity；non—interference；interfaceautomata；refinement；component—baseddesign摘要在复杂构件化软件的设计和实现过程中，由于安全属性的可组合性难以实现，使得系统整体的安全需求难以得到有效保证，因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题．针对当前构件化软件设计过程中，信息流安全属性仅局限于二元安全级格模型的问题，在现有安全接口结构基础上提出广义安全接口结构，在广义安全接口结构上定义精化关系，并利用这一精化关系定义了能够支持任意有限格模型

8、的基于安全多执行的无干扰属性，首次将安全多执行的思想应用于构件化系统的信息流安全