基于计算模型的安全协议Swift语言实施安全性分析

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

Abstract

Abstract:

Analysis of security protocol Swift implementations in IOS platform is important to protect the security of IOS applications.Firstly,according to the security protocol Swift implementations,the SubSwift language,which was a subset of Swift language,was widely used in IOS system,and its BNF were specified.Secondly,the mapping model from SubSwift language to Blanchet calculus based on the operational semantic was presented which consisted of mapping rules,relationship from the statements and types in SubSwift language to Blanchet calculus.And then,a method of generating security protocol Blanchet calculus implementations from SubSwift language implementations was developed.Finally,security protocol Blanchet calculus implementation generation tool SubSwift2CV was developed with Antrl4 and Java language.At the same time,OpenID Connect,Oauth2.0 and TLS security protocol SubSwift language implementations were analyzed with SubSwift2CV and CryptoVerif.

Key words: security protocol, implementations security, Swift language, formal analysis, model extraction

CLC Number:

TP309

Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model[J]. Journal on Communications, 2018, 39(9): 178-190.

Figures/Tables 25

References 38

[1]	张焕国, 韩文报, 来学嘉 ,等. 网络空间安全综述[J]. 中国科学:信息科学, 2016,46(2): 125-164.
	ZHANG H G , HAN W B , LAI X J ,et al. Survey on cyberspace security[J]. SCIENTIA SINICA Informationis, 2016,46(2): 125-164.
[2]	王世伟 . 论信息安全、网络安全、网络空间安全[J]. 中国图书馆学报, 2015(2): 72-84.
	WANG S W . On information security,network security and cyberspace security[J]. Journal of Library Science in China, 2015(2): 72-84.
[3]	MIN K S , CHAI S W , HAN M . An international comparative study on cyber security strategy[J]. International Journal of Security and its Applications, 2015,9(2): 13-20.
[4]	张焕国, 吴福生, 王后珍 ,等. 密码协议代码执行的安全验证分析综述[J]. 计算机学报, 2018,41(2): 288-308.
	ZHANG H G , WU F S , WANG H Z ,et al. A survey:security verification analysis of cryptographic protocols implementations on real code[J]. Chinese Journal of Computers, 2018,41(2): 288-308.
[5]	孟博, 张金丽, 鲁金钿 . 基于计算模型的OpenID Connect协议认证性的自动化分析[J]. 中南大学民族大学学报（自然科学版）, 2016,35(3): 123-129.
	MENG B , ZHANG J L , LU J T . Automatic analysis of authentication of OpenID Connect protocol based on the computational model[J]. Journal of South-Central University for Nationalities (Natural Science Edition), 2016,35(3): 123-129.
[6]	牛乐园, 杨伊彤, 王德军 ,等. 计算模型下的SSHV2协议认证性自动化分析[J]. 计算机工程, 2015,41(10): 148-154.
	NIU L Y , YANG Y T , WANG D J ,et al. Automatic analysis on authentication of SSHV2 protocol in computational model[J]. Computer Engineering, 2015,41(10): 148-154.
[7]	AVALLE M , PIRONTI A , SISTO R . Formal verification of security protocol implementations:a survey[J]. Formal Aspects of Computing, 2014,26(1): 99-123.
[8]	MENG B , HUANG C T , YANG Y T ,et al. Automatic generation of security protocol implementations written in Java from abstract specifications proved in the computational model[J]. International Journal of Network Security, 2017,19(1): 138-153.
[9]	MENG B , YANG Y T , ZHANG J L ,et al. PV2Java:automatic generator of security protocol implementations written in Java language from the applied PI calculus proved in the symbolic model[J]. International Journal of Security and its Applications, 2016,10(11): 211-229.
[10]	孟博, 王德军 . 安全协议实施自动化生成与验证[M]. 北京: 科学出版社, 2016.
	MENG B , WANG D J . Automatic generation and verification of security protocols’ implements[M]. Beijing: Science PressPress, 2016.
[11]	雷新锋, 宋书民, 刘伟兵 ,等. 计算可靠的密码协议形式化分析综述[J]. 计算机学报, 2014,37(5): 993-1016.
	LEI X F , SONG S M , LIU W B ,et al. A Survey on computationally sound formal analysis of cryptographic protocols[J]. Chinese Journal of Computers, 2014,37(5): 993-1016.
