基于模型检测的服务链信息流安全可组合验证方法

doi:10.11959/j.issn.1000-436x.2014.11.003

通信学报 ›› 2014, Vol. 35 ›› Issue (11): 23-31.doi: 10.11959/j.issn.1000-436x.2014.11.003

基于模型检测的服务链信息流安全可组合验证方法

习宁,马建峰,孙聪,卢笛,张涛

西安电子科技大学计算机学院，陕西西安 710071

出版日期:2014-11-25 发布日期:2017-06-20
基金资助:
国家自然科学基金资助项目;国家自然科学基金资助项目;航空科学基金资助项目;航空科学基金资助项目;陕西省自然科学基础研究计划基金资助项目

Composable information flow verification for service chain based on model checking

Ning XI,Jian-feng MA,Cong SUN,Di LU,Tao ZHANG

School of Computer Science and Technology，Xidian University，Xi’an 710071，China

Online:2014-11-25 Published:2017-06-20
Supported by:
The National Natural Science Foundation of China;The National Natural Science Foundation of China;The Aviation Science Foundation of China;The Aviation Science Foundation of China;The Natural Science Basis Research Plan in Shaanxi Province of China

摘要/Abstract

摘要：

提出了一种可组合的服务链信息流安全验证方法。在保证单一组件信息流安全的基础上，给出相邻组件可组合的信息流安全条件和验证算法。实验和仿真结果表明，相比传统模型检测方法，所提的可组合验证算法能够有效减小验证开销，提高验证效率。

关键词: 模型检测, 服务链, 信息流安全, 可组合

Abstract:

A composable information verification approach is proposed for the secure service chain composition.Based on the secure service component，the security constraints for the component’s composibility is specified and the information flow verification algorithms is proposed.Through the experiments and simulation，it shows that the approach can decrease the verification cost effectively and improve the efficiency of the verification.

Key words: model checking, service chain, information flow security, composibility

习宁,马建峰,孙聪,卢笛,张涛. 基于模型检测的服务链信息流安全可组合验证方法[J]. 通信学报, 2014, 35(11): 23-31.

Ning XI,Jian-feng MA,Cong SUN,Di LU,Tao ZHANG. Composable information flow verification for service chain based on model checking[J]. Journal on Communications, 2014, 35(11): 23-31.

图/表 9

图1

图2

图3

图4

图5

图6

图7

图8

图9

参考文献 20

[1]	ENDREI M ， ANG J ， ARSANJANI A ，et al. Patterns:Service Oriented Architecture and Web Services[S].IBM International Technical Support Organization，2004. IBM International Technical Support Organization， 2004.
[2]	JOANNA N . The Personal Web:smart internet for me[A]. Proceedings of the 2010 Conference of the Center for Advanced Studies on Collaborative Research[C]. 2010.
[3]	YU T ， ZHANG Y ， LIN K J . Efficient algorithms for Web services selection with end-to-end QoS constraints[J]. ACM Transactions on the Web (TWEB)， 2007，1(1): 103-126.
[4]	龙军，袁鑫攀，桂卫华 . 基于环境感知的可信QoS评价与服务选取策略[J]. 电子学报， 2012，40(6): 1133-1140. LONG J ， YUAN X P ， GUO W H . A policy for the trusted QoS evaluation and service selection with environment aware[J]. Acta Electronica Sinica， 2012，40(6): 1133-1140.
[5]	BERTINO E ， SQUICCIARINI A C ， MEVI D . A fine-grained access control model for Web services[A]. SCC[C]. 2004. 33-40.
[6]	BHATTI R ， BERTINO E ， GHAFOOR A . Trust-based context-awareaccess control model for Web-services[A]. ICWS[C]. 2004. 184-191.
[7]	ZHENG Z B ， ZHU J M ， LYU M R . Service-generated big data and big data-as-a-service:an overview[A]. 2013 IEEE International Congress on Big Data[C]. 2013. 403-410.
[8]	VOLPANO D ， IRVINE C ， SMITH G . A sound type system for secure flow analysis[J]. Journal of Computer Security， 1996，4(2): 167-187.
[9]	FERRANTE J ， OTTENSTEIN K J ， WARREN J D . The program dependence graph and its use in optimization[J]. ACM Transactions on Programming Languages and Systems， 1987，9(3): 319-349.
[10]	DIMITROVA R ， FINKBEINER B，KOVáCS M ， et al.Model Checking Information Flow in Reactive Systems . Verification，Model Checking，and Abstract Interpretation[M]. Springer Berlin Heidelberg， 2012. 169-185.
[11]	HUTTER D ， VOLKAMER M . Information flow control to secure dynamic Web service composition[A]. Security in Pervasive Computing[C]. 2006. 196-210.
[12]	XI N ， MA J F ， SUN C ， et al. Distributed information flow verification framework for the composition of service chain in wireless sensor network[EB/OL]. .
[13]	NAKAJIMA S . Model-checking of safety and security aspects in Web service flows[A]. ICWE 2004[C]. 2004. 488-501.
[14]	SABINA R L S . Model checking adaptive multilevel service compositions[A]. FACS 2010[C]. 2012. 106-124.
[15]	SUN C ， ZHAI E ， CHEN Z ，et al. A multi-compositional enforcement on information flow security[J]. Information and Communications Security Lecture Notes in Computer Science， 2011，7043: 345-359.
[16]	GROBA C ， CLARKE S . Opportunistic composition of sequentially-connected services in mobile computing environments[A]. ICWS[C]. 2011. 17-24.
[17]	BIBA K J . Integrity Considerations for Secure Computer Systems[R]. Electronic Systems Division，Bedford，MA， 1977.
[18]	BARTHE G，D’ARGENIO P R ， RESK T . Secure information flow by self-composition[A]. Proc of the 17th Computer Security Foundations Workshop[C]. 2004. 100-114.
[19]	Open Source Project.Spin verification tool[EB/OL]. .
[20]	Open Source Project.NS-3 project[EB/OL]. .

