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

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

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

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.

Figures/Tables 9

References 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]. .

Metrics

Recommended 0

No Suggested Reading articles found!

Composable information flow verification for service chain based on model checking

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 9

References 20

Related Articles 13

Metrics

Recommended 0

[1]	Ze’nan WANG, Jiao ZHANG, Shuo WANG, Tao HUANG, F.Richard Yu. Service chain deployment algorithms for deterministic end-to-end delay upper bound [J]. Journal on Communications, 2021, 42(11): 66-78.
[2]	Chen SUN,Jun BI,Zhilong ZHENG,Shuhe WANG,Hongxin HU. MicroNF:a microservice-based hybrid framework for NFV [J]. Journal on Communications, 2019, 40(8): 54-59.
[3]	Julong LAN,Zijin JIN,Penghao SUN,Yiming JIANG,Yue WANG. Service function chain construct algorithm based on reliability [J]. Journal on Communications, 2019, 40(1): 64-70.
[4]	Guoqing WANG,Lei ZHUANG,Ruimin WANG,Yu SONG,Kunli ZHANG. Modeling and verifying based on timed automata of Internet of things gateway security system [J]. Journal on Communications, 2018, 39(3): 63-75.
[5]	Shun WANG,Ye DU,Zhen HAN,Jiqiang LIU. Locality-guided based optimization method for bounded model checker [J]. Journal on Communications, 2018, 39(3): 181-190.
[6]	Hongqi ZHANG,Rui HUANG,Yingjie YANG,Dexian CHANG,Liancheng ZHANG. Cross-domain service chain mapping mechanism based on Q-learning [J]. Journal on Communications, 2018, 39(12): 102-112.
[7]	Liang WEI,Tao HUANG,Jiao ZHANG,Zenan WANG,Jiang LIU,Yunjie LIU. Service chain mapping algorithm based on reinforcement learning [J]. Journal on Communications, 2018, 39(1): 90-100.
[8]	Ding MA,Lei ZHUANG,Ju-long LAN. Discrete particle swarm optimization based multi-objective service path constructing algorithm [J]. Journal on Communications, 2017, 38(2): 94-105.
[9]	Jing YANG,Dan FAN,Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking [J]. Journal on Communications, 2015, 36(Z1): 266-276.
[10]	. Composable information flow verification for service chain based on model checking [J]. Journal on Communications, 2014, 35(11): 3-22.
[11]	Xiao-feng CHEN,Deng-guo FENG. Model checking of trusted cryptographic module [J]. Journal on Communications, 2010, 31(1): 59-64.
[12]	Xia LIU,Tian-long GU,Rong-sheng DONG,Yun-chuan GUO. Design and analysis of a novel fair payment protocol in mobile environments [J]. Journal on Communications, 2007, 28(4): 32-37.
[13]	Jia-jing LI,Tao WEI,Jian MAO. Method of model checking x86 executables for temporal security vulnerabilities [J]. Journal on Communications, 2007, 28(11A): 98-102.