[12]	GOUBAULT L J , PARRENNES F . Cryptographic protocol analysis on real C code[C]// International Workshop on Verification,Model Checking,and Abstract Interpretation. 2005: 363-379.
[13]	JURJENS J . Automated security verification for crypto protocol implementations:verifying the JESSIE project[J]. Electronic Notes in Theoretical Computer Science, 2009,250(1): 123-136.
[14]	CHAKI S , DATTA A . ASPIER:an automated framework for verifying security protocol implementations[C]// 22nd IEEE Computer Security Foundations Symposium. 2009: 172-185.
[15]	DUPRESSOIR F , GORDON A D , JüRJENS J ,et al. Guiding a general-purpose C verifier to prove cryptographic protocols[C]// 24th IEEE Computer Security Foundations Symposium. 2011: 3-17.
[16]	BHARGAVAN K , GORDON A D . Modular verification of security protocol code by typing[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 2010: 445-456.
[17]	BACKES M , MAFFEI M , UNRUH D . Computationally sound verification of source code[C]// 17th ACM Conference on Computer and Communications Security. 2010: 387-398.
[18]	BENGTSON J , BHARGAVAN K , FOURNET C ,et al. Refinement types for secure implementations[J]. ACM Transactions on Programming Languages and Systems, 2011,33(2): 8-45.
[19]	SWAMY N , CHEN J , FOURENT C ,et al. Secure distributed programming with value-dependent types[C]// 16th ACM Sigplan International Conference on Functional Programming. 2011: 266-278.
[20]	SWAMY N , HRI?CU C , KELLER C ,et al. Semantic purity and effects reunited in F*[C]// 20th ACM SIGPLAN International Conference on Functional Programming. New York:ACM, 2015:12.
[21]	SWAMY N , HRI?CU C , KELLER C . Dependent types and multi-monadic effects in F*[C]// 43rd annual ACM SIGPLANSIGACT Symp on Principles of Programming Languages. 2016: 256-270.
[22]	BHARGAVAN K , FOURNET C , GORDON A D ,et al. Verified interoperable implementations of security protocols[J]. ACM Transactions on Programming Languages and Systems, 2008,31(1):5.
[23]	BHARGAVAN K , CORIN R , FOURNET C ,et al. Automated computational verification for cryptographic protocol implementations[J]. Unpublished draft,Oct, 2009.
[24]	BHARGAVAN K , FOURNET C , CORIN R ,et al. Cryptographically verified implementations for TLS[C]// 15th ACM Conference on Computer and Communications Security. 2008: 459-468.
[25]	MIHHAIL A , GORDON A D , JüRJENS J . Extracting and verifying cryptographic models from C protocol code by symbolic execution[C]// 18th ACM Conference on Computer and Communications Security. 2011: 331-340.
[26]	AIZATULIN M , GORDON A D , JURJENS J . Computational verification of C protocol implementations by symbolic execution[C]// 19th ACM Conference on Computer and Communications Security. 2012: 712-723.
[27]	BHARGAVAN K , BLANCHET K , KOBEISSI N . Verified models and reference implementations for the TLS 1.3 standard candidate[C]// 38th IEEE Symp on Security and Privacy. 2017:20.
[28]	BLANCHET B . A computationally sound mechanized prover for security protocols[J]. IEEE Transactions on Dependable and Secure Computing, 2008,5(4): 193-207.
[29]	BLANCHET B , . An efficient cryptographic protocol verifier based on prolog rules[C]// 14th IEEE Computer Security Foundations Workshop,Cape Breton. 2001: 82-96.
[30]	O'SHEA N , . Using ELYJAH to analyses Java implementations of cryptographic protocols[C]// FCS-ARSPA-WITS'08. 2008: 211-223.
[31]	LI Z M , MENG B , WANG D J ,et al. Mechanized verification of cryptographic security of cryptographic security protocol implementation in JAVA through model extraction in the computational model[J]. Journal of Software Engineering, 2015,9(1): 1-32.
[32]	唐朝京, 鲁智勇, 冯超 . 基于计算语义的安全协议验证逻辑[J]. 电子学报, 2014,42(6): 1179-1185.
	TANG Z J , LU Z Y , FENG C . A verification logic for security protocols based on computational semantics[J]. Chinese Journal of Electronics, 2014,42(6): 1179-1185.
[33]	SONY Corporation. The Swift Programming Language[EB/OL].[2017-4-1]
[34]	TERENCE P . The definitive Antrl4 reference[M]. USA: The Pragmatic BookshelfPress, 2012
[35]	SAKIMURA N , BRADLEY J , JONES M ,et al. OpenID connect core 1.0[EB/OL].[2017-1-10]
[36]	XU X D , NIU L Y , MENG B . Automatic verification of security properties of OAuth 2.0 protocol with CryptoVerif in computational model[J]. Information Technology Journal, 2013,12(12): 2273-2285.
[37]	MENG B , NIU L Y , YANG Y T ,et al. Mechanized verification of security properties of transport layer security 1.2 protocol with CryptoVerif in computational model[J]. Information Technology Journal, 2014,13(4): 601-613.
[38]	Client library for OAuth2/OpenID Connect[EB/OL].[2016-10-1].

Metrics

Recommended 0

No Suggested Reading articles found!

Security analysis of security protocol Swift implementations based on computational model

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 25

References 38

Related Articles 15

Metrics

Recommended 0

[1]	Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN [J]. Journal on Communications, 2021, 42(9): 240-253.
[2]	Wen GU,Ji-hong HAN,Lin YUAN. SSMCI:verification mechanism for security protocols centered on the attacker [J]. Journal on Communications, 2017, 38(10): 175-188.
[3]	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.
[4]	. Towards session identification using principal behavior for multi-party secure protocol [J]. Journal on Communications, 2015, 36(11): 190-200.
[5]	Chun-xiang GU,Huan-xiao WANG,Yong-hui ZHENG,Dan XIN,Nan LIU. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 117-125.
[6]	Zheng-da JIAO,Jian-feng MA,Cong SUN,Qing-song YAO. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 146-153.
[7]	. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 13-116.
[8]	. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 17-154.
[9]	Li-cai LIU,Li-hua YIN,Yun-chuan GUO,Yan SUN. Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 58-66.
[10]	Rong-sen LI,Wen-hua DOU. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 116-125.
[11]	. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 15-125.
[12]	. Analysis and improvement for authentication protocols ofmobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 8-66.
[13]	Jin-chao XU,Guo-sun ZENG,Wei WANG. Software services protection security protocol based on software watermarking in cloud environment [J]. Journal on Communications, 2012, 33(Z2): 176-181.
[14]	Zhi-geng HAN,Geng CHEN,Jun-zhou LUO. Modeling and analysis of multi-party non-repudiation protocols with extended-CSP approach [J]. Journal on Communications, 2012, 33(Z2): 189-195.
[15]	Lai-feng LU,Xin-dong DUAN,Jian-feng MA. Improvement and formal proof on protocol Otway-Rees [J]. Journal on Communications, 2012, 33(Z1): 250-254.