基于模型检测的服务链信息流安全可组合验证方法

Composable information flow verification for service chain based on model checking

在线阅读

PDF下载

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 9

参考文献 20

相关文章 15

Metrics

推荐阅读 0

[1]	田有亮, 蒋小霞. 通用可组合框架下的公平理性委托计算[J]. 通信学报, 2021, 42(9): 106-119.
[2]	王泽南, 张娇, 汪硕, 黄韬, F.RichardYu. 端到端时延上限确定的服务链部署算法[J]. 通信学报, 2021, 42(11): 66-78.
[3]	孙晨,毕军,郑智隆,王舒鹤,胡宏新. MicroNF：基于微服务的异构网络功能虚拟化框架[J]. 通信学报, 2019, 40(8): 54-59.
[4]	王国卿,庄雷,王瑞民,宋玉,张坤丽. 基于时间自动机的物联网网关安全系统的建模及验证[J]. 通信学报, 2018, 39(3): 63-75.
[5]	王舜,杜晔,韩臻,刘吉强. 基于程序局部性引导的有界模型检测优化方法[J]. 通信学报, 2018, 39(3): 181-190.
[6]	张红旗,黄睿,杨英杰,常德显,张连成. 基于Q-learning的跨域服务链映射机制[J]. 通信学报, 2018, 39(12): 102-112.
[7]	魏亮,黄韬,张娇,王泽南,刘江,刘韵洁. 基于强化学习的服务链映射算法[J]. 通信学报, 2018, 39(1): 90-100.
[8]	马丁,庄雷,兰巨龙. 基于离散粒子群优化的多目标服务路径构建算法[J]. 通信学报, 2017, 38(2): 94-105.
[9]	杨京,范丹,张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015, 36(Z1): 266-276.
[10]	原变青,刘吉强. 可证明安全的RFID标签所有权转移协议[J]. 通信学报, 2015, 36(8): 83-90.
[11]	习宁，马建峰，孙聪，卢笛，张涛. 基于模型检测的服务链信息流安全可组合验证方法[J]. 通信学报, 2014, 35(11): 3-22.
[12]	吴振强,周彦伟,乔子芮. 移动互联网下可信移动平台接入机制[J]. 通信学报, 2010, 31(10): 158-169.
[13]	陈小峰,冯登国. 可信密码模块的模型检测分析[J]. 通信学报, 2010, 31(1): 59-64.
[14]	邓淼磊,马建峰,周利华. RFID匿名认证协议的设计[J]. 通信学报, 2009, 30(7): 20-26.
[15]	马卓,马建峰,曾勇,沈玉龙. 通用可组合安全的WLAN Mesh网络可信接入认证协议[J]. 通信学报, 2008, 29(10): 126-